feat(RepresentationTheory/GroupCohomology/LowDegree): Identify `group…

…Cohomology A n`with `Hn A` for `n = 0, 1, 2` (#8802)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

@@ -220,6 +220,19 @@ def inhomogeneousCochainsIso : inhomogeneousCochains A ≅ linearYonedaObjResolu
     Category.comp_id]
 #align group_cohomology.inhomogeneous_cochains_iso groupCohomology.inhomogeneousCochainsIso
 
+/-- The `n`-cocycles `Zⁿ(G, A)` of a `k`-linear `G`-representation `A`, i.e. the kernel of the
+`n`th differential in the complex of inhomogeneous cochains. -/
+abbrev cocycles (n : ℕ) : ModuleCat k := (inhomogeneousCochains A).cycles n
+
+/-- The natural inclusion of the `n`-cocycles `Zⁿ(G, A)` into the `n`-cochains `Cⁿ(G, A).` -/
+abbrev iCocycles (n : ℕ) : cocycles A n ⟶ ModuleCat.of k ((Fin n → G) → A) :=
+  (inhomogeneousCochains A).iCycles n
+
+/-- This is the map from `i`-cochains to `j`-cocycles induced by the differential in the complex of
+inhomogeneous cochains. -/
+abbrev toCocycles (i j : ℕ) : ModuleCat.of k ((Fin i → G) → A) ⟶ cocycles A j :=
+  (inhomogeneousCochains A).toCycles i j
+
 end groupCohomology
 
 open groupCohomology
@@ -230,6 +243,12 @@ def groupCohomology [Group G] (A : Rep k G) (n : ℕ) : ModuleCat k :=
   (inhomogeneousCochains A).homology n
 #align group_cohomology groupCohomology
 
