The low-degree homology of a k-linear G-representation

Let k be a commutative ring and G a group. This file contains specialised API for the cycles and group homology of a k-linear G-representation A in degrees 0, 1 and 2. In Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean, we define the nth group homology of A to be the homology of a complex inhomogeneousChains A, whose objects are (Fin n →₀ G) → A; this is unnecessarily unwieldy in low degree.

Given an additive abelian group A with an appropriate scalar action of G, we provide support for turning a finsupp f : G →₀ A satisfying the 1-cycle identity into an element of the cycles₁ of the representation on A corresponding to the scalar action. We also do this for 0-boundaries, 1-boundaries, 2-cycles and 2-boundaries.

The file also contains an identification between the definitions in Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean, groupHomology.cycles A n, and the cyclesₙ in this file for n = 1, 2, as well as an isomorphism groupHomology.cycles A 0 ≅ A.V. Moreover, we provide API for the natural maps cyclesₙ A → Hn A for n = 1, 2.

We show that when the representation on A is trivial, H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A.

Main definitions

• groupHomology.H0Iso A: isomorphism between H₀(G, A) and the coinvariants A_G of the G-representation on A.
• groupHomology.H1π A: epimorphism from the 1-cycles (i.e. Z₁(G, A) := Ker(d₀ : (G →₀ A) → A) to H₁(G, A).
• groupHomology.H2π A: epimorphism from the 2-cycles (i.e. Z₂(G, A) := Ker(d₁ : (G² →₀ A) → (G →₀ A)) to H₂(G, A).
• groupHomology.H1AddEquivOfIsTrivial: an isomorphism H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A when the representation on A is trivial.

noncomputable def groupHomology.chainsIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousChains A).X 0 ≅ ModuleCat.of k ↑A

The 0th object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to A as a k-module.

Equations

• groupHomology.chainsIso₀ A = (Finsupp.LinearEquiv.finsuppUnique k (↑A) (Fin 0 → G)).toModuleIso

noncomputable def groupHomology.chainsIso₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousChains A).X 1 ≅ ModuleCat.of k (G →₀ ↑A)

The 1st object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G →₀ A as a k-module.

Equations

• groupHomology.chainsIso₁ A = (Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)).toModuleIso

noncomputable def groupHomology.chainsIso₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousChains A).X 2 ≅ ModuleCat.of k (G × G →₀ ↑A)

The 2nd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G² →₀ A as a k-module.

Equations

• groupHomology.chainsIso₂ A = (Finsupp.domLCongr (piFinTwoEquiv fun (x : Fin 2) => G)).toModuleIso

noncomputable def groupHomology.chainsIso₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (inhomogeneousChains A).X 3 ≅ ModuleCat.of k (G × G × G →₀ ↑A)

The 3rd object in the complex of inhomogeneous chains of A : Rep k G is isomorphic to G³ → A as a k-module.

Equations

• groupHomology.chainsIso₃ A = (Finsupp.domLCongr ((Fin.consEquiv fun (i : Fin (2 + 1)) => G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) => G)))).toModuleIso

noncomputable def groupHomology.d₁₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G →₀ ↑A) ⟶ ModuleCat.of k ↑A

The 0th differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G →₀ A) → A. It is defined by single g a ↦ ρ_A(g⁻¹)(a) - a.

Equations

• groupHomology.d₁₀ A = ModuleCat.ofHom ((Finsupp.lsum k) fun (g : G) => A.ρ g⁻¹ - LinearMap.id)

@[simp]

theorem groupHomology.d₁₀_single {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₁₀ A)) (Finsupp.single g a) = (A.ρ g⁻¹) a - a

theorem groupHomology.d₁₀_single_one {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₁₀ A)) (Finsupp.single 1 a) = 0

theorem groupHomology.d₁₀_single_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₁₀ A)) (Finsupp.single g⁻¹ a) = -(CategoryTheory.ConcreteCategory.hom (d₁₀ A)) (Finsupp.single g ((A.ρ g) a))

theorem groupHomology.range_d₁₀_eq_coinvariantsKer {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (ModuleCat.Hom.hom (d₁₀ A)).range = Representation.Coinvariants.ker A.ρ

@[simp]

theorem groupHomology.d₁₀_comp_coinvariantsMk {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (d₁₀ A) ((Rep.coinvariantsMk k G).app A) = 0

@[simp]

theorem groupHomology.d₁₀_comp_coinvariantsMk_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (d₁₀ A) (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupHomology.d₁₀_comp_coinvariantsMk_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G →₀ ↑A) : (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) x) = 0 x

noncomputable def groupHomology.chains₁ToCoinvariantsKer {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G →₀ ↑A) ⟶ ModuleCat.of k ↥(Representation.Coinvariants.ker A.ρ)

The 0th differential in the complex of inhomogeneous chains of a G-representation A as a linear map into the k-submodule of A spanned by elements of the form ρ(g)(x) - x, g ∈ G, x ∈ A.

Equations

• groupHomology.chains₁ToCoinvariantsKer A = ModuleCat.ofHom (LinearMap.codRestrict (Representation.Coinvariants.ker A.ρ) (ModuleCat.Hom.hom (groupHomology.d₁₀ A)) ⋯)

theorem groupHomology.chains₁ToCoinvariantsKer_surjective {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (chains₁ToCoinvariantsKer A))

@[simp]

theorem groupHomology.d₁₀_eq_zero_of_isTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : d₁₀ A = 0

noncomputable def groupHomology.d₂₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G × G →₀ ↑A) ⟶ ModuleCat.of k (G →₀ ↑A)

The 1st differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G² →₀ A) → (G →₀ A). It is defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

Equations

• groupHomology.d₂₁ A = ModuleCat.ofHom ((Finsupp.lsum k) fun (g : G × G) => Finsupp.lsingle g.2 ∘ₗ A.ρ g.1⁻¹ - Finsupp.lsingle (g.1 * g.2) + Finsupp.lsingle g.1)

@[simp]

theorem groupHomology.d₂₁_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single g a) = Finsupp.single g.2 ((A.ρ g.1⁻¹) a) - Finsupp.single (g.1 * g.2) a + Finsupp.single g.1 a

theorem groupHomology.d₂₁_single_one_fst {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (1, g) a) = Finsupp.single 1 a

theorem groupHomology.d₂₁_single_one_snd {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (g, 1) a) = Finsupp.single 1 ((A.ρ g⁻¹) a)

