refactor(RepresentationTheory/GroupCohomology/LowDegree): make nCoboundaries a submodule of the n-cochains rather than the nCocycles for n = 0, 1, 2 (#22047)

Author: 101damnations

Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

@@ -105,7 +105,7 @@ noncomputable instance H1ofAutOnUnitsUnique : Unique (H1 (Rep.ofAlgebraAutOnUnit
   uniq := fun a => Quotient.inductionOn' a fun x => (H1π_eq_zero_iff _).2 <| by
     refine (oneCoboundariesOfIsMulOneCoboundary ?_).2
     rcases isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units x.1
-      (isMulOneCocycle_of_oneCocycles x) with ⟨β, hβ⟩
+      (isMulOneCocycle_of_mem_oneCocycles _ x.2) with ⟨β, hβ⟩
     use β
 
 end groupCohomology

Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

@@ -276,6 +276,10 @@ theorem mem_oneCocycles_iff (f : G → A) :
   rw [← add_eq_zero_iff_eq_neg, ← oneCocycles_map_one f, ← mul_inv_cancel g,
     (mem_oneCocycles_iff f).1 f.2 g g⁻¹]
 
+theorem dZero_apply_mem_oneCocycles (x : A) :
+    dZero A x ∈ oneCocycles A :=
+  congr($(dOne_comp_dZero A) x)
+
 theorem oneCocycles_map_mul_of_isTrivial [A.IsTrivial] (f : oneCocycles A) (g h : G) :
     f (g * h) = f g + f h := by
   rw [(mem_oneCocycles_iff f).1 f.2, apply_eq_self A.ρ g (f h), add_comm]
@@ -351,84 +355,85 @@ lemma twoCocycles_ρ_map_inv_sub_map_inv (f : twoCocycles A) (g : G) :
     at this
   exact sub_eq_sub_iff_add_eq_add.2 this.symm
 
+theorem dOne_apply_mem_twoCocycles (x : G → A) :
+    dOne A x ∈ twoCocycles A :=
+  congr($(dTwo_comp_dOne A) x)
+
 end Cocycles
 
 section Coboundaries
 
 /-- The 1-coboundaries `B¹(G, A)` of `A : Rep k G`, defined as the image of the map
 `A → Fun(G, A)` sending `(a, g) ↦ ρ_A(g)(a) - a.` -/
-def oneCoboundaries : Submodule k (oneCocycles A) :=
-  LinearMap.range ((dZero A).codRestrict (oneCocycles A) fun c =>
-    LinearMap.ext_iff.1 (dOne_comp_dZero A) c)
+def oneCoboundaries : Submodule k (G → A) :=
+  LinearMap.range (dZero A)
 
 /-- The 2-coboundaries `B²(G, A)` of `A : Rep k G`, defined as the image of the map
 `Fun(G, A) → Fun(G × G, A)` sending `(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).` -/
-def twoCoboundaries : Submodule k (twoCocycles A) :=
-  LinearMap.range ((dOne A).codRestrict (twoCocycles A) fun c =>
-    LinearMap.ext_iff.1 (dTwo_comp_dOne.{u} A) c)
+def twoCoboundaries : Submodule k (G × G → A) :=
+  LinearMap.range (dOne A)
 
 variable {A}
 
-/-- Makes a 1-coboundary out of `f ∈ Im(d⁰)`. -/
-def oneCoboundariesOfMemRange {f : G → A} (h : f ∈ LinearMap.range (dZero A)) :
-    oneCoboundaries A :=
-  ⟨⟨f, LinearMap.range_le_ker_iff.2 (dOne_comp_dZero A) h⟩,
-    by rcases h with ⟨x, rfl⟩; exact ⟨x, rfl⟩⟩
+instance : FunLike (oneCoboundaries A) G A := ⟨Subtype.val, Subtype.val_injective⟩
 
-theorem oneCoboundaries_of_mem_range_apply {f : G → A} (h : f ∈ LinearMap.range (dZero A)) :
-    (oneCoboundariesOfMemRange h).1.1 = f := rfl
+@[simp]
+theorem oneCoboundaries.coe_mk (f : G → A) (hf) :
+    ((⟨f, hf⟩ : oneCoboundaries A) : G → A) = f := rfl
 
-/-- Makes a 1-coboundary out of `f : G → A` and `x` such that
-`ρ(g)(x) - x = f(g)` for all `g : G`. -/
-def oneCoboundariesOfEq {f : G → A} {x : A} (hf : ∀ g, A.ρ g x - x = f g) :
-    oneCoboundaries A :=
-  oneCoboundariesOfMemRange ⟨x, funext hf⟩
+@[simp]
+theorem oneCoboundaries.val_eq_coe (f : oneCoboundaries A) : f.1 = f := rfl
 
-theorem oneCoboundariesOfEq_apply {f : G → A} {x : A} (hf : ∀ g, A.ρ g x - x = f g) :
-    (oneCoboundariesOfEq hf).1.1 = f := rfl
+@[ext]
+theorem oneCoboundaries_ext {f₁ f₂ : oneCoboundaries A} (h : ∀ g : G, f₁ g = f₂ g) : f₁ = f₂ :=
+  DFunLike.ext f₁ f₂ h
 
-theorem mem_range_of_mem_oneCoboundaries {f : oneCocycles A} (h : f ∈ oneCoboundaries A) :
-    f.1 ∈ LinearMap.range (dZero A) := by
-  rcases h with ⟨x, rfl⟩; exact ⟨x, rfl⟩
+variable (A) in
+lemma oneCoboundaries_le_oneCocycles : oneCoboundaries A ≤ oneCocycles A := by
+  rintro _ ⟨x, rfl⟩
+  exact dZero_apply_mem_oneCocycles x
+
+variable (A) in
+/-- Natural inclusion `B¹(G, A) →ₗ[k] Z¹(G, A)`. -/
+abbrev oneCoboundariesToOneCocycles : oneCoboundaries A →ₗ[k] oneCocycles A :=
+  Submodule.inclusion (oneCoboundaries_le_oneCocycles A)
+
+@[simp]
+lemma oneCoboundariesToOneCocycles_apply (x : oneCoboundaries A) :
+    oneCoboundariesToOneCocycles A x = x.1 := rfl
 
 theorem oneCoboundaries_eq_bot_of_isTrivial (A : Rep k G) [A.IsTrivial] :
     oneCoboundaries A = ⊥ := by
   simp_rw [oneCoboundaries, dZero_eq_zero]
   exact LinearMap.range_eq_bot.2 rfl
 
-theorem mem_oneCoboundaries_iff (f : oneCocycles A) : f ∈ oneCoboundaries A ↔
-    ∃ x : A, ∀ g : G, A.ρ g x - x = f g := exists_congr fun x ↦ by
-  simpa only [LinearMap.codRestrict, dZero, LinearMap.coe_mk, AddHom.coe_mk] using
-    groupCohomology.oneCocycles_ext_iff
+instance : FunLike (twoCoboundaries A) (G × G) A := ⟨Subtype.val, Subtype.val_injective⟩
 
-/-- Makes a 2-coboundary out of `f ∈ Im(d¹)`. -/
-def twoCoboundariesOfMemRange {f : G × G → A} (h : f ∈ LinearMap.range (dOne A)) :
-    twoCoboundaries A :=
-  ⟨⟨f, LinearMap.range_le_ker_iff.2 (dTwo_comp_dOne A) h⟩,
-    by rcases h with ⟨x, rfl⟩; exact ⟨x, rfl⟩⟩
+@[simp]
+theorem twoCoboundaries.coe_mk (f : G × G → A) (hf) :
+    ((⟨f, hf⟩ : twoCoboundaries A) : G × G → A) = f := rfl
 
-theorem twoCoboundariesOfMemRange_apply {f : G × G → A} (h : f ∈ LinearMap.range (dOne A)) :
-    (twoCoboundariesOfMemRange h).1.1 = f := rfl
+@[simp]
+theorem twoCoboundaries.val_eq_coe (f : twoCoboundaries A) : f.1 = f := rfl
 
-/-- Makes a 2-coboundary out of `f : G × G → A` and `x : G → A` such that
-`ρ(g)(x(h)) - x(gh) + x(g) = f(g, h)` for all `g, h : G`. -/
-def twoCoboundariesOfEq {f : G × G → A} {x : G → A}
-    (hf : ∀ g h, A.ρ g (x h) - x (g * h) + x g = f (g, h)) :
-    twoCoboundaries A :=
-  twoCoboundariesOfMemRange ⟨x, funext fun g ↦ hf g.1 g.2⟩
+@[ext]
+theorem twoCoboundaries_ext {f₁ f₂ : twoCoboundaries A} (h : ∀ g h : G, f₁ (g, h) = f₂ (g, h)) :
+    f₁ = f₂ :=
+  DFunLike.ext f₁ f₂ (Prod.forall.mpr h)
 
-theorem twoCoboundariesOfEq_apply {f : G × G → A} {x : G → A}
-    (hf : ∀ g h, A.ρ g (x h) - x (g * h) + x g = f (g, h)) :
-    (twoCoboundariesOfEq hf).1.1 = f := rfl
+variable (A) in
+lemma twoCoboundaries_le_twoCocycles : twoCoboundaries A ≤ twoCocycles A := by
+  rintro _ ⟨x, rfl⟩
+  exact dOne_apply_mem_twoCocycles x
 
-theorem mem_range_of_mem_twoCoboundaries {f : twoCocycles A} (h : f ∈ twoCoboundaries A) :
-    (twoCocycles A).subtype f ∈ LinearMap.range (dOne A) := by
-  rcases h with ⟨x, rfl⟩; exact ⟨x, rfl⟩
+variable (A) in
+/-- Natural inclusion `B²(G, A) →ₗ[k] Z²(G, A)`. -/
+abbrev twoCoboundariesToTwoCocycles : twoCoboundaries A →ₗ[k] twoCocycles A :=
+  Submodule.inclusion (twoCoboundaries_le_twoCocycles A)
 
-theorem mem_twoCoboundaries_iff (f : twoCocycles A) : f ∈ twoCoboundaries A ↔
-    ∃ x : G → A, ∀ g h : G, A.ρ g (x h) - x (g * h) + x g = f (g, h) := exists_congr fun x ↦ by
-  simpa only [LinearMap.codRestrict, dOne, LinearMap.coe_mk, AddHom.coe_mk] using
-    groupCohomology.twoCocycles_ext_iff
+@[simp]
+lemma twoCoboundariesToTwoCocycles_apply (x : twoCoboundaries A) :
+    twoCoboundariesToTwoCocycles A x = x.1 := rfl
 
 end Coboundaries
 
@@ -508,46 +513,55 @@ variable {k G A : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A]
 /-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
 `f : G → A` satisfying the 1-cocycle condition, produces a 1-cocycle for the representation on
 `A` induced by the `DistribMulAction`. -/
+@[simps]
 def oneCocyclesOfIsOneCocycle {f : G → A} (hf : IsOneCocycle f) :
     oneCocycles (Rep.ofDistribMulAction k G A) :=
   ⟨f, (mem_oneCocycles_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩
 
-theorem isOneCocycle_of_oneCocycles (f : oneCocycles (Rep.ofDistribMulAction k G A)) :
-    IsOneCocycle (A := A) f := (mem_oneCocycles_iff f).1 f.2
+theorem isOneCocycle_of_mem_oneCocycles
+    (f : G → A) (hf : f ∈ oneCocycles (Rep.ofDistribMulAction k G A)) :
+    IsOneCocycle f :=
+  fun _ _ => (mem_oneCocycles_iff (A := Rep.ofDistribMulAction k G A) f).1 hf _ _
 
 /-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
 `f : G → A` satisfying the 1-coboundary condition, produces a 1-coboundary for the representation
 on `A` induced by the `DistribMulAction`. -/
+@[simps]
 def oneCoboundariesOfIsOneCoboundary {f : G → A} (hf : IsOneCoboundary f) :
     oneCoboundaries (Rep.ofDistribMulAction k G A) :=
-  oneCoboundariesOfMemRange ⟨hf.choose, funext hf.choose_spec⟩
+  ⟨f, hf.choose, funext hf.choose_spec⟩
 
-theorem isOneCoboundary_of_oneCoboundaries (f : oneCoboundaries (Rep.ofDistribMulAction k G A)) :
-    IsOneCoboundary (A := A) f.1.1 := by
-  rcases mem_range_of_mem_oneCoboundaries f.2 with ⟨x, hx⟩
-  exact ⟨x, by rw [← hx]; intro g; rfl⟩
+theorem isOneCoboundary_of_mem_oneCoboundaries
+    (f : G → A) (hf : f ∈ oneCoboundaries (Rep.ofDistribMulAction k G A)) :
+    IsOneCoboundary f := by
+  rcases hf with ⟨a, rfl⟩
+  exact ⟨a, fun _ => rfl⟩
 
 /-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
 `f : G × G → A` satisfying the 2-cocycle condition, produces a 2-cocycle for the representation on
 `A` induced by the `DistribMulAction`. -/
+@[simps]
 def twoCocyclesOfIsTwoCocycle {f : G × G → A} (hf : IsTwoCocycle f) :
     twoCocycles (Rep.ofDistribMulAction k G A) :=
   ⟨f, (mem_twoCocycles_iff (A := Rep.ofDistribMulAction k G A) f).2 hf⟩
 
-theorem isTwoCocycle_of_twoCocycles (f : twoCocycles (Rep.ofDistribMulAction k G A)) :
-    IsTwoCocycle (A := A) f := (mem_twoCocycles_iff f).1 f.2
+theorem isTwoCocycle_of_mem_twoCocycles
+    (f : G × G → A) (hf : f ∈ twoCocycles (Rep.ofDistribMulAction k G A)) :
+    IsTwoCocycle f := (mem_twoCocycles_iff (A := Rep.ofDistribMulAction k G A) f).1 hf
 
 /-- Given a `k`-module `A` with a compatible `DistribMulAction` of `G`, and a function
 `f : G × G → A` satisfying the 2-coboundary condition, produces a 2-coboundary for the
 representation on `A` induced by the `DistribMulAction`. -/
+@[simps]
 def twoCoboundariesOfIsTwoCoboundary {f : G × G → A} (hf : IsTwoCoboundary f) :
     twoCoboundaries (Rep.ofDistribMulAction k G A) :=
-  twoCoboundariesOfMemRange (⟨hf.choose,funext fun g ↦ hf.choose_spec g.1 g.2⟩)
+  ⟨f, hf.choose,funext fun g ↦ hf.choose_spec g.1 g.2⟩
 
-theorem isTwoCoboundary_of_twoCoboundaries (f : twoCoboundaries (Rep.ofDistribMulAction k G A)) :
-    IsTwoCoboundary (A := A) f.1.1 := by
-  rcases mem_range_of_mem_twoCoboundaries f.2 with ⟨x, hx⟩
-  exact ⟨x, fun g h => funext_iff.1 hx (g, h)⟩
+theorem isTwoCoboundary_of_mem_twoCoboundaries
+    (f : G × G → A) (hf : f ∈ twoCoboundaries (Rep.ofDistribMulAction k G A)) :
+    IsTwoCoboundary f := by
+  rcases hf with ⟨a, rfl⟩
+  exact ⟨a, fun _ _ => rfl⟩
 
 end ofDistribMulAction
 
@@ -631,48 +645,55 @@ variable {G M : Type} [Group G] [CommGroup M] [MulDistribMulAction G M]
 /-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
 `f : G → M` satisfying the multiplicative 1-cocycle condition, produces a 1-cocycle for the
 representation on `Additive M` induced by the `MulDistribMulAction`. -/
+@[simps]
 def oneCocyclesOfIsMulOneCocycle {f : G → M} (hf : IsMulOneCocycle f) :
     oneCocycles (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, (mem_oneCocycles_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩
 
-theorem isMulOneCocycle_of_oneCocycles (f : oneCocycles (Rep.ofMulDistribMulAction G M)) :
-    IsMulOneCocycle (M := M) (Additive.toMul ∘ f) := (mem_oneCocycles_iff f).1 f.2
+theorem isMulOneCocycle_of_mem_oneCocycles
+    (f : G → M) (hf : f ∈ oneCocycles (Rep.ofMulDistribMulAction G M)) :
+    IsMulOneCocycle (Additive.toMul ∘ f) :=
+  (mem_oneCocycles_iff (A := Rep.ofMulDistribMulAction G M) f).1 hf
 
 /-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
 `f : G → M` satisfying the multiplicative 1-coboundary condition, produces a
 1-coboundary for the representation on `Additive M` induced by the `MulDistribMulAction`. -/
+@[simps]
 def oneCoboundariesOfIsMulOneCoboundary {f : G → M} (hf : IsMulOneCoboundary f) :
     oneCoboundaries (Rep.ofMulDistribMulAction G M) :=
-  oneCoboundariesOfMemRange (f := Additive.ofMul ∘ f) ⟨hf.choose, funext hf.choose_spec⟩
+  ⟨f, hf.choose, funext hf.choose_spec⟩
 
-theorem isMulOneCoboundary_of_oneCoboundaries
-    (f : oneCoboundaries (Rep.ofMulDistribMulAction G M)) :
-    IsMulOneCoboundary (M := M) (Additive.ofMul ∘ f.1.1) := by
-  rcases mem_range_of_mem_oneCoboundaries f.2 with ⟨x, hx⟩
-  exact ⟨x, by rw [← hx]; intro g; rfl⟩
+theorem isMulOneCoboundary_of_mem_oneCoboundaries
+    (f : G → M) (hf : f ∈ oneCoboundaries (Rep.ofMulDistribMulAction G M)) :
+    IsMulOneCoboundary (M := M) (Additive.ofMul ∘ f) := by
+  rcases hf with ⟨x, rfl⟩
+  exact ⟨x, fun _ =>  rfl⟩
 
 /-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
 `f : G × G → M` satisfying the multiplicative 2-cocycle condition, produces a 2-cocycle for the
 representation on `Additive M` induced by the `MulDistribMulAction`. -/
+@[simps]
 def twoCocyclesOfIsMulTwoCocycle {f : G × G → M} (hf : IsMulTwoCocycle f) :
     twoCocycles (Rep.ofMulDistribMulAction G M) :=
   ⟨Additive.ofMul ∘ f, (mem_twoCocycles_iff (A := Rep.ofMulDistribMulAction G M) f).2 hf⟩
 
-theorem isMulTwoCocycle_of_twoCocycles (f : twoCocycles (Rep.ofMulDistribMulAction G M)) :
-    IsMulTwoCocycle (M := M) (Additive.toMul ∘ f) := (mem_twoCocycles_iff f).1 f.2
+theorem isMulTwoCocycle_of_mem_twoCocycles
+    (f : G × G → M) (hf : f ∈ twoCocycles (Rep.ofMulDistribMulAction G M)) :
+    IsMulTwoCocycle (Additive.toMul ∘ f) :=
+  (mem_twoCocycles_iff (A := Rep.ofMulDistribMulAction G M) f).1 hf
 
 /-- Given an abelian group `M` with a `MulDistribMulAction` of `G`, and a function
 `f : G × G → M` satisfying the multiplicative 2-coboundary condition, produces a
 2-coboundary for the representation on `M` induced by the `MulDistribMulAction`. -/
 def twoCoboundariesOfIsMulTwoCoboundary {f : G × G → M} (hf : IsMulTwoCoboundary f) :
     twoCoboundaries (Rep.ofMulDistribMulAction G M) :=
-  twoCoboundariesOfMemRange ⟨hf.choose, funext fun g ↦ hf.choose_spec g.1 g.2⟩
+  ⟨f, hf.choose, funext fun g ↦ hf.choose_spec g.1 g.2⟩
 
-theorem isMulTwoCoboundary_of_twoCoboundaries
-    (f : twoCoboundaries (Rep.ofMulDistribMulAction G M)) :
-    IsMulTwoCoboundary (M := M) (Additive.toMul ∘ f.1.1) := by
-  rcases mem_range_of_mem_twoCoboundaries f.2 with ⟨x, hx⟩
-  exact ⟨x, fun g h => funext_iff.1 hx (g, h)⟩
+theorem isMulTwoCoboundary_of_mem_twoCoboundaries
+    (f : G × G → M) (hf : f ∈ twoCoboundaries (Rep.ofMulDistribMulAction G M)) :
+    IsMulTwoCoboundary (M := M) (Additive.toMul ∘ f) := by
+  rcases hf with ⟨x, rfl⟩
+  exact ⟨x, fun _ _ => rfl⟩
 
 end ofMulDistribMulAction
 
@@ -691,8 +712,9 @@ abbrev H1 := (shortComplexH1 A).moduleCatHomology
 abbrev H1π : ModuleCat.of k (oneCocycles A) ⟶ H1 A := (shortComplexH1 A).moduleCatHomologyπ
 
 variable {A} in
-lemma H1π_eq_zero_iff (x : oneCocycles A) : H1π A x = 0 ↔ x ∈ oneCoboundaries A :=
-  Submodule.Quotient.mk_eq_zero _
+lemma H1π_eq_zero_iff (x : oneCocycles A) : H1π A x = 0 ↔ ⇑x ∈ oneCoboundaries A := by
+  show (LinearMap.range ((dZero A).codRestrict (oneCocycles A) _)).mkQ _ = 0 ↔ _
+  simp [LinearMap.range_codRestrict, oneCoboundaries]
 
 /-- We define the 2nd group cohomology of a `k`-linear `G`-representation `A`, `H²(G, A)`, to be
 2-cocycles (i.e. `Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)`) modulo 2-coboundaries
@@ -703,8 +725,9 @@ abbrev H2 := (shortComplexH2 A).moduleCatHomology
 abbrev H2π : ModuleCat.of k (twoCocycles A) ⟶ H2 A := (shortComplexH2 A).moduleCatHomologyπ
 
 variable {A} in
-lemma H2π_eq_zero_iff (x : twoCocycles A) : H2π A x = 0 ↔ x ∈ twoCoboundaries A :=
-  Submodule.Quotient.mk_eq_zero _
+lemma H2π_eq_zero_iff (x : twoCocycles A) : H2π A x = 0 ↔ ⇑x ∈ twoCoboundaries A := by
+  show (LinearMap.range ((dOne A).codRestrict (twoCocycles A) _)).mkQ _ = 0 ↔ _
+  simp [LinearMap.range_codRestrict, twoCoboundaries]
 
 end Cohomology
 
@@ -731,8 +754,9 @@ section H1
 group homs `G → A`. -/
 def H1LequivOfIsTrivial [A.IsTrivial] :
     H1 A ≃ₗ[k] Additive G →+ A :=
-  (Submodule.quotEquivOfEqBot _ (oneCoboundaries_eq_bot_of_isTrivial A)).trans
-    (oneCocyclesLequivOfIsTrivial A)
+  (Submodule.quotEquivOfEqBot _
+    (by simp [shortComplexH1, ShortComplex.moduleCatToCycles, Submodule.eq_bot_iff])).trans
+  (oneCocyclesLequivOfIsTrivial A)
 
 theorem H1LequivOfIsTrivial_comp_H1π [A.IsTrivial] :
     (H1LequivOfIsTrivial A).comp (H1π A).hom = oneCocyclesLequivOfIsTrivial A := by