Group homology of a finite cyclic group

Let k be a commutative ring, G a group and A a k-linear G-representation. Given endomorphisms φ, ψ : A ⟶ A such that φ ∘ ψ = ψ ∘ φ = 0, denote by Chains(A, φ, ψ) the periodic chain complex ... ⟶ A --φ--> A --ψ--> A --φ--> A --ψ--> A ⟶ 0.

When G is finite and generated by g : G, then P := Chains(k[G], N, ρ(g) - Id) (with ρ the left regular representation) is a projective resolution of k as a trivial representation. In this file we show that for A : Rep k G, (A ⊗ P)_G is isomorphic to Chains(A, N, ρ_A(g) - Id) as a complex of k-modules, and hence the homology of this complex computes group homology.

Main definitions

• Rep.FiniteCyclicGroup.groupHomologyIso₀ A g hg: given a finite cyclic group G generated by g, and a representation A : Rep k G, this is an isomorphism H₀(G, A) ≅ Coker(ρ_A(g) - Id).
• Rep.FiniteCyclicGroup.groupHomologyIsoOdd A g hg i hi: given a finite cyclic group G generated by g, and a representation A : Rep k G, this is an isomorphism between Hᵢ(G, A) and the homology of A --N--> A --(ρ(g) - Id)--> A for all odd i.
• Rep.FiniteCyclicGroup.groupHomologyIsoEven A g hg i hi: given a finite cyclic group G generated by g, and a representation A : Rep k G, this is an isomorphism between Hᵢ(G, A) and the homology of A --(ρ(g) - Id)--> A --N--> A for all positive even i.

noncomputable def Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : HomologicalComplex.coinvariantsTensorObj A (resolution k g⁻¹ ⋯).complex ≅ moduleCatChainComplex A g

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, the period chain complex ... ⟶ (A ⊗ₖ k[G])_G --⟦Id ⊗ N⟧--> (A ⊗ₖ k[G])_G --⟦Id ⊗ (ρ(g⁻¹) - 𝟙)⟧--> (A ⊗ₖ k[G])_G ⟶ 0 is isomorphic as a complex in ModuleCat k to ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0.

Equations

• Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso A g hg = HomologicalComplex.Hom.isoOfComponents (fun (x : ℕ) => A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) ⋯

@[simp]

theorem Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a✝ : TensorProduct k (↑A.V) (G →₀ k) ⧸ (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup) : (ModuleCat.Hom.hom ((coinvariantsTensorResolutionIso A g hg).hom.f i)) a✝ = (QuotientAddGroup.lift (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup (TensorProduct.lift (Finsupp.linearCombination k fun (g : G) => A.ρ g⁻¹) ∘ₗ ↑(TensorProduct.comm k (↑A.V) (G →₀ k))).toAddMonoidHom ⋯) a✝

@[simp]

theorem Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a : ↑A.V) : (ModuleCat.Hom.hom ((coinvariantsTensorResolutionIso A g hg).inv.f i)) a = ((↑A.ρ.coinvariantsTprodLeftRegularLEquiv).inverse ⇑A.ρ.coinvariantsTprodLeftRegularLEquiv.symm ⋯ ⋯) a

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupHomologyIso₀ {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupHomology A 0 ≅ ModuleCat.of k (↑A.V ⧸ LinearMap.range (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom))

Given a finite cyclic group G generated by g and A : Rep k G, H₀(G, A) is isomorphic to the cokernel of ρ(g) - Id(A).

Equations

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

noncomputable def Rep.FiniteCyclicGroup.groupHomologyIsoEven {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i) : groupHomology A i ≅ (subCompNormHom A g).homology

Given a finite cyclic group G generated by g and A : Rep k G, Hᵢ(G, A) is isomorphic to the homology of the short complex of k-modules A --(ρ(g) - 𝟙)--> A --N--> A when i is nonzero and even.

Equations

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

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupHomologyπEven {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) : ModuleCat.of k ↥(LinearMap.ker A.ρ.norm) ⟶ groupHomology A i

Given a finite cyclic group G generated by g and A : Rep k G, this is the quotient map Ker(N) ⟶ Ker(N)/Im(ρ(g) - Id(A)) ≅ Hᵢ(G, A) for any nonzero even i.

Equations

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

theorem Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom)

theorem Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x y : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) y ↔ ↑x - ↑y ∈ LinearMap.range (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom)

noncomputable def Rep.FiniteCyclicGroup.groupHomologyIsoOdd {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : groupHomology A i ≅ (normHomCompSub A g).homology

Given a finite cyclic group G generated by g and A : Rep k G, Hⁱ(G, A) is isomorphic to the homology of the short complex of k-modules A --N--> A --(ρ(g) - 𝟙)--> A when i is odd.

Equations

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

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupHomologyπOdd {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(LinearMap.ker (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom)) ⟶ groupHomology A i

Given a finite cyclic group G generated by g and A : Rep k G, this is the quotient map Ker(ρ(g) - Id(A)) ⟶ Ker(ρ(g) - Id(A))/Im(N) ≅ Hᵢ(G, A) for any odd i.

Equations

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

theorem Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(LinearMap.ker (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom))) : (CategoryTheory.ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range A.ρ.norm

theorem Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] [DecidableEq G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (A : Rep k G) (i : ℕ) (hi : Odd i) (x y : ↥(LinearMap.ker (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom))) : (CategoryTheory.ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) y ↔ ↑x - ↑y ∈ LinearMap.range A.ρ.norm