refactor(RepresentationTheory/GroupCohomology): tidy up 8599 and add more low degree cocycle API (#8785)

Author: Amelia Livingston

Mathlib/Algebra/Algebra/Equiv.lean

@@ -750,13 +750,6 @@ instance applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁ w
   mul_smul _ _ _ := rfl
 #align alg_equiv.apply_mul_semiring_action AlgEquiv.applyMulSemiringAction
 
-instance : MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ where
-  smul := fun f => Units.map f
-  one_smul := fun x => by ext; rfl
-  mul_smul := fun x y z => by ext; rfl
-  smul_mul := fun x y z => by ext; exact x.map_mul _ _
-  smul_one := fun x => by ext; exact x.map_one
-
 @[simp]
 protected theorem smul_def (f : A₁ ≃ₐ[R] A₁) (a : A₁) : f • a = f a :=
   rfl
@@ -774,6 +767,17 @@ instance apply_smulCommClass' : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁ where
   smul_comm e r a := e.map_smul r a
 #align alg_equiv.apply_smul_comm_class' AlgEquiv.apply_smulCommClass'
 
+instance : MulDistribMulAction (A₁ ≃ₐ[R] A₁) A₁ˣ where
+  smul := fun f => Units.map f
+  one_smul := fun x => by ext; rfl
+  mul_smul := fun x y z => by ext; rfl
+  smul_mul := fun x y z => by ext; exact x.map_mul _ _
+  smul_one := fun x => by ext; exact x.map_one
+
+@[simp]
+theorem smul_units_def (f : A₁ ≃ₐ[R] A₁) (x : A₁ˣ) :
+    f • x = Units.map f x := rfl
+
 @[simp]
 theorem algebraMap_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :
     algebraMap R A₂ y = e x ↔ algebraMap R A₁ y = x :=

Mathlib/Algebra/Algebra/Hom.lean

@@ -586,6 +586,10 @@ instance : MulDistribMulAction (A →ₐ[R] A) Aˣ where
   smul_mul := fun x y z => by ext; exact x.map_mul _ _
   smul_one := fun x => by ext; exact x.map_one
 
+@[simp]
+theorem smul_units_def (f : A →ₐ[R] A) (x : Aˣ) :
+    f • x = Units.map (f : A →* A) x := rfl
+
 end MulDistribMulAction
 end Algebra
 

Mathlib/RepresentationTheory/Basic.lean

@@ -293,7 +293,7 @@ theorem ofMulAction_single (g : G) (x : H) (r : k) :
 end MulAction
 section DistribMulAction
 
-variable (k G A : Type*) [CommSemiring k] [Monoid G] [AddCommGroup A] [Module k A]
+variable (k G A : Type*) [CommSemiring k] [Monoid G] [AddCommMonoid A] [Module k A]
   [DistribMulAction G A] [SMulCommClass G k A]
 
 /-- Turns a `k`-module `A` with a compatible `DistribMulAction` of a monoid `G` into a
@@ -320,8 +320,8 @@ def ofMulDistribMulAction : Representation ℤ M (Additive G) :=
   (addMonoidEndRingEquivInt (Additive G) : AddMonoid.End (Additive G) →* _).comp
     ((monoidEndToAdditive G : _ →* _).comp (MulDistribMulAction.toMonoidEnd M G))
 
-@[simp] theorem ofMulDistribMulAction_apply_apply (g : M) (a : G) :
-    ofMulDistribMulAction M G g a = g • a := rfl
+@[simp] theorem ofMulDistribMulAction_apply_apply (g : M) (a : Additive G) :
+    ofMulDistribMulAction M G g a = Additive.ofMul (g • Additive.toMul a) := rfl
 
 end MulDistribMulAction
 section Group

Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

@@ -16,8 +16,8 @@ Let `k` be a commutative ring and `G` a group. This file defines the group cohom
 `A : Rep k G` to be the cohomology of the complex
 $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
 with differential $d^n$ sending $f: G^n \to A$ to the function mapping $(g_0, \dots, g_n)$ to
-$$\rho(g_0)(f(g_1, \dots, g_n))
-+ \sum_{i = 0}^{n - 1} (-1)^{i + 1}\cdot f(g_0, \dots, g_ig_{i + 1}, \dots, g_n)$$
+$$\rho(g_0)(f(g_1, \dots, g_n))$$
+$$+ \sum_{i = 0}^{n - 1} (-1)^{i + 1}\cdot f(g_0, \dots, g_ig_{i + 1}, \dots, g_n)$$
 $$+ (-1)^{n + 1}\cdot f(g_0, \dots, g_{n - 1})$$ (where `ρ` is the representation attached to `A`).
 
 We have a `k`-linear isomorphism $\mathrm{Fun}(G^n, A) \cong \mathrm{Hom}(k[G^{n + 1}], A)$, where

Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

@@ -24,15 +24,17 @@ Noether's generalization also holds for infinite Galois extensions.
 
 ## Main statements
 
-* `hilbert90`: for all $f: Aut_K(L) \to L^\times$ satisfying the 1-cocycle condition, there exists
-`β : Lˣ` such that $f(g)g(β) = β$ for all `g : Aut_K(L)`.
-* `groupCohomology.hilbert90`: $H^1(Aut_K(L), L^\times)$ is trivial.
+* `groupCohomology.isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units`: Noether's generalization
+of Hilbert's Theorem 90: for all $f: Aut_K(L) \to L^\times$ satisfying the 1-cocycle
+condition, there exists `β : Lˣ` such that $g(β)/β = f(g)$ for all `g : Aut_K(L)`.
+* `groupCohomology.H1ofAutOnUnitsUnique`: Noether's generalization of Hilbert's Theorem 90:
+$H^1(Aut_K(L), L^\times)$ is trivial.
 
 ## Implementation notes
 
 Given a commutative ring `k` and a group `G`, group cohomology is developed in terms of `k`-linear
-`G`-representations on `k`-modules. Thus stating Noether's generalization of Hilbert 90 in terms
-of `H¹` requires us to turn the natural action of `Aut_K(L)` on `Lˣ` into a morphism
+`G`-representations on `k`-modules. Therefore stating Noether's generalization of Hilbert 90 in
+terms of `H¹` requires us to turn the natural action of `Aut_K(L)` on `Lˣ` into a morphism
 `Aut_K(L) →* (Additive Lˣ →ₗ[ℤ] Additive Lˣ)`. Thus we provide the non-`H¹` version too, as its
 statement is clearer.
 
@@ -46,16 +48,17 @@ for all $1 ≤ n.$
 -/
 
 open BigOperators
+namespace groupCohomology
 namespace Hilbert90
 
-variable (K L : Type*) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
+variable {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
 
 /-- Given `f : Aut_K(L) → Lˣ`, the sum `∑ f(φ) • φ` for `φ ∈ Aut_K(L)`, as a function `L → L`. -/
 noncomputable def aux (f : (L ≃ₐ[K] L) → Lˣ) : L → L :=
   Finsupp.total (L ≃ₐ[K] L) (L → L) L (fun φ => φ)
     (Finsupp.equivFunOnFinite.symm (fun φ => (f φ : L)))
 
-theorem aux_ne_zero (f : (L ≃ₐ[K] L) → Lˣ) : aux K L f ≠ 0 :=
+theorem aux_ne_zero (f : (L ≃ₐ[K] L) → Lˣ) : aux f ≠ 0 :=
 /- the set `Aut_K(L)` is linearly independent in the `L`-vector space `L → L`, by Dedekind's
 linear independence of characters -/
   have : LinearIndependent L (fun (f : L ≃ₐ[K] L) => (f : L → L)) :=
@@ -71,38 +74,38 @@ section
 open Hilbert90
 variable {K L : Type*} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
 
-theorem hilbert90 (f : (L ≃ₐ[K] L) → Lˣ)
-    (hf : ∀ (g h : (L ≃ₐ[K] L)), f (g * h) = g (f h) * f g) :
-    ∃ β : Lˣ, ∀ g : (L ≃ₐ[K] L), f g * Units.map g β = β := by
+/-- Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields and a
+function `f : Aut_K(L) → Lˣ` satisfying `f(gh) = g(f(h)) * f(g)` for all `g, h : Aut_K(L)`, there
+exists `β : Lˣ` such that `g(β)/β = f(g)` for all `g : Aut_K(L).` -/
+theorem isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units
+    (f : (L ≃ₐ[K] L) → Lˣ) (hf : IsMulOneCocycle f) :
+    IsMulOneCoboundary f := by
 /- Let `z : L` be such that `∑ f(h) * h(z) ≠ 0`, for `h ∈ Aut_K(L)` -/
-  obtain ⟨z, hz⟩ : ∃ z, aux K L f z ≠ 0 :=
-    not_forall.1 (fun H => aux_ne_zero K L f <| funext fun x => H x)
-  have : aux K L f z = ∑ h, f h * h z := by simp [aux, Finsupp.total, Finsupp.sum_fintype]
-/- Let `β = ∑ f(h) * h(z).` -/
-  use Units.mk0 (aux K L f z) hz
+  obtain ⟨z, hz⟩ : ∃ z, aux f z ≠ 0 :=
+    not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)
+  have : aux f z = ∑ h, f h * h z := by simp [aux, Finsupp.total, Finsupp.sum_fintype]
+/- Let `β = (∑ f(h) * h(z))⁻¹.` -/
+  use (Units.mk0 (aux f z) hz)⁻¹
   intro g
-/- Then the equality follows from the hypothesis `hf` (that `f` is a 1-cocycle). -/
-  simp_rw [Units.ext_iff, this, Units.val_mul, Units.coe_map, Units.val_mk0, MonoidHom.coe_coe,
-    map_sum, map_mul, Finset.mul_sum, ← mul_assoc, mul_comm (f _ : L), ← hf, mul_comm (f _ : L)]
-  exact Fintype.sum_bijective (fun i => g * i) (Group.mulLeft_bijective g) _ _ (fun i => rfl)
+/- Then the equality follows from the hypothesis that `f` is a 1-cocycle. -/
+  simp only [IsMulOneCocycle, IsMulOneCoboundary, AlgEquiv.smul_units_def,
+    map_inv, div_inv_eq_mul, inv_mul_eq_iff_eq_mul, Units.ext_iff, this,
+    Units.val_mul, Units.coe_map, Units.val_mk0, MonoidHom.coe_coe] at hf ⊢
+  simp_rw [map_sum, map_mul, Finset.sum_mul, mul_assoc, mul_comm _ (f _ : L), ← mul_assoc, ← hf g]
+  exact eq_comm.1 (Fintype.sum_bijective (fun i => g * i)
+    (Group.mulLeft_bijective g) _ _ (fun i => rfl))
 
 end
-namespace groupCohomology
 variable (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
 
-/-- Given a finite extension of fields `L/K`, the first group cohomology `H¹(Aut_K(L), Lˣ)` is
-trivial. -/
-noncomputable instance hilbert90 : Unique (H1 (Rep.ofAlgebraAutOnUnits K L)) where
+/-- Noether's generalization of Hilbert's Theorem 90: given a finite extension of fields `L/K`, the
+first group cohomology `H¹(Aut_K(L), Lˣ)` is trivial. -/
+noncomputable instance H1ofAutOnUnitsUnique : Unique (H1 (Rep.ofAlgebraAutOnUnits K L)) where
   default := 0
   uniq := fun a => Quotient.inductionOn' a fun x => (Submodule.Quotient.mk_eq_zero _).2 <| by
-    rcases _root_.hilbert90 (Additive.toMul ∘ x.1) (fun g h => Units.ext_iff.1
-      ((mem_oneCocycles_iff x.1).1 x.2 g h)) with ⟨β, hβ⟩
-    use Additive.ofMul (β⁻¹ : Lˣ)
-    ext g
-    refine' Additive.toMul.bijective.1 _
-    show Units.map g β⁻¹ / β⁻¹ = Additive.toMul (x.1 g)
-    rw [map_inv, div_inv_eq_mul, mul_comm]
-    -- TODO this used to be `exact` prior to leanprover/lean4#2478
-    apply mul_inv_eq_iff_eq_mul.2 (hβ g).symm
+    refine' (oneCoboundariesOfIsMulOneCoboundary _).2
+    rcases isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units x.1
+      (isMulOneCocycle_of_oneCocycles x) with ⟨β, hβ⟩
+    use β
 
 end groupCohomology