theorem groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (g⁻¹, g) ((A.ρ g⁻¹) a) - Finsupp.single (g, g⁻¹) a) = Finsupp.single 1 a - Finsupp.single 1 ((A.ρ g⁻¹) a)

theorem groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (g, g⁻¹) ((A.ρ g) a) - Finsupp.single (g⁻¹, g) a) = Finsupp.single 1 a - Finsupp.single 1 ((A.ρ g) a)

theorem groupHomology.d₂₁_single_ρ_add_single_inv_mul {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (g, h) ((A.ρ g) a) + Finsupp.single (g⁻¹, g * h) a) = Finsupp.single g ((A.ρ g) a) + Finsupp.single g⁻¹ a

theorem groupHomology.d₂₁_single_inv_mul_ρ_add_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) (Finsupp.single (g⁻¹, g * h) ((A.ρ g⁻¹) a) + Finsupp.single (g, h) a) = Finsupp.single g⁻¹ ((A.ρ g⁻¹) a) + Finsupp.single g a

noncomputable def groupHomology.d₃₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k (G × G × G →₀ ↑A) ⟶ ModuleCat.of k (G × G →₀ ↑A)

The 2nd differential in the complex of inhomogeneous chains of A : Rep k G, as a k-linear map (G³ →₀ A) → (G² →₀ A). It is defined by a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.d₃₂_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G × G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) (Finsupp.single g a) = Finsupp.single (g.2.1, g.2.2) ((A.ρ g.1⁻¹) a) - Finsupp.single (g.1 * g.2.1, g.2.2) a + Finsupp.single (g.1, g.2.1 * g.2.2) a - Finsupp.single (g.1, g.2.1) a

theorem groupHomology.d₃₂_single_one_fst {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) (Finsupp.single (1, g, h) a) = Finsupp.single (1, g * h) a - Finsupp.single (1, g) a

theorem groupHomology.d₃₂_single_one_snd {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) (Finsupp.single (g, 1, h) a) = Finsupp.single (1, h) ((A.ρ g⁻¹) a) - Finsupp.single (g, 1) a

theorem groupHomology.d₃₂_single_one_thd {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) (Finsupp.single (g, h, 1) a) = Finsupp.single (h, 1) ((A.ρ g⁻¹) a) - Finsupp.single (g * h, 1) a

theorem groupHomology.comp_d₁₀_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₁ A).hom (d₁₀ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 1 0) (chainsIso₀ A).hom

Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₁₀ gives a simpler expression for the 0th differential: that is, the following square commutes:

  C₁(G, A) --d 1 0--> C₀(G, A)
    |                   |
    |                   |
    |                   |
    v                   v
  (G →₀ A) ----d₁₀----> A

where the vertical arrows are chainsIso₁ and chainsIso₀ respectively.

theorem groupHomology.eq_d₁₀_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv ((inhomogeneousChains A).d 1 0) = CategoryTheory.CategoryStruct.comp (d₁₀ A) (chainsIso₀ A).inv

theorem groupHomology.eq_d₁₀_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 0 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv (CategoryTheory.CategoryStruct.comp (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 1 0) h) = CategoryTheory.CategoryStruct.comp (d₁₀ A) (CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv h)

theorem groupHomology.eq_d₁₀_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 1 0)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) x)

theorem groupHomology.comp_d₂₁_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom (d₂₁ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 2 1) (chainsIso₁ A).hom

Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₂₁ gives a simpler expression for the 1st differential: that is, the following square commutes:

  C₂(G, A) --d 2 1--> C₁(G, A)
    |                    |
    |                    |
    |                    |
    v                    v
  (G² →₀ A) --d₂₁--> (G →₀ A)

where the vertical arrows are chainsIso₂ and chainsIso₁ respectively.

theorem groupHomology.eq_d₂₁_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv ((inhomogeneousChains A).d 2 1) = CategoryTheory.CategoryStruct.comp (d₂₁ A) (chainsIso₁ A).inv

theorem groupHomology.eq_d₂₁_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 1 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv (CategoryTheory.CategoryStruct.comp (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 2 1) h) = CategoryTheory.CategoryStruct.comp (d₂₁ A) (CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv h)

theorem groupHomology.eq_d₂₁_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 2 1)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x)

theorem groupHomology.comp_d₃₂_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₃ A).hom (d₃₂ A) = CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 3 2) (chainsIso₂ A).hom

Let C(G, A) denote the complex of inhomogeneous chains of A : Rep k G. This lemma says d₃₂ gives a simpler expression for the 2nd differential: that is, the following square commutes:

   C₃(G, A) --d 3 2--> C₂(G, A)
    |                    |
    |                    |
    |                    |
    v                    v
  (G³ →₀ A) --d₃₂--> (G² →₀ A)

where the vertical arrows are chainsIso₃ and chainsIso₂ respectively.

theorem groupHomology.eq_d₃₂_comp_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (chainsIso₃ A).inv ((inhomogeneousChains A).d 3 2) = CategoryTheory.CategoryStruct.comp (d₃₂ A) (chainsIso₂ A).inv

theorem groupHomology.eq_d₃₂_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 2 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainsIso₃ A).inv (CategoryTheory.CategoryStruct.comp (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 3 2) h) = CategoryTheory.CategoryStruct.comp (d₃₂ A) (CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv h)

theorem groupHomology.eq_d₃₂_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G × G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (ChainComplex.of.d (fun (n : ℕ) => ModuleCat.of k ((Fin n → G) →₀ ↑A)) (fun (n : ℕ) => inhomogeneousChains.d A n) 3 2)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₃ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) ((CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x)

@[simp]

theorem groupHomology.d₂₁_comp_d₁₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (d₂₁ A) (d₁₀ A) = 0

@[simp]

theorem groupHomology.d₂₁_comp_d₁₀_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↑A ⟶ Z) : CategoryTheory.CategoryStruct.comp (d₂₁ A) (CategoryTheory.CategoryStruct.comp (d₁₀ A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupHomology.d₂₁_comp_d₁₀_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (d₁₀ A)) ((CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x) = 0

@[simp]

theorem groupHomology.d₃₂_comp_d₂₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (d₃₂ A) (d₂₁ A) = 0

@[simp]

theorem groupHomology.d₃₂_comp_d₂₁_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k (G →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (d₃₂ A) (CategoryTheory.CategoryStruct.comp (d₂₁ A) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem groupHomology.d₃₂_comp_d₂₁_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : G × G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) ((CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x) = 0

noncomputable def groupHomology.shortComplexH0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The (exact) short complex (G →₀ A) ⟶ A ⟶ A.ρ.coinvariants.

Equations

• One or more equations did not get rendered due to their size.

theorem groupHomology.shortComplexH0_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).g = (Rep.coinvariantsMk k G).app A

theorem groupHomology.shortComplexH0_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).f = d₁₀ A

noncomputable def groupHomology.shortComplexH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A.

Equations

• groupHomology.shortComplexH1 A = { X₁ := ModuleCat.of k (G × G →₀ ↑A), X₂ := ModuleCat.of k (G →₀ ↑A), X₃ := ModuleCat.of k ↑A, f := groupHomology.d₂₁ A, g := groupHomology.d₁₀ A, zero := ⋯ }

theorem groupHomology.shortComplexH1_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH1 A).g = d₁₀ A

theorem groupHomology.shortComplexH1_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH1 A).f = d₂₁ A

