feat(RepresentationTheory/Homological): add standard resolution for finite cyclic groups (#27363)

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 in this PR.

Author: 101damnations

Mathlib.lean

@@ -5371,6 +5371,7 @@ import Mathlib.RepresentationTheory.GroupCohomology.Functoriality
 import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
 import Mathlib.RepresentationTheory.GroupCohomology.LowDegree
 import Mathlib.RepresentationTheory.GroupCohomology.Resolution
+import Mathlib.RepresentationTheory.Homological.FiniteCyclic
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean

@@ -0,0 +1,216 @@
+/-
+Copyright (c) 2025 Amelia Livingston. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Amelia Livingston
+-/
+import Mathlib.Algebra.Homology.AlternatingConst
+import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
+import Mathlib.CategoryTheory.Preadditive.Projective.Resolution
+import Mathlib.GroupTheory.OrderOfElement
+import Mathlib.RepresentationTheory.Coinvariants
+
+/-!
+# 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.
+
+## 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 (co)homology of representations of finite cyclic groups.
+
+-/
+
+universe v u
+
+open CategoryTheory Finsupp
+
+namespace Representation.FiniteCyclicGroup
+
+variable {k G V : Type*} [CommRing k] [Group G] [Fintype G] {V : Type*} [AddCommGroup V]
+  [Module k V] (ρ : Representation k G V) (g : G)
+
+lemma coinvariantsKer_eq_range (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    Coinvariants.ker ρ = LinearMap.range (ρ g - LinearMap.id) := by
+  refine le_antisymm (Submodule.span_le.2 ?_) ?_
+  · rintro a ⟨⟨γ, α⟩, rfl⟩
+    rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
+    induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
+    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
+    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
+  · rintro x ⟨y, rfl⟩
+    simpa using Coinvariants.sub_mem_ker g y
+
+/-- Given a finite cyclic group `G` generated by `g` and a `G` representation `(V, ρ)`, `V_G` is
+isomorphic to `V ⧸ Im(ρ(g - 1))`. -/
+noncomputable def coinvariantsEquiv (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    ρ.Coinvariants ≃ₗ[k] (_ ⧸ LinearMap.range (ρ g - LinearMap.id)) :=
+  Submodule.quotEquivOfEq _ _ (coinvariantsKer_eq_range ρ g hg)
+
+lemma coinvariantsKer_leftRegular_eq_ker :
+    Coinvariants.ker (Representation.leftRegular k G) =
+      LinearMap.ker (linearCombination k (fun _ => (1 : k))) := by
+  refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
+  · rintro x ⟨⟨g, y⟩, rfl⟩
+    simpa [linearCombination, sub_eq_zero, sum_fintype]
+      using Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by aesop) (by aesop)
+  · have : x = x.sum (fun g r => single g r - single 1 r) := by
+      ext g
+      by_cases hg : g = 1
+      · simp_all [linearCombination, sum_apply']
+      · simp_all [sum_apply']
+    rw [this]
+    exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
+      Coinvariants.mem_ker_of_eq g (single 1 (x g)) _ (by simp)
+
+end Representation.FiniteCyclicGroup
+
+namespace Rep.FiniteCyclicGroup
+
+variable (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G)
+
+namespace leftRegular
+
+open Finsupp IsCyclic Representation
+
+lemma range_norm_eq_ker_applyAsHom_sub (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    LinearMap.range (leftRegular k G).norm.hom.hom =
+      LinearMap.ker (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom :=
+  le_antisymm (fun _ ⟨_, h⟩ => by simp_all [← h]) fun x hx => ⟨single 1 (x g), by
+    ext j; simpa [Representation.norm] using (apply_eq_of_leftRegular_eq_of_generator g hg _
+      (by simpa [sub_eq_zero] using hx) j).symm⟩
+
+lemma range_applyAsHom_sub_eq_ker_linearCombination (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    LinearMap.range (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom =
+      LinearMap.ker (linearCombination k (fun _ => (1 : k))) := by
+  simp [← FiniteCyclicGroup.coinvariantsKer_eq_range _ _ hg,
+    ← FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker]
+
+lemma range_applyAsHom_sub_eq_ker_norm (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    LinearMap.range (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom =
+      LinearMap.ker (leftRegular k G).norm.hom.hom := by
+  simp [ker_leftRegular_norm_eq, ← range_applyAsHom_sub_eq_ker_linearCombination k g hg]
+
+end leftRegular
+
+/-- 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. -/
+@[simps]
+noncomputable def chainComplexFunctor : Rep k G ⥤ ChainComplex (Rep k G) ℕ where
+  obj A := HomologicalComplex.alternatingConst A (φ := A.norm) (ψ := applyAsHom A g - 𝟙 A)
+    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.down_nat_odd_add
+  map f := {
+    f i := f
+    comm' := by
+      rintro i j ⟨rfl⟩
+      by_cases hj : Even (j + 1)
+      · simp [if_pos hj, norm_comm]
+      · simp [if_neg hj, applyAsHom_comm] }
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+variable {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`. -/
+noncomputable abbrev normHomCompSub : ShortComplex (ModuleCat k) :=
+  ShortComplex.mk A.norm.hom (applyAsHom A g - 𝟙 A).hom (by ext; simp)
+
+/-- 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`. -/
+noncomputable abbrev subCompNormHom : ShortComplex (ModuleCat k) :=
+  ShortComplex.mk (applyAsHom A g - 𝟙 A).hom A.norm.hom (by ext; simp)
+
+/-- 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`. -/
+noncomputable abbrev moduleCatChainComplex : ChainComplex (ModuleCat k) ℕ :=
+  HomologicalComplex.alternatingConst A.V (φ := A.norm.hom) (ψ := (applyAsHom A g - 𝟙 A).hom)
+    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.down_nat_odd_add
+
+/-- 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 abbrev moduleCatCochainComplex : CochainComplex (ModuleCat k) ℕ :=
+  HomologicalComplex.alternatingConst A.V (φ := (applyAsHom A g - 𝟙 A).hom) (ψ := A.norm.hom)
+    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.up_nat_odd_add
+
+variable (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. -/
+@[simps!]
+noncomputable def resolution.π (g : G) :
+    (chainComplexFunctor k g).obj (leftRegular k G) ⟶
+      (ChainComplex.single₀ (Rep k G)).obj (trivial k G k) :=
+  (((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv _).symm
+    ⟨leftRegularHom _ 1, (leftRegularHomEquiv _).injective <| by simp [leftRegularHomEquiv]⟩
+
+lemma resolution_quasiIso (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    QuasiIso (resolution.π k g) where
+  quasiIsoAt m := by
+    induction m with
+    | zero =>
+      simp only [resolution.π]
+      rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]
+      constructor
+      · apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
+        simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
+          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using
+          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg
+      · rw [Rep.epi_iff_surjective]
+        intro x
+        use single 1 x
+        simp [ChainComplex.toSingle₀Equiv]
+    | succ m _ =>
+      rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
+          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
+      apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
+      rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
+      by_cases hm : Odd (m + 1)
+      · simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
+          if_neg (Nat.not_even_iff_odd.2 hm)]
+          using leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg
+      · simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
+          if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)]
+        using leftRegular.range_applyAsHom_sub_eq_ker_norm 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. -/
+@[simps]
+noncomputable def resolution (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
+    ProjectiveResolution (trivial k G k) where
+  complex := (FiniteCyclicGroup.chainComplexFunctor k g).obj (leftRegular k G)
+  projective _ := inferInstanceAs <| Projective (leftRegular k G)
+  π := FiniteCyclicGroup.resolution.π k g
+  quasiIso := resolution_quasiIso k g hg
+
+end Rep.FiniteCyclicGroup

Mathlib/RepresentationTheory/Invariants.lean

@@ -85,6 +85,14 @@ theorem invariants_eq_top [ρ.IsTrivial] :
     invariants ρ = ⊤ :=
 eq_top_iff.2 (fun x _ g => ρ.isTrivial_apply g x)
 
+lemma mem_invariants_iff_of_forall_mem_zpowers
+    (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) (x : V) :
+    x ∈ ρ.invariants ↔ ρ g x = x :=
+  ⟨fun h => h g, fun hx γ => by
+    rcases hg γ with ⟨i, rfl⟩
+    induction i with | zero => simp | succ i _ => simp_all [zpow_add_one] | pred i h => _
+    simpa [neg_sub_comm _ (1 : ℤ), zpow_sub] using congr(ρ g⁻¹ $(h.trans hx.symm))⟩
+
 section
 
 variable [Fintype G] [Invertible (Fintype.card G : k)]