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 RepresentationTheory/HomologicalComplex/GroupHomology/FiniteCyclic.lean, we use this resolution to compute the group homology 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 cohomology of representations of finite cyclic groups.

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

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

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

Equations

• Representation.FiniteCyclicGroup.coinvariantsEquiv ρ g hg = (Representation.Coinvariants.ker ρ).quotEquivOfEq (LinearMap.range (ρ g - LinearMap.id)) ⋯

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

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) : LinearMap.range (ModuleCat.Hom.hom (leftRegular k G).norm.hom) = LinearMap.ker (ModuleCat.Hom.hom ((leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (leftRegular k G)).hom)

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

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) : LinearMap.range (ModuleCat.Hom.hom ((leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (leftRegular k G)).hom) = LinearMap.ker (ModuleCat.Hom.hom (leftRegular k G).norm.hom)

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.

Equations

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

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

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

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

Equations

• Rep.FiniteCyclicGroup.normHomCompSub A g = { X₁ := A.V, X₂ := A.V, X₃ := A.V, f := A.norm.hom, g := (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom, zero := ⋯ }

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

Equations

• Rep.FiniteCyclicGroup.subCompNormHom A g = { X₁ := A.V, X₂ := A.V, X₃ := A.V, f := (A.applyAsHom g - CategoryTheory.CategoryStruct.id A).hom, g := A.norm.hom, zero := ⋯ }

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

Equations

• Rep.FiniteCyclicGroup.moduleCatChainComplex A g = HomologicalComplex.alternatingConst A.V ⋯ ⋯ ⋯

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

Equations

• Rep.FiniteCyclicGroup.moduleCatCochainComplex A g = HomologicalComplex.alternatingConst A.V ⋯ ⋯ ⋯

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.

Equations

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

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

Equations

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

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

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