noncomputable def groupHomology.shortComplexH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.ShortComplex (ModuleCat k)

The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A).

Equations

• One or more equations did not get rendered due to their size.

theorem groupHomology.shortComplexH2_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH2 A).g = d₂₁ A

theorem groupHomology.shortComplexH2_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH2 A).f = d₃₂ A

noncomputable def groupHomology.cycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G →₀ ↑A)

The 1-cycles Z₁(G, A) of A : Rep k G, defined as the kernel of the map (G →₀ A) → A defined by single g a ↦ ρ_A(g⁻¹)(a) - a.

Equations

• groupHomology.cycles₁ A = (ModuleCat.Hom.hom (groupHomology.d₁₀ A)).ker

noncomputable def groupHomology.cycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G × G →₀ ↑A)

The 2-cycles Z₂(G, A) of A : Rep k G, defined as the kernel of the map (G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

Equations

• groupHomology.cycles₂ A = (ModuleCat.Hom.hom (groupHomology.d₂₁ A)).ker

theorem groupHomology.mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G →₀ ↑A) : x ∈ cycles₁ A ↔ (x.sum fun (g : G) (a : ↑A) => (A.ρ g⁻¹) a) = x.sum fun (x : G) (a : ↑A) => a

theorem groupHomology.single_mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : Finsupp.single g a ∈ cycles₁ A ↔ (A.ρ g) a = a

theorem groupHomology.single_mem_cycles₁_of_mem_invariants {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) (ha : a ∈ A.ρ.invariants) : Finsupp.single g a ∈ cycles₁ A

theorem groupHomology.d₂₁_apply_mem_cycles₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (d₂₁ A)) x ∈ cycles₁ A

theorem groupHomology.cycles₁_eq_top_of_isTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : cycles₁ A = ⊤

noncomputable def groupHomology.cycles₁IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : ModuleCat.of k ↥(cycles₁ A) ≅ ModuleCat.of k (G →₀ ↑A)

The natural inclusion Z₁(G, A) ⟶ C₁(G, A) is an isomorphism when the representation on A is trivial.

Equations

• groupHomology.cycles₁IsoOfIsTrivial A = (LinearEquiv.ofTop (groupHomology.cycles₁ A) ⋯).toModuleIso

@[simp]

theorem groupHomology.cycles₁IsoOfIsTrivial_hom_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (x : ↥(cycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).hom) x = ↑x

@[simp]

theorem groupHomology.cycles₁IsoOfIsTrivial_inv_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (x : G →₀ ↑A) : ↑((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) x) = x

theorem groupHomology.mem_cycles₂_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G →₀ ↑A) : x ∈ cycles₂ A ↔ (x.sum fun (g : G × G) (a : ↑A) => Finsupp.single g.2 ((A.ρ g.1⁻¹) a) + Finsupp.single g.1 a) = x.sum fun (g : G × G) (a : ↑A) => Finsupp.single (g.1 * g.2) a

theorem groupHomology.single_mem_cycles₂_iff_inv {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : ↑A) : Finsupp.single g a ∈ cycles₂ A ↔ Finsupp.single g.2 ((A.ρ g.1⁻¹) a) + Finsupp.single g.1 a = Finsupp.single (g.1 * g.2) a

theorem groupHomology.single_mem_cycles₂_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : ↑A) : Finsupp.single g a ∈ cycles₂ A ↔ Finsupp.single (g.1 * g.2) ((A.ρ g.1) a) = Finsupp.single g.2 a + Finsupp.single g.1 ((A.ρ g.1) a)

theorem groupHomology.d₃₂_apply_mem_cycles₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G × G →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x ∈ cycles₂ A

noncomputable def groupHomology.boundaries₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G →₀ ↑A)

The 1-boundaries B₁(G, A) of A : Rep k G, defined as the image of the map (G² →₀ A) → (G →₀ A) defined by a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁.

Equations

• groupHomology.boundaries₁ A = (ModuleCat.Hom.hom (groupHomology.d₂₁ A)).range

noncomputable def groupHomology.boundaries₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : Submodule k (G × G →₀ ↑A)

The 2-boundaries B₂(G, A) of A : Rep k G, defined as the image of the map (G³ →₀ A) → (G² →₀ A) defined by a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂).

Equations

• groupHomology.boundaries₂ A = (ModuleCat.Hom.hom (groupHomology.d₃₂ A)).range

theorem groupHomology.mem_cycles₁_of_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G →₀ ↑A) (h : f ∈ boundaries₁ A) : f ∈ cycles₁ A

theorem groupHomology.boundaries₁_le_cycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : boundaries₁ A ≤ cycles₁ A

@[reducible, inline]

noncomputable abbrev groupHomology.boundariesToCycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(boundaries₁ A) →ₗ[k] ↥(cycles₁ A)

The natural inclusion B₁(G, A) →ₗ[k] Z₁(G, A).

Equations

• groupHomology.boundariesToCycles₁ A = Submodule.inclusion ⋯

@[simp]

theorem groupHomology.boundariesToCycles₁_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(boundaries₁ A)) : ↑((boundariesToCycles₁ A) x) = ↑x

theorem groupHomology.single_one_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (a : ↑A) : Finsupp.single 1 a ∈ boundaries₁ A

theorem groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : Finsupp.single g ((A.ρ g) a) + Finsupp.single g⁻¹ a ∈ boundaries₁ A

theorem groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A) : Finsupp.single g⁻¹ ((A.ρ g⁻¹) a) + Finsupp.single g a ∈ boundaries₁ A

