Documentation

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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.

def groupHomology.chainsIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

(inhomogeneousChains A).X 0 ≅ A.V

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

Equations

Instances For

def groupHomology.chainsIso₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

(inhomogeneousChains A).X 1 ≅ ModuleCat.of k (G →₀ ↑A.V)

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

Equations

Instances For

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.V)

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

Equations

Instances For

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.V)

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

Equations

Instances For

def groupHomology.d₁₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

ModuleCat.of k (G →₀ ↑A.V) ⟶ A.V

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

Instances For

@[simp]

theorem groupHomology.d₁₀_single {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (g : G) (a : ↑A.V) :

(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.V) :

(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.V) :

(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) :

LinearMap.range (ModuleCat.Hom.hom (d₁₀ A)) = 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 : CategoryTheory.ToType (ModuleCat.of k (G →₀ ↑A.V))) :

(Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (d₁₀ A)) x) = 0 x

def groupHomology.chains₁ToCoinvariantsKer {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

ModuleCat.of k (G →₀ ↑A.V) ⟶ 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

Instances For

@[simp]

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

def groupHomology.d₂₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

ModuleCat.of k (G × G →₀ ↑A.V) ⟶ ModuleCat.of k (G →₀ ↑A.V)

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

Instances For

@[simp]

theorem groupHomology.d₂₁_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G) (a : ↑A.V) :

(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.V) :

(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.V) :

(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.V) :

(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.V) :

(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.V) :

(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.V) :

(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

def groupHomology.d₃₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

ModuleCat.of k (G × G × G →₀ ↑A.V) ⟶ ModuleCat.of k (G × G →₀ ↑A.V)

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

Instances For

@[simp]

theorem groupHomology.d₃₂_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G × G × G) (a : ↑A.V) :

(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.V) :

(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.V) :

(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.V) :

(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.

@[simp]

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

@[simp]

theorem groupHomology.eq_d₁₀_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousChains A).X 0 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 1 0) h) = CategoryTheory.CategoryStruct.comp (d₁₀ A) (CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv h)

@[simp]

theorem groupHomology.eq_d₁₀_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G →₀ ↑A.V))) :

(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 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.

@[simp]

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

@[simp]

theorem groupHomology.eq_d₂₁_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousChains A).X 1 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 2 1) h) = CategoryTheory.CategoryStruct.comp (d₂₁ A) (CategoryTheory.CategoryStruct.comp (chainsIso₁ A).inv h)

@[simp]

theorem groupHomology.eq_d₂₁_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G × G →₀ ↑A.V))) :

(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 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.

@[simp]

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

@[simp]

theorem groupHomology.eq_d₃₂_comp_inv_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {Z : ModuleCat k} (h : (inhomogeneousChains A).X 2 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (chainsIso₃ A).inv (CategoryTheory.CategoryStruct.comp ((inhomogeneousChains A).d 3 2) h) = CategoryTheory.CategoryStruct.comp (d₃₂ A) (CategoryTheory.CategoryStruct.comp (chainsIso₂ A).inv h)

@[simp]

theorem groupHomology.eq_d₃₂_comp_inv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : CategoryTheory.ToType (ModuleCat.of k (G × G × G →₀ ↑A.V))) :

(CategoryTheory.ConcreteCategory.hom ((inhomogeneousChains A).d 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 : A.V ⟶ 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 : CategoryTheory.ToType (ModuleCat.of k (G × G →₀ ↑A.V))) :

(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.V) ⟶ 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 : CategoryTheory.ToType (ModuleCat.of k (G × G × G →₀ ↑A.V))) :

(CategoryTheory.ConcreteCategory.hom (d₂₁ A)) ((CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x) = 0

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

Instances For

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

(shortComplexH0 A).f = d₁₀ A

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

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

Instances For

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

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

Instances For

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

(shortComplexH2 A).f = d₃₂ A

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

(shortComplexH2 A).g = d₂₁ A

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

Submodule k (G →₀ ↑A.V)

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

Instances For

def groupHomology.cycles₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

Submodule k (G × G →₀ ↑A.V)

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

Instances For

theorem groupHomology.mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (x : G →₀ ↑A.V) :

x ∈ cycles₁ A ↔ (x.sum fun (g : G) (a : ↑A.V) => (A.ρ g⁻¹) a) = x.sum fun (x : G) (a : ↑A.V) => a

theorem groupHomology.single_mem_cycles₁_iff {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (g : G) (a : ↑A.V) :

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.V) (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.V) :

(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 = ⊤

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.V)

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

Equations

Instances For

@[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.V) :

↑((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.V) :

x ∈ cycles₂ A ↔ (x.sum fun (g : G × G) (a : ↑A.V) => Finsupp.single g.2 ((A.ρ g.1⁻¹) a) + Finsupp.single g.1 a) = x.sum fun (g : G × G) (a : ↑A.V) => 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.V) :

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.V) :

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.V) :

(CategoryTheory.ConcreteCategory.hom (d₃₂ A)) x ∈ cycles₂ A

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

Submodule k (G →₀ ↑A.V)

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

Instances For

def groupHomology.boundaries₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

Submodule k (G × G →₀ ↑A.V)

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

Instances For

theorem groupHomology.mem_cycles₁_of_mem_boundaries₁ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} (f : G →₀ ↑A.V) (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]

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

Instances For

@[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.V) :

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.V) :

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.V) :

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.V) (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]

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

Instances For

@[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.V) :

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.V) :

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.V) :

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.V) :

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) :

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

Equations

Instances For

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

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

Equations

Instances For

@[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) :

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

@[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

Instances For

@[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)) :

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

Instances For

@[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

Instances For

@[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)) :

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

Instances For

@[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

def groupHomology.cyclesIso₀ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

cycles A 0 ≅ A.V

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

Equations

Instances For

@[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 : (inhomogeneousChains A).X 0 ⟶ 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 : CategoryTheory.ToType A.V) :

(CategoryTheory.ConcreteCategory.hom (iCycles A 0)) ((CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x) = (CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x

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

Instances For

@[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

@[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_hom_right {k G : Type u} [CommRing k] [Group G] (A : Rep k G) :

(d₁₀ArrowIso A).hom.right = (chainsIso₀ A).hom

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

Instances For

@[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 : CategoryTheory.ToType ((inhomogeneousChains A).X 0)) :

(CategoryTheory.ConcreteCategory.hom (opcyclesIso₀ A).hom) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0)) x) = (Representation.Coinvariants.mk 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.ToType ((Action.forget (ModuleCat k) G).obj A)) :

(CategoryTheory.ConcreteCategory.hom (opcyclesIso₀ A).inv) ((Representation.Coinvariants.mk A.ρ) x) = (CategoryTheory.CategoryStruct.comp (chainsIso₀ A).inv (HomologicalComplex.pOpcycles (inhomogeneousChains A) 0)) x

theorem groupHomology.cyclesMk₀_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↑A.V) :

cyclesMk 0 0 ⋯ ((CategoryTheory.ConcreteCategory.hom (chainsIso₀ A).inv) x) ⋯ = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).inv) x

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

Instances For

@[simp]

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

@[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

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

Instances For

@[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 : CategoryTheory.ToType (cycles A 1)) :

(LinearMap.ker (ModuleCat.Hom.hom (shortComplexH1 A).g)).subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) x) = (CategoryTheory.CategoryStruct.comp (iCycles A 1) (chainsIso₁ A).hom) 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 : (inhomogeneousChains A).X 1 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (isoCycles₁ A).inv (CategoryTheory.CategoryStruct.comp (iCycles A 1) h) = CategoryTheory.CategoryStruct.comp (shortComplexH1 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (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 : CategoryTheory.ToType (ModuleCat.of k ↥(cycles₁ A))) :

(CategoryTheory.ConcreteCategory.hom (iCycles A 1)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).inv) x) = (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 : CategoryTheory.ToType ((inhomogeneousChains A).X 2)) :

(CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 2 1)) x) = (CategoryTheory.CategoryStruct.comp (chainsIso₂ A).hom (shortComplexH1 A).moduleCatLeftHomologyData.f') x

theorem groupHomology.cyclesMk₁_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₁ A)) :

cyclesMk 1 0 ⋯ ((CategoryTheory.ConcreteCategory.hom (chainsIso₁ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₁ A).inv) x

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

Instances For

@[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

@[simp]

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

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

Instances For

@[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 : CategoryTheory.ToType (cycles A 2)) :

(LinearMap.ker (ModuleCat.Hom.hom (shortComplexH2 A).g)).subtype ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) x) = (CategoryTheory.CategoryStruct.comp (iCycles A 2) (chainsIso₂ A).hom) 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 : (inhomogeneousChains A).X 2 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (isoCycles₂ A).inv (CategoryTheory.CategoryStruct.comp (iCycles A 2) h) = CategoryTheory.CategoryStruct.comp (shortComplexH2 A).moduleCatLeftHomologyData.i (CategoryTheory.CategoryStruct.comp (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 : CategoryTheory.ToType (ModuleCat.of k ↥(cycles₂ A))) :

(CategoryTheory.ConcreteCategory.hom (iCycles A 2)) ((CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).inv) x) = (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 : CategoryTheory.ToType ((inhomogeneousChains A).X 3)) :

(CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).hom) ((CategoryTheory.ConcreteCategory.hom (toCycles A 3 2)) x) = (CategoryTheory.CategoryStruct.comp (chainsIso₃ A).hom (shortComplexH2 A).moduleCatLeftHomologyData.f') x

theorem groupHomology.cyclesMk₂_eq {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (x : ↥(cycles₂ A)) :

cyclesMk 2 1 ⋯ ((CategoryTheory.ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) ⋯ = (CategoryTheory.ConcreteCategory.hom (isoCycles₂ A).inv) x

@[reducible, inline]

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

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

Instances For

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

Instances For

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

A.V ⟶ H0 A

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

Equations

Instances For

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 : CategoryTheory.ToType (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.ToType ((Action.forget (ModuleCat k) G).obj A)) :

(CategoryTheory.ConcreteCategory.hom (H0Iso A).inv) ((Representation.Coinvariants.mk A.ρ) x) = (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 : CategoryTheory.ToType A.V) :

(CategoryTheory.ConcreteCategory.hom (H0Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (H0π A)) x) = ((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 : CategoryTheory.ToType (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.V), C ((CategoryTheory.ConcreteCategory.hom (H0π A)) x)) :

C x

def groupHomology.H0IsoOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :

H0 A ≅ A.V

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

Equations

Instances For

@[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 : A.V ⟶ 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 : CategoryTheory.ToType (cycles A 0)) :

(CategoryTheory.ConcreteCategory.hom (H0IsoOfIsTrivial A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 0)) x) = (CategoryTheory.ConcreteCategory.hom (cyclesIso₀ A).hom) x

@[reducible, inline]

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

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

Instances For

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

Instances For

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

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

Instances For

@[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 : CategoryTheory.ToType (cycles A 1)) :

(CategoryTheory.ConcreteCategory.hom (H1Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 1)) x) = Submodule.Quotient.mk ((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 : CategoryTheory.ToType (shortComplexH1 A).moduleCatLeftHomologyData.K) :

(CategoryTheory.ConcreteCategory.hom (H1Iso A).inv) (Submodule.Quotient.mk x) = (H1π A) x

def groupHomology.mkH1OfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :

Additive (Abelianization G) →ₗ[ℤ ] ↑A.V →ₗ[ℤ ] ↑(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

Instances For

@[simp]

theorem groupHomology.mkH1OfIsTrivial_apply {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (g : G) (a : ↑A.V) :

((mkH1OfIsTrivial A) (Additive.ofMul (Abelianization.of g))) a = (CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))

def groupHomology.H1ToTensorOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :

↑(H1 A) →ₗ[ℤ ] TensorProduct ℤ (Additive (Abelianization G)) ↑A.V

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

Instances For

@[simp]

theorem groupHomology.H1ToTensorOfIsTrivial_H1π_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} [A.IsTrivial] (g : G) (a : ↑A.V) :

(H1ToTensorOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom (H1π A)) ((CategoryTheory.ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (Finsupp.single g a))) = Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ ] a

def groupHomology.H1AddEquivOfIsTrivial {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] :

↑(H1 A) ≃+ TensorProduct ℤ (Additive (Abelianization G)) ↑A.V

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

Instances For

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.V) :

(H1AddEquivOfIsTrivial A).symm a✝ = (TensorProduct.lift (mkH1OfIsTrivial A)) a✝

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✝

@[simp]

theorem groupHomology.H1AddEquivOfIsTrivial_single {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [A.IsTrivial] (g : G) (a : ↑A.V) :

(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.V) :

(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]

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

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

Instances For

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

Instances For

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

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

Instances For

@[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 : CategoryTheory.ToType (cycles A 2)) :

(CategoryTheory.ConcreteCategory.hom (H2Iso A).hom) ((CategoryTheory.ConcreteCategory.hom (π A 2)) x) = Submodule.Quotient.mk ((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 : CategoryTheory.ToType (shortComplexH2 A).moduleCatLeftHomologyData.K) :

(CategoryTheory.ConcreteCategory.hom (H2Iso A).inv) (Submodule.Quotient.mk x) = (H2π A) x