Projective resolution of k as a trivial k-linear representation of a finite cyclic group

Let k be a commutative ring and G a finite commutative group. Given g : G and A : Rep k G, we can define a periodic chain complex in Rep k G given by ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0 where N is the norm map sending a : A to ∑ ρ(g)(a) for all g in G.

When G is generated by g and A is the left regular representation k[G], this chain complex is a projective resolution of k as a trivial representation, which we prove here.

In the file Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean, we use this resolution to compute the group cohomology of representations of finite cyclic groups.

Main definitions

• Rep.FiniteCyclicGroup.resolution k g hg: given a finite cyclic group G generated by g : G, this is the projective resolution of k as a trivial k-linear G-representation given by periodic complex ... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0 where ρ is the left regular representation and N is the norm map.

TODO

• Use this to analyse the group homology of representations of finite cyclic groups.

theorem Representation.FiniteCyclicGroup.coinvariantsKer_eq_range {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_4} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) [Finite G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : Coinvariants.ker ρ = (ρ g - LinearMap.id).range

noncomputable def Representation.FiniteCyclicGroup.coinvariantsEquiv {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_4} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) [Fintype G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : ρ.Coinvariants ≃ₗ[k] V ⧸ (ρ g - LinearMap.id).range

Given a finite cyclic group G generated by g and a G representation (V, ρ), V_G is isomorphic to V ⧸ Im(ρ(g - 1)).

theorem Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] [Finite G] : Coinvariants.ker (leftRegular k G) = (Finsupp.linearCombination k fun (x : G) => 1).ker

theorem Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (ModuleCat.Hom.hom (leftRegular k G).norm.hom).range = (ModuleCat.Hom.hom ((leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (leftRegular k G)).hom).ker

theorem Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination (k : Type u) {G : Type u} [CommRing k] [CommGroup G] (g : G) [Finite G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (ModuleCat.Hom.hom ((leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (leftRegular k G)).hom).range = (Finsupp.linearCombination k fun (x : G) => 1).ker

theorem Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (ModuleCat.Hom.hom ((leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (leftRegular k G)).hom).range = (ModuleCat.Hom.hom (leftRegular k G).norm.hom).ker

noncomputable def Rep.FiniteCyclicGroup.chainComplexFunctor (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) : CategoryTheory.Functor (Rep k G) (ChainComplex (Rep k G) ℕ)

Given a finite group G and g : G, this is the functor Rep k G ⥤ ChainComplex (Rep k G) ℕ sending A : Rep k G to the periodic chain complex in Rep k G given by ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0 where N is the norm map. When G is generated by g and A is the left regular representation k[G], it is a projective resolution of k as a trivial representation.

It sends a morphism f : A ⟶ B to the chain morphism defined by f in every degree.

@[simp]

theorem Rep.FiniteCyclicGroup.chainComplexFunctor_map_f (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) (i : ℕ) : ((chainComplexFunctor k g).map f).f i = f

@[simp]

theorem Rep.FiniteCyclicGroup.chainComplexFunctor_obj (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (A : Rep k G) : (chainComplexFunctor k g).obj A = HomologicalComplex.alternatingConst A ⋯ ⋯ ⋯

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.normHomCompSub {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) : CategoryTheory.ShortComplex (ModuleCat k)

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the short complex in ModuleCat k given by A --N--> A --(ρ(g) - 𝟙)--> A where N is the norm map. Its homology is Hⁱ(G, A) for even i and Hᵢ(G, A) for odd i.

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.subCompNormHom {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) : CategoryTheory.ShortComplex (ModuleCat k)

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the short complex in ModuleCat k given by A --N--> A --(ρ(g) - 𝟙)--> A where N is the norm map. Its homology is Hⁱ(G, A) for even i and Hᵢ(G, A) for odd i.

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.moduleCatChainComplex {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) : ChainComplex (ModuleCat k) ℕ

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the periodic chain complex in ModuleCat k given by ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0 where N is the norm map. Its homology is the group homology of A.

@[reducible, inline]

noncomputable abbrev Rep.FiniteCyclicGroup.moduleCatCochainComplex {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G) : CochainComplex (ModuleCat k) ℕ

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the periodic chain complex in Rep k G given by 0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ... where N is the norm map. Its cohomology is the group cohomology of A.

noncomputable def Rep.FiniteCyclicGroup.resolution.π (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) : (chainComplexFunctor k g).obj (leftRegular k G) ⟶ (ChainComplex.single₀ (Rep k G)).obj (trivial k G k)

Given a finite cyclic group G generated by g : G, let P denote the periodic chain complex of k-linear G-representations given by ... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0 where ρ is the left regular representation and N is the norm map. This is the chain morphism from P to the chain complex concentrated at 0 by the trivial representation k used to show P is a projective resolution of k. It sends x : k[G] to the sum of its coefficients.

@[simp]

theorem Rep.FiniteCyclicGroup.resolution.π_f (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (i : ℕ) : (π k g).f i = if hi : i = 0 then CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst (leftRegular k G) ⋯ ⋯ ⋯).XIsoOfEq hi).hom (CategoryTheory.CategoryStruct.comp ((trivial k G k).leftRegularHom 1) (HomologicalComplex.singleObjXIsoOfEq (ComplexShape.down ℕ) 0 (trivial k G k) i hi).inv) else 0

theorem Rep.FiniteCyclicGroup.resolution_quasiIso (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : QuasiIso (resolution.π k g)

noncomputable def Rep.FiniteCyclicGroup.resolution (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : CategoryTheory.ProjectiveResolution (trivial k G k)

Given a finite cyclic group G generated by g : G, this is the projective resolution of k as a trivial k-linear G-representation given by periodic complex ... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0 where ρ is the left regular representation and N is the norm map.

@[simp]

theorem Rep.FiniteCyclicGroup.resolution_π (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (resolution k g hg).π = resolution.π k g

@[simp]

theorem Rep.FiniteCyclicGroup.resolution_complex (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (resolution k g hg).complex = (chainComplexFunctor k g).obj (leftRegular k G)