theorem groupHomology.mem_cycles₂_of_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G × G →₀ ↑A) (h : x ∈ boundaries₂ A) : x ∈ cycles₂ A

theorem groupHomology.boundaries₂_le_cycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : boundaries₂ A ≤ cycles₂ A

@[reducible, inline]

noncomputable abbrev groupHomology.boundariesToCycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ↥(boundaries₂ A) →ₗ[k] ↥(cycles₂ A)

The natural inclusion B₂(G, A) →ₗ[k] Z₂(G, A).

Equations

• groupHomology.boundariesToCycles₂ A = Submodule.inclusion ⋯

@[simp]

theorem groupHomology.boundariesToCycles₂_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(boundaries₂ A)) : ↑((boundariesToCycles₂ A) x) = ↑x

theorem groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : Finsupp.single (1, g * h) a - Finsupp.single (1, g) a ∈ boundaries₂ A

theorem groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : Finsupp.single (1, h) ((A.ρ g⁻¹) a) - Finsupp.single (g, 1) a ∈ boundaries₂ A

theorem groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : Finsupp.single (g, 1) ((A.ρ g) a) - Finsupp.single (1, h) a ∈ boundaries₂ A

theorem groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g h : G) (a : ↑A) : Finsupp.single (h, 1) ((A.ρ g⁻¹) a) - Finsupp.single (g * h, 1) a ∈ boundaries₂ A

def groupHomology.IsCycle₁ {G : Type u_1} {A : Type u_2} [Inv G] [AddCommGroup A] [SMul G A] (x : G →₀ A) : Prop

A finsupp ∑ aᵢ·gᵢ : G →₀ A satisfies the 1-cycle condition if ∑ gᵢ⁻¹ • aᵢ = ∑ aᵢ.

Equations

• groupHomology.IsCycle₁ x = ((x.sum fun (g : G) (a : A) => g⁻¹ • a) = x.sum fun (x : G) (a : A) => a)

def groupHomology.IsCycle₂ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G × G →₀ A) : Prop

A finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A satisfies the 2-cycle condition if ∑ (gᵢ⁻¹ • aᵢ)·hᵢ + aᵢ·gᵢ = ∑ aᵢ·gᵢhᵢ.

Equations

• groupHomology.IsCycle₂ x = ((x.sum fun (g : G × G) (a : A) => Finsupp.single g.2 (g.1⁻¹ • a) + Finsupp.single g.1 a) = x.sum fun (g : G × G) (a : A) => Finsupp.single (g.1 * g.2) a)

@[simp]

theorem groupHomology.single_isCycle₁_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G) (a : A) : IsCycle₁ (Finsupp.single g a) ↔ g • a = a

theorem groupHomology.single_isCycle₁_of_mem_fixedPoints {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G) (a : A) (ha : a ∈ MulAction.fixedPoints G A) : IsCycle₁ (Finsupp.single g a)

theorem groupHomology.single_isCycle₂_iff_inv {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G × G) (a : A) : IsCycle₂ (Finsupp.single g a) ↔ Finsupp.single g.2 (g.1⁻¹ • a) + Finsupp.single g.1 a = Finsupp.single (g.1 * g.2) a

@[simp]

theorem groupHomology.single_isCycle₂_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (g : G × G) (a : A) : IsCycle₂ (Finsupp.single g a) ↔ Finsupp.single g.2 a + Finsupp.single g.1 (g.1 • a) = Finsupp.single (g.1 * g.2) (g.1 • a)

def groupHomology.IsBoundary₀ (G : Type u_1) {A : Type u_2} [Inv G] [AddCommGroup A] [SMul G A] (a : A) : Prop

A term x : A satisfies the 0-boundary condition if there exists a finsupp ∑ aᵢ·gᵢ : G →₀ A such that ∑ gᵢ⁻¹ • aᵢ - aᵢ = x.

Equations

• groupHomology.IsBoundary₀ G a = ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) => g⁻¹ • z - z) = a

def groupHomology.IsBoundary₁ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G →₀ A) : Prop

A finsupp x : G →₀ A satisfies the 1-boundary condition if there's a finsupp ∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A such that ∑ (gᵢ⁻¹ • aᵢ)·hᵢ - aᵢ·gᵢhᵢ + aᵢ·gᵢ = x.

Equations

• groupHomology.IsBoundary₁ x = ∃ (y : G × G →₀ A), (y.sum fun (g : G × G) (a : A) => Finsupp.single g.2 (g.1⁻¹ • a) - Finsupp.single (g.1 * g.2) a + Finsupp.single g.1 a) = x

def groupHomology.IsBoundary₂ {G : Type u_1} {A : Type u_2} [Mul G] [Inv G] [AddCommGroup A] [SMul G A] (x : G × G →₀ A) : Prop

A finsupp x : G × G →₀ A satisfies the 2-boundary condition if there's a finsupp ∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A such that ∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.

Equations

• One or more equations did not get rendered due to their size.

theorem groupHomology.isBoundary₀_iff (G : Type u_1) {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (a : A) : IsBoundary₀ G a ↔ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) => g • z - z) = a

theorem groupHomology.isBoundary₁_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (x : G →₀ A) : IsBoundary₁ x ↔ ∃ (y : G × G →₀ A), (y.sum fun (g : G × G) (a : A) => Finsupp.single g.2 a - Finsupp.single (g.1 * g.2) (g.1 • a) + Finsupp.single g.1 (g.1 • a)) = x

theorem groupHomology.isBoundary₂_iff {G : Type u_1} {A : Type u_2} [Group G] [AddCommGroup A] [DistribMulAction G A] (x : G × G →₀ A) : IsBoundary₂ x ↔ ∃ (y : G × G × G →₀ A), (y.sum fun (g : G × G × G) (a : A) => Finsupp.single (g.2.1, g.2.2) a - Finsupp.single (g.1 * g.2.1, g.2.2) (g.1 • a) + Finsupp.single (g.1, g.2.1 * g.2.2) (g.1 • a) - Finsupp.single (g.1, g.2.1) (g.1 • a)) = x