+/-- The natural map from `n`-cocycles to `n`th group cohomology for a `k`-linear
+`G`-representation `A`. -/
+abbrev groupCohomologyπ [Group G] (A : Rep k G) (n : ℕ) :
+    groupCohomology.cocycles A n ⟶ groupCohomology A n :=
+  (inhomogeneousCochains A).homologyπ n
+
 /-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
 `Extⁿ(k, A)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation. -/
 def groupCohomologyIsoExt [Group G] (A : Rep k G) (n : ℕ) :

Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2023 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Amelia Livingston
+Authors: Amelia Livingston, Joël Riou
 
 -/
+import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 import Mathlib.RepresentationTheory.GroupCohomology.Basic
 import Mathlib.RepresentationTheory.Invariants
 
@@ -20,9 +21,9 @@ cokernel, whereas the definitions here are explicit quotients of cocycles by cob
 
 We also show that when the representation on `A` is trivial, `H¹(G, A) ≃ Hom(G, A)`.
 
-Later this file will contain an identification between the definition in
-`RepresentationTheory.GroupCohomology.Basic`, `groupCohomology A n`, and the `Hn A` in this file,
-for `n = 0, 1, 2`.
+The file also contains an identification between the definitions in
+`RepresentationTheory.GroupCohomology.Basic`, `groupCohomology.cocycles A n` and
+`groupCohomology A n`, and the `nCocycles` and `Hn A` in this file, for `n = 0, 1, 2`.
 
 ## Main definitions
 
@@ -33,11 +34,11 @@ for `n = 0, 1, 2`.
 2-coboundaries (i.e. `B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))`).
 * `groupCohomology.H1LequivOfIsTrivial`: the isomorphism `H¹(G, A) ≃ Hom(G, A)` when  the
 representation on `A` is trivial.
+* `groupCohomology.isoHn` for `n = 0, 1, 2`: an isomorphism
+`groupCohomology A n ≅ groupCohomology.Hn A`.
 
 ## TODO
 
-* Identify `Hn A` as defined in this file with `groupCohomology A n` for `n = 0, 1, 2`.
-* Hilbert's theorem 90
 * The relationship between `H2` and group extensions
 * The inflation-restriction exact sequence
 * Nonabelian group cohomology
@@ -405,4 +406,155 @@ theorem H1LequivOfIsTrivial_comp_H1_π [A.IsTrivial] :
   rfl
 
 end H1
+section groupCohomologyIso
+open ShortComplex
+section H0
+
+lemma dZero_comp_H0_subtype : dZero A ∘ₗ (H0 A).subtype = 0 := by
+  ext ⟨x, hx⟩ g
+  replace hx := hx g
+  rw [← sub_eq_zero] at hx
+  exact hx
+
+/-- The (exact) short complex `A.ρ.invariants ⟶ A ⟶ (G → A)`. -/
+@[simps!]
+def shortComplexH0 : ShortComplex (ModuleCat k) :=
+  ShortComplex.moduleCatMk _ _ (dZero_comp_H0_subtype A)
+
+instance : Mono (shortComplexH0 A).f := by
+  rw [ModuleCat.mono_iff_injective]
+  apply Submodule.injective_subtype
+
+lemma shortComplexH0_exact : (shortComplexH0 A).Exact := by
+  rw [ShortComplex.moduleCat_exact_iff]
+  intro (x : A) (hx : dZero _ x = 0)
+  refine' ⟨⟨x, fun g => _⟩, rfl⟩
+  rw [← sub_eq_zero]
+  exact congr_fun hx g
+
+/-- The arrow `A --dZero--> Fun(G, A)` is isomorphic to the differential
+`(inhomogeneousCochains A).d 0 1` of the complex of inhomogeneous cochains of `A`. -/
+@[simps! hom_left hom_right inv_left inv_right]
+def dZeroArrowIso : Arrow.mk ((inhomogeneousCochains A).d 0 1) ≅
+    Arrow.mk (ModuleCat.ofHom (dZero A)) :=
+  Arrow.isoMk (zeroCochainsLequiv A).toModuleIso
+    (oneCochainsLequiv A).toModuleIso (dZero_comp_eq A)
+
+/-- The 0-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
+`A.ρ.invariants`, which is a simpler type. -/
+def isoZeroCocycles : cocycles A 0 ≅ ModuleCat.of k A.ρ.invariants :=
+  KernelFork.mapIsoOfIsLimit
+    ((inhomogeneousCochains A).cyclesIsKernel 0 1 (by simp)) (shortComplexH0_exact A).fIsKernel
+      (dZeroArrowIso A)
+
+lemma isoZeroCocycles_hom_comp_subtype :
+    (isoZeroCocycles A).hom ≫ A.ρ.invariants.subtype =
+      iCocycles A 0 ≫ (zeroCochainsLequiv A).toModuleIso.hom := by
+  dsimp [isoZeroCocycles]
+  apply KernelFork.mapOfIsLimit_ι
+
+/-- The 0th group cohomology of `A`, defined as the 0th cohomology of the complex of inhomogeneous
+cochains, is isomorphic to the invariants of the representation on `A`. -/
+def isoH0 : groupCohomology A 0 ≅ ModuleCat.of k (H0 A) :=
+  (CochainComplex.isoHomologyπ₀ _).symm ≪≫ isoZeroCocycles A
+
+lemma groupCohomologyπ_comp_isoH0_hom  :
+    groupCohomologyπ A 0 ≫ (isoH0 A).hom = (isoZeroCocycles A).hom := by
+  simp [isoH0]
+
+end H0
+section H1
+
+/-- The short complex `A --dZero--> Fun(G, A) --dOne--> Fun(G × G, A)`. -/
+def shortComplexH1 : ShortComplex (ModuleCat k) :=
+  moduleCatMk (dZero A) (dOne A) (dOne_comp_dZero A)
+
+/-- The short complex `A --dZero--> Fun(G, A) --dOne--> Fun(G × G, A)` is isomorphic to the 1st
+short complex associated to the complex of inhomogeneous cochains of `A`. -/
+@[simps! hom inv]
+def shortComplexH1Iso : (inhomogeneousCochains A).sc' 0 1 2 ≅ shortComplexH1 A :=
+    isoMk (zeroCochainsLequiv A).toModuleIso (oneCochainsLequiv A).toModuleIso
+      (twoCochainsLequiv A).toModuleIso (dZero_comp_eq A) (dOne_comp_eq A)
+
+/-- The 1-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
+`oneCocycles A`, which is a simpler type. -/
+def isoOneCocycles : cocycles A 1 ≅ ModuleCat.of k (oneCocycles A) :=
+  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+    cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso
+
+lemma isoOneCocycles_hom_comp_subtype :
+    (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
+      iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom := by
+  dsimp [isoOneCocycles]
+  rw [Category.assoc, Category.assoc]
+  erw [(shortComplexH1 A).moduleCatCyclesIso_hom_subtype]
+  rw [cyclesMap_i, HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc]
+
+lemma toCocycles_comp_isoOneCocycles_hom :
+    toCocycles A 0 1 ≫ (isoOneCocycles A).hom =
+      (zeroCochainsLequiv A).toModuleIso.hom ≫
+        ModuleCat.ofHom (shortComplexH1 A).moduleCatToCycles := by
+  simp [isoOneCocycles]
+  rfl
+
+/-- The 1st group cohomology of `A`, defined as the 1st cohomology of the complex of inhomogeneous
+cochains, is isomorphic to `oneCocycles A ⧸ oneCoboundaries A`, which is a simpler type. -/
+def isoH1 : groupCohomology A 1 ≅ ModuleCat.of k (H1 A) :=
+  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+    homologyMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatHomologyIso
+
+lemma groupCohomologyπ_comp_isoH1_hom  :
+    groupCohomologyπ A 1 ≫ (isoH1 A).hom =
+      (isoOneCocycles A).hom ≫ (shortComplexH1 A).moduleCatHomologyπ := by
+  simp [isoH1, isoOneCocycles]
+
+end H1
+section H2
+
+/-- The short complex `Fun(G, A) --dOne--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A)`. -/
+def shortComplexH2 : ShortComplex (ModuleCat k) :=
+  moduleCatMk (dOne A) (dTwo A) (dTwo_comp_dOne A)
+
+/-- The short complex `Fun(G, A) --dOne--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A)` is
+isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of `A`. -/
+@[simps! hom inv]
+def shortComplexH2Iso :
+    (inhomogeneousCochains A).sc' 1 2 3 ≅ shortComplexH2 A :=
+  isoMk (oneCochainsLequiv A).toModuleIso (twoCochainsLequiv A).toModuleIso
+    (threeCochainsLequiv A).toModuleIso (dOne_comp_eq A) (dTwo_comp_eq A)
+
+/-- The 2-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
+`twoCocycles A`, which is a simpler type. -/
+def isoTwoCocycles : cocycles A 2 ≅ ModuleCat.of k (twoCocycles A) :=
+  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+    cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso
+
+lemma isoTwoCocycles_hom_comp_subtype :
+    (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
+      iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom := by
+  dsimp [isoTwoCocycles]
+  rw [Category.assoc, Category.assoc]
+  erw [(shortComplexH2 A).moduleCatCyclesIso_hom_subtype]
+  rw [cyclesMap_i, HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc]
+
+lemma toCocycles_comp_isoTwoCocycles_hom :
+    toCocycles A 1 2 ≫ (isoTwoCocycles A).hom =
+      (oneCochainsLequiv A).toModuleIso.hom ≫
+        ModuleCat.ofHom (shortComplexH2 A).moduleCatToCycles := by
+  simp [isoTwoCocycles]
+  rfl
+
+/-- The 2nd group cohomology of `A`, defined as the 2nd cohomology of the complex of inhomogeneous
+cochains, is isomorphic to `twoCocycles A ⧸ twoCoboundaries A`, which is a simpler type. -/
+def isoH2 : groupCohomology A 2 ≅ ModuleCat.of k (H2 A) :=
+  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+    homologyMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatHomologyIso
+
+lemma groupCohomologyπ_comp_isoH2_hom  :
+    groupCohomologyπ A 2 ≫ (isoH2 A).hom =
+      (isoTwoCocycles A).hom ≫ (shortComplexH2 A).moduleCatHomologyπ := by
+  simp [isoH2, isoTwoCocycles]
+
+end H2
+end groupCohomologyIso
 end groupCohomology