From 5683185bee6799867b53e866c930b341ea627a75 Mon Sep 17 00:00:00 2001 From: Amelia Livingston <101damnations@github.com> Date: Mon, 1 Jan 2024 15:59:48 +0000 Subject: [PATCH] feat(RepresentationTheory/GroupCohomology/LowDegree): Identify `groupCohomology A n`with `Hn A` for `n = 0, 1, 2` (#8802) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Joël Riou --- .../GroupCohomology/Basic.lean | 19 ++ .../GroupCohomology/LowDegree.lean | 164 +++++++++++++++++- 2 files changed, 177 insertions(+), 6 deletions(-) diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean index c2e8043a3b16c..107b8481575ac 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean +++ b/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 : ℕ) : diff --git a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean index bd779ec3f2dce..3ef48ae74ca4d 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean +++ b/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