def groupHomology.coinvariantsKerOfIsBoundary₀ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : A) (hx : IsBoundary₀ G x) : ↥(Representation.Coinvariants.ker (Representation.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a term x : A satisfying the 0-boundary condition, this produces an element of the kernel of the quotient map A → A_G for the representation on A induced by the DistribMulAction.

Equations

• groupHomology.coinvariantsKerOfIsBoundary₀ x hx = ⟨x, ⋯⟩

@[simp]

theorem groupHomology.coinvariantsKerOfIsBoundary₀_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : A) (hx : IsBoundary₀ G x) : ↑(coinvariantsKerOfIsBoundary₀ x hx) = x

theorem groupHomology.isBoundary₀_of_mem_coinvariantsKer {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : A) (hx : x ∈ Representation.Coinvariants.ker (Representation.ofDistribMulAction k G A)) : IsBoundary₀ G x

def groupHomology.cyclesOfIsCycle₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : IsCycle₁ x) : ↥(cycles₁ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G →₀ A satisfying the 1-cycle condition, produces a 1-cycle for the representation on A induced by the DistribMulAction.

Equations

• groupHomology.cyclesOfIsCycle₁ x hx = ⟨x, ⋯⟩

@[simp]

theorem groupHomology.cyclesOfIsCycle₁_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : IsCycle₁ x) : ↑(cyclesOfIsCycle₁ x hx) = x

theorem groupHomology.isCycle₁_of_mem_cycles₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : x ∈ cycles₁ (Rep.ofDistribMulAction k G A)) : IsCycle₁ x

def groupHomology.boundariesOfIsBoundary₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : IsBoundary₁ x) : ↥(boundaries₁ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G →₀ A satisfying the 1-boundary condition, produces a 1-boundary for the representation on A induced by the DistribMulAction.

Equations

• groupHomology.boundariesOfIsBoundary₁ x hx = ⟨x, hx⟩

@[simp]

theorem groupHomology.boundariesOfIsBoundary₁_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : IsBoundary₁ x) : ↑(boundariesOfIsBoundary₁ x hx) = x

theorem groupHomology.isBoundary₁_of_mem_boundaries₁ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G →₀ A) (hx : x ∈ boundaries₁ (Rep.ofDistribMulAction k G A)) : IsBoundary₁ x

def groupHomology.cyclesOfIsCycle₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : IsCycle₂ x) : ↥(cycles₂ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G × G →₀ A satisfying the 2-cycle condition, produces a 2-cycle for the representation on A induced by the DistribMulAction.

Equations

• groupHomology.cyclesOfIsCycle₂ x hx = ⟨x, ⋯⟩

@[simp]

theorem groupHomology.cyclesOfIsCycle₂_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : IsCycle₂ x) : ↑(cyclesOfIsCycle₂ x hx) = x

theorem groupHomology.isCycle₂_of_mem_cycles₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : x ∈ cycles₂ (Rep.ofDistribMulAction k G A)) : IsCycle₂ x

def groupHomology.boundariesOfIsBoundary₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : IsBoundary₂ x) : ↥(boundaries₂ (Rep.ofDistribMulAction k G A))

Given a k-module A with a compatible DistribMulAction of G, and a finsupp x : G × G →₀ A satisfying the 2-boundary condition, produces a 2-boundary for the representation on A induced by the DistribMulAction.

Equations

• groupHomology.boundariesOfIsBoundary₂ x hx = ⟨x, hx⟩

@[simp]

theorem groupHomology.boundariesOfIsBoundary₂_coe {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : IsBoundary₂ x) : ↑(boundariesOfIsBoundary₂ x hx) = x

theorem groupHomology.isBoundary₂_of_mem_boundaries₂ {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (x : G × G →₀ A) (hx : x ∈ boundaries₂ (Rep.ofDistribMulAction k G A)) : IsBoundary₂ x

instance groupHomology.instEpiModuleCatGShortComplexH0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (shortComplexH0 A).g

theorem groupHomology.shortComplexH0_exact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (shortComplexH0 A).Exact

noncomputable def groupHomology.cyclesIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cycles A 0 ≅ ModuleCat.of k ↑A

The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to A.

Equations

• groupHomology.cyclesIso₀ A = HomologicalComplex.iCyclesIso (groupHomology.inhomogeneousChains A) 0 0 groupHomology.cyclesIso₀._proof_1 ⋯ ≪≫ groupHomology.chainsIso₀ A

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_iCycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).inv (iCycles A 0) = (chainsIso₀ A).inv

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_iCycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 0 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).inv (CategoryTheory.CategoryStruct.comp (iCycles A 0) h) = CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv h

@[simp]

theorem groupHomology.cyclesIso₀_inv_comp_iCycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom (iCycles A 0)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x

noncomputable def groupHomology.d₁₀ArrowIso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Arrow.mk ((inhomogeneousChains A).d 1 0) ≅ CategoryTheory.Arrow.mk (d₁₀ A)

The arrow (G →₀ A) --d₁₀--> A is isomorphic to the differential (inhomogeneousChains A).d 1 0 of the complex of inhomogeneous chains of A.

Equations

• groupHomology.d₁₀ArrowIso A = CategoryTheory.Arrow.isoMk (groupHomology.chainsIso₁ A) (groupHomology.chainsIso₀ A) ⋯

@[simp]

theorem groupHomology.d₁₀ArrowIso_hom_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (d₁₀ArrowIso A).hom.right = (chainsIso₀ A).hom

@[simp]

theorem groupHomology.d₁₀ArrowIso_inv_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (d₁₀ArrowIso A).inv.left = (chainsIso₁ A).inv

@[simp]

theorem groupHomology.d₁₀ArrowIso_hom_left {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (d₁₀ArrowIso A).hom.left = (chainsIso₁ A).hom

@[simp]

theorem groupHomology.d₁₀ArrowIso_inv_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (d₁₀ArrowIso A).inv.right = (chainsIso₀ A).inv

noncomputable def groupHomology.opcyclesIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.opcycles (inhomogeneousChains A) 0 ≅ (Rep.coinvariantsFunctor k G).obj A

The 0-cycles of the complex of inhomogeneous chains of A are isomorphic to A.ρ.coinvariants, which is a simpler type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.pOpcycles_comp_opcyclesIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0) (opcyclesIso₀ A).hom = CategoryTheory.CategoryStruct.comp (chainsIso₀ A).hom ((Rep.coinvariantsMk k G).app A)

@[simp]

theorem groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0) (CategoryTheory.CategoryStruct.comp (opcyclesIso₀ A).hom h) = CategoryTheory.CategoryStruct.comp (chainsIso₀ A).hom (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h)

@[simp]

theorem groupHomology.pOpcycles_comp_opcyclesIso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : (Fin 0 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (opcyclesIso₀ A).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0)) x) = (CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).hom) x)

@[simp]

theorem groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (opcyclesIso₀ A).inv = CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0)

@[simp]

theorem groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : HomologicalComplex.opcycles (inhomogeneousChains A) 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (CategoryTheory.CategoryStruct.comp (opcyclesIso₀ A).inv h) = CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0) h)

@[simp]

theorem groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).obj A)) : (CategoryTheory.ConcreteCategory.hom (opcyclesIso₀ A).inv) ((CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) x) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0)) ((CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x)

theorem groupHomology.cyclesMk₀_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑A) : cyclesMk 0 0 cyclesMk₀_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x) ⋯ = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x

noncomputable def groupHomology.isoShortComplexH1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousChains A) 1 ≅ shortComplexH1 A

The short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A is isomorphic to the 1st short complex associated to the complex of inhomogeneous chains of A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.isoShortComplexH1_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH1 A).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homMk (chainsIso₂ A).inv (chainsIso₁ A).inv (chainsIso₀ A).inv ⋯ ⋯) ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 isoShortComplexH1._proof_1 isoShortComplexH1._proof_2).inv.app (inhomogeneousChains A))

@[simp]

theorem groupHomology.isoShortComplexH1_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH1 A).hom = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 isoShortComplexH1._proof_1 isoShortComplexH1._proof_2).hom.app (inhomogeneousChains A)) (CategoryTheory.ShortComplex.isoMk (chainsIso₂ A) (chainsIso₁ A) (chainsIso₀ A) ⋯ ⋯).hom

noncomputable def groupHomology.isoCycles₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cycles A 1 ≅ ModuleCat.of k ↥(cycles₁ A)

The 1-cycles of the complex of inhomogeneous chains of A are isomorphic to cycles₁ A, which is a simpler type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.isoCycles₁_hom_comp_i {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (iCycles A 1) (chainsIso₁ A).hom

@[simp]

theorem groupHomology.isoCycles₁_hom_comp_i_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH1 A).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (iCycles A 1) (CategoryTheory.CategoryStruct.comp (chainsIso₁ A).hom h)

@[simp]

theorem groupHomology.isoCycles₁_hom_comp_i_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 1)) : (ModuleCat.Hom.hom (shortComplexH1 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (iCycles A 1)) x)

@[simp]

theorem groupHomology.isoCycles₁_inv_comp_iCycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCycles₁ A).inv (iCycles A 1) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (chainsIso₁ A).inv

@[simp]

theorem groupHomology.isoCycles₁_inv_comp_iCycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 1 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCycles₁ A).inv (CategoryTheory.CategoryStruct.comp (iCycles A 1) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (chainsIso₁ A).inv) h

@[simp]

theorem groupHomology.isoCycles₁_inv_comp_iCycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (iCycles A 1)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (chainsIso₁ A).inv)) x

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₁_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (toCycles A 2 1) (isoCycles₁ A).hom = CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.f'

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₁_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cycles₁ A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toCycles A 2 1) (CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom h) = CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.f' h)

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₁_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : (Fin 2 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 2 1)) x) = (shortComplexH1 A).moduleCatToCycles ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).hom) x)

theorem groupHomology.cyclesMk₁_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₁ A)) : cyclesMk 1 0 cyclesMk₁_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).inv) x

noncomputable def groupHomology.isoShortComplexH2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : HomologicalComplex.sc (inhomogeneousChains A) 2 ≅ shortComplexH2 A

The short complex (G³ →₀ A) --d₃₂--> (G² →₀ A) --d₂₁--> (G →₀ A) is isomorphic to the 2nd short complex associated to the complex of inhomogeneous chains of A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.isoShortComplexH2_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH2 A).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homMk (chainsIso₃ A).inv (chainsIso₂ A).inv (chainsIso₁ A).inv ⋯ ⋯) ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 isoShortComplexH2._proof_1 isoShortComplexH2._proof_2).inv.app (inhomogeneousChains A))

@[simp]

theorem groupHomology.isoShortComplexH2_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : (isoShortComplexH2 A).hom = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 3 2 1 isoShortComplexH2._proof_1 isoShortComplexH2._proof_2).hom.app (inhomogeneousChains A)) (CategoryTheory.ShortComplex.isoMk (chainsIso₃ A) (chainsIso₂ A) (chainsIso₁ A) ⋯ ⋯).hom

noncomputable def groupHomology.isoCycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : cycles A 2 ≅ ModuleCat.of k ↥(cycles₂ A)

The 2-cycles of the complex of inhomogeneous chains of A are isomorphic to cycles₂ A, which is a simpler type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.isoCycles₂_hom_comp_i {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.i = CategoryTheory.CategoryStruct.comp (iCycles A 2) (chainsIso₂ A).hom

@[simp]

theorem groupHomology.isoCycles₂_hom_comp_i_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH2 A).X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i h) = CategoryTheory.CategoryStruct.comp (iCycles A 2) (CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom h)

@[simp]

theorem groupHomology.isoCycles₂_hom_comp_i_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 2)) : (ModuleCat.Hom.hom (shortComplexH2 A).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (iCycles A 2)) x)

@[simp]

theorem groupHomology.isoCycles₂_inv_comp_iCycles {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (isoCycles₂ A).inv (iCycles A 2) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (chainsIso₂ A).inv

@[simp]

theorem groupHomology.isoCycles₂_inv_comp_iCycles_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin 2 → G) →₀ ↑A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoCycles₂ A).inv (CategoryTheory.CategoryStruct.comp (iCycles A 2) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (chainsIso₂ A).inv) h

@[simp]

theorem groupHomology.isoCycles₂_inv_comp_iCycles_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (iCycles A 2)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (chainsIso₂ A).inv)) x

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₂_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (toCycles A 3 2) (isoCycles₂ A).hom = CategoryTheory.CategoryStruct.comp (chainsIso₃ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.f'

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₂_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : ModuleCat.of k ↥(cycles₂ A) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toCycles A 3 2) (CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom h) = CategoryTheory.CategoryStruct.comp (chainsIso₃ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.f' h)

@[simp]

theorem groupHomology.toCycles_comp_isoCycles₂_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : (Fin 3 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 3 2)) x) = (shortComplexH2 A).moduleCatToCycles ((CategoryTheory.ConcreteCategory.hom (chainsIso₃ A).hom) x)

theorem groupHomology.cyclesMk₂_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₂ A)) : cyclesMk 2 1 cyclesMk₂_eq._proof_1 ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).inv) x

@[reducible, inline]

noncomputable abbrev groupHomology.H0 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 0th group homology of a k-linear G-representation A, H₀(G, A), defined as the 0th homology of the complex of inhomogeneous chains of A.

Equations

• groupHomology.H0 A = groupHomology A 0

noncomputable def groupHomology.H0Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H0 A ≅ (Rep.coinvariantsFunctor k G).obj A

The 0th group homology of A, defined as the 0th homology of the complex of inhomogeneous chains, is isomorphic to the invariants of the representation on A.

Equations

• groupHomology.H0Iso A = (groupHomology.inhomogeneousChains A).isoHomologyι₀ ≪≫ groupHomology.opcyclesIso₀ A

noncomputable def groupHomology.H0π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k ↑A ⟶ H0 A

The quotient map from A to H₀(G, A).

Equations

• groupHomology.H0π A = CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv (groupHomology.π A 0)

instance groupHomology.instEpiModuleCatH0π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (H0π A)

@[simp]

theorem groupHomology.π_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 0) (H0Iso A).hom = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom ((Rep.coinvariantsMk k G).app A)

@[simp]

theorem groupHomology.π_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 0) (CategoryTheory.CategoryStruct.comp (H0Iso A).hom h) = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h)

@[simp]

theorem groupHomology.π_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 0)) : (CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x)

@[simp]

theorem groupHomology.coinvariantsMk_comp_H0Iso_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (H0Iso A).inv = H0π A

@[simp]

theorem groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : H0 A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) (CategoryTheory.CategoryStruct.comp (H0Iso A).inv h) = CategoryTheory.CategoryStruct.comp (H0π A) h

@[simp]

theorem groupHomology.coinvariantsMk_comp_H0Iso_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).obj A)) : (CategoryTheory.ConcreteCategory.hom (H0Iso A).inv) ((CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) x) = (CategoryTheory.ConcreteCategory.hom (H0π A)) x

@[simp]

theorem groupHomology.H0π_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (H0π A) (H0Iso A).hom = (Rep.coinvariantsMk k G).app A

@[simp]

theorem groupHomology.H0π_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (Rep.coinvariantsFunctor k G).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0π A) (CategoryTheory.CategoryStruct.comp (H0Iso A).hom h) = CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) h

@[simp]

theorem groupHomology.H0π_comp_H0Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑A) : (CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (H0π A)) x) = (CategoryTheory.ConcreteCategory.hom ((Rep.coinvariantsMk k G).app A)) x

@[simp]

theorem groupHomology.cyclesIso₀_comp_H0π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom (H0π A) = π A 0

@[simp]

theorem groupHomology.cyclesIso₀_comp_H0π_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : H0 A ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom (CategoryTheory.CategoryStruct.comp (H0π A) h) = CategoryTheory.CategoryStruct.comp (π A 0) h

@[simp]

theorem groupHomology.cyclesIso₀_comp_H0π_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 0)) : (CategoryTheory.ConcreteCategory.hom (H0π A)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x) = (CategoryTheory.ConcreteCategory.hom (π A 0)) x

theorem groupHomology.H0_induction_on {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {C : ↑(H0 A) → Prop} (x : ↑(H0 A)) (h : ∀ (x : ↑A), C ((CategoryTheory.ConcreteCategory.hom (H0π A)) x)) : C x

noncomputable def groupHomology.H0IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : H0 A ≅ ModuleCat.of k ↑A

When the representation on A is trivial, then H₀(G, A) is all of A.

Equations

• groupHomology.H0IsoOfIsTrivial A = (HomologicalComplex.isoHomologyπ (groupHomology.inhomogeneousChains A) 1 0 groupHomology.opcyclesIso₀._proof_1 ⋯).symm ≪≫ groupHomology.cyclesIso₀ A

@[simp]

theorem groupHomology.H0IsoOfIsTrivial_inv_eq_π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : (H0IsoOfIsTrivial A).inv = H0π A

@[simp]

theorem groupHomology.π_comp_H0IsoOfIsTrivial_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : CategoryTheory.CategoryStruct.comp (π A 0) (H0IsoOfIsTrivial A).hom = (cyclesIso₀ A).hom

@[simp]

theorem groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] {Z : ModuleCat k} (h : ModuleCat.of k ↑A ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 0) (CategoryTheory.CategoryStruct.comp (H0IsoOfIsTrivial A).hom h) = CategoryTheory.CategoryStruct.comp (cyclesIso₀ A).hom h

@[simp]

theorem groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (x : ↑(cycles A 0)) : (CategoryTheory.ConcreteCategory.hom (H0IsoOfIsTrivial A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x

@[reducible, inline]

noncomputable abbrev groupHomology.H1 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 1st group homology of a k-linear G-representation A, H₁(G, A), defined as the 1st homology of the complex of inhomogeneous chains of A.

Equations

• groupHomology.H1 A = groupHomology A 1

noncomputable def groupHomology.H1π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k ↥(cycles₁ A) ⟶ H1 A

The quotient map from the 1-cycles of A, as a submodule of G →₀ A, to H₁(G, A).

Equations

• groupHomology.H1π A = CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).inv (groupHomology.π A 1)

instance groupHomology.instEpiModuleCatH1π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (H1π A)

theorem groupHomology.H1π_eq_zero_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A

theorem groupHomology.H1π_eq_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x y : ↥(cycles₁ A)) : (CategoryTheory.ConcreteCategory.hom (H1π A)) x = (CategoryTheory.ConcreteCategory.hom (H1π A)) y ↔ ↑x - ↑y ∈ boundaries₁ A

theorem groupHomology.H1_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(H1 A) → Prop} (x : ↑(H1 A)) (h : ∀ (x : ↥(cycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (H1π A)) x)) : C x

noncomputable def groupHomology.H1Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H1 A ≅ (shortComplexH1 A).moduleCatLeftHomologyData.H

The 1st group homology of A, defined as the 1st homology of the complex of inhomogeneous chains, is isomorphic to cycles₁ A ⧸ boundaries₁ A, which is a simpler type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.π_comp_H1Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 1) (H1Iso A).hom = CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.π

@[simp]

theorem groupHomology.π_comp_H1Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH1 A).moduleCatLeftHomologyData.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 1) (CategoryTheory.CategoryStruct.comp (H1Iso A).hom h) = CategoryTheory.CategoryStruct.comp (isoCycles₁ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.π h)

@[simp]

theorem groupHomology.π_comp_H1Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 1)) : (CategoryTheory.ConcreteCategory.hom (H1Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 1)) x) = (shortComplexH1 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x)

@[simp]

theorem groupHomology.π_comp_H1Iso_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.π (H1Iso A).inv = H1π A

@[simp]

theorem groupHomology.π_comp_H1Iso_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : H1 A ⟶ Z) : CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.π (CategoryTheory.CategoryStruct.comp (H1Iso A).inv h) = CategoryTheory.CategoryStruct.comp (H1π A) h

@[simp]

theorem groupHomology.π_comp_H1Iso_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(shortComplexH1 A).moduleCatLeftHomologyData.K) : (CategoryTheory.ConcreteCategory.hom (H1Iso A).inv) ((shortComplexH1 A).moduleCatToCycles.range.mkQ x) = (CategoryTheory.ConcreteCategory.hom (H1π A)) x

noncomputable def groupHomology.mkH1OfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : Additive (Abelianization G) →ₗ[ℤ] ↑A →ₗ[ℤ] ↑(H1 A)

If a G-representation on A is trivial, this is the natural map Gᵃᵇ → A → H₁(G, A) sending ⟦g⟧, a to ⟦single g a⟧.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.mkH1OfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (g : G) (a : ↑A) : ((mkH1OfIsTrivial A) (Additive.ofMul (Abelianization.of g))) a = (CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))

noncomputable def groupHomology.H1ToTensorOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : ↑(H1 A) →ₗ[ℤ] TensorProduct ℤ (Additive (Abelianization G)) ↑A

If a G-representation on A is trivial, this is the natural map H₁(G, A) → Gᵃᵇ ⊗[ℤ] A sending ⟦single g a⟧ to ⟦g⟧ ⊗ₜ a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.H1ToTensorOfIsTrivial_H1π_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (g : G) (a : ↑A) : (H1ToTensorOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

noncomputable def groupHomology.H1AddEquivOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] : ↑(H1 A) ≃+ TensorProduct ℤ (Additive (Abelianization G)) ↑A

If a G-representation on A is trivial, this is the group isomorphism between H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A defined by ⟦single g a⟧ ↦ ⟦g⟧ ⊗ a.

Equations

• groupHomology.H1AddEquivOfIsTrivial A = (LinearEquiv.ofLinear (groupHomology.H1ToTensorOfIsTrivial A) (TensorProduct.lift (groupHomology.mkH1OfIsTrivial A)) ⋯ ⋯).toAddEquiv

theorem groupHomology.H1AddEquivOfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (a✝ : ↑(H1 A)) : (H1AddEquivOfIsTrivial A) a✝ = (H1ToTensorOfIsTrivial A) a✝

theorem groupHomology.H1AddEquivOfIsTrivial_symm_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (a✝ : TensorProduct ℤ (Additive (Abelianization G)) ↑A) : (H1AddEquivOfIsTrivial A).symm a✝ = (TensorProduct.lift (mkH1OfIsTrivial A)) a✝

@[simp]

theorem groupHomology.H1AddEquivOfIsTrivial_single {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (g : G) (a : ↑A) : (H1AddEquivOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

@[simp]

theorem groupHomology.H1AddEquivOfIsTrivial_symm_tmul {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (g : G) (a : ↑A) : (H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) = (CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))

@[reducible, inline]

noncomputable abbrev groupHomology.H2 {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat k

Shorthand for the 2nd group homology of a k-linear G-representation A, H₂(G, A), defined as the 2nd homology of the complex of inhomogeneous chains of A.

Equations

• groupHomology.H2 A = groupHomology A 2

noncomputable def groupHomology.H2π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : ModuleCat.of k ↥(cycles₂ A) ⟶ H2 A

The quotient map from the 2-cycles of A, as a submodule of G × G →₀ A, to H₂(G, A).

Equations

• groupHomology.H2π A = CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).inv (groupHomology.π A 2)

instance groupHomology.instEpiModuleCatH2π {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Epi (H2π A)

theorem groupHomology.H2π_eq_zero_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : ↥(cycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (H2π A)) x = 0 ↔ ↑x ∈ boundaries₂ A

theorem groupHomology.H2π_eq_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x y : ↥(cycles₂ A)) : (CategoryTheory.ConcreteCategory.hom (H2π A)) x = (CategoryTheory.ConcreteCategory.hom (H2π A)) y ↔ ↑x - ↑y ∈ boundaries₂ A

theorem groupHomology.H2_induction_on {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {C : ↑(H2 A) → Prop} (x : ↑(H2 A)) (h : ∀ (x : ↥(cycles₂ A)), C ((CategoryTheory.ConcreteCategory.hom (H2π A)) x)) : C x

noncomputable def groupHomology.H2Iso {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : H2 A ≅ (shortComplexH2 A).moduleCatLeftHomologyData.H

The 2nd group homology of A, defined as the 2nd homology of the complex of inhomogeneous chains, is isomorphic to cycles₂ A ⧸ boundaries₂ A, which is a simpler type.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem groupHomology.π_comp_H2Iso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (π A 2) (H2Iso A).hom = CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.π

@[simp]

theorem groupHomology.π_comp_H2Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (shortComplexH2 A).moduleCatLeftHomologyData.H ⟶ Z) : CategoryTheory.CategoryStruct.comp (π A 2) (CategoryTheory.CategoryStruct.comp (H2Iso A).hom h) = CategoryTheory.CategoryStruct.comp (isoCycles₂ A).hom (CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.π h)

@[simp]

theorem groupHomology.π_comp_H2Iso_hom_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(cycles A 2)) : (CategoryTheory.ConcreteCategory.hom (H2Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 2)) x) = (shortComplexH2 A).moduleCatToCycles.range.mkQ ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x)

@[simp]

theorem groupHomology.π_comp_H2Iso_inv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.π (H2Iso A).inv = H2π A

@[simp]

theorem groupHomology.π_comp_H2Iso_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : H2 A ⟶ Z) : CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.π (CategoryTheory.CategoryStruct.comp (H2Iso A).inv h) = CategoryTheory.CategoryStruct.comp (H2π A) h

@[simp]

theorem groupHomology.π_comp_H2Iso_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑(shortComplexH2 A).moduleCatLeftHomologyData.K) : (CategoryTheory.ConcreteCategory.hom (H2Iso A).inv) ((shortComplexH2 A).moduleCatToCycles.range.mkQ x) = (CategoryTheory.ConcreteCategory.hom (H2π A)) x