Group cohomology 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 and by Cochains(A, φ, ψ) the periodic cochain complex 0 ⟶ A --ψ--> A --φ--> A --ψ--> A --φ--> A ⟶ ....

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, Hom(P, A) is isomorphic to Cochains(A, N, ρ_A(g) - Id) as a complex of k-modules, and hence the cohomology of this complex computes group cohomology.

Main definitions

• Rep.FiniteCyclicGroup.groupCohomologyIso₀ 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) ≅ Ker(ρ_A(g) - Id).
• Rep.FiniteCyclicGroup.groupCohomologyIsoOdd 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 odd i.
• Rep.FiniteCyclicGroup.groupCohomologyIsoEven 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 positive even i.

noncomputable def Rep.FiniteCyclicGroup.homResolutionIso {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (resolution k g hg).complex.linearYonedaObj k A ≅ moduleCatCochainComplex A g

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, the periodic cochain complex 0 ⟶ Hom(k[G], A) --(- ∘ (ρ(g) - 𝟙))--> Hom(k[G], A) --(- ∘ N)--> Hom(k[G], A) ⟶ ... is isomorphic as a complex in ModuleCat k to 0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ....

Equations

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

@[simp]

theorem Rep.FiniteCyclicGroup.homResolutionIso_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 : ℕ) (f : leftRegular k G ⟶ A) : (ModuleCat.Hom.hom ((homResolutionIso A g hg).hom.f i)) f = (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single 1 1)

@[simp]

theorem Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_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) (d : G →₀ k) : (ModuleCat.Hom.hom ((ModuleCat.Hom.hom ((homResolutionIso A g hg).inv.f i)) a).hom) d = d.sum fun (i : G) (c : k) => c • (A.ρ i) a

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupCohomologyIso₀ {k G : Type u} [CommRing k] [CommGroup G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupCohomology A 0 ≅ ModuleCat.of k ↥(LinearMap.ker (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 kernel of ρ(g) - Id(A).

Equations

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

noncomputable def Rep.FiniteCyclicGroup.groupCohomologyIsoEven {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) [DecidableEq G] (i : ℕ) [h₀ : NeZero i] (hi : Even i) : groupCohomology 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 nonzero and even.

Equations

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

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupCohomologyπEven {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) [DecidableEq G] (i : ℕ) [NeZero i] (hi : Even i) : ModuleCat.of k ↥(LinearMap.ker (ModuleCat.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom)) ⟶ groupCohomology 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 nonzero even i.

Equations

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

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

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

noncomputable def Rep.FiniteCyclicGroup.groupCohomologyIsoOdd {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) [DecidableEq G] (i : ℕ) (hi : Odd i) : groupCohomology 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 odd.

Equations

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

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.groupCohomologyπOdd {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) [DecidableEq G] (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(LinearMap.ker (ModuleCat.Hom.hom A.norm.hom)) ⟶ groupCohomology 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 odd i.

Equations

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

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

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