feat(RepresentationTheory/GroupCohomology/LowDegree): `H¹(G, A) ≃ Hom…

…(G, A)` for a trivial representation (#7988)

Mathlib/RepresentationTheory/Basic.lean

@@ -62,11 +62,22 @@ def trivial : Representation k G V :=
 #align representation.trivial Representation.trivial
 
 -- Porting note: why is `V` implicit
-@[simp]
 theorem trivial_def (g : G) (v : V) : trivial k (V := V) g v = v :=
   rfl
 #align representation.trivial_def Representation.trivial_def
 
+variable {k}
+
+/-- A predicate for representations that fix every element. -/
+class IsTrivial (ρ : Representation k G V) : Prop where
+  out : ∀ g x, ρ g x = x := by aesop
+
+instance : IsTrivial (trivial k (G := G) (V := V)) where
+
+@[simp] theorem apply_eq_self
+    (ρ : Representation k G V) (g : G) (x : V) [h : IsTrivial ρ] :
+    ρ g x = x := h.out g x
+
 end trivial
 
 section MonoidAlgebra

Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

@@ -18,6 +18,8 @@ the cohomology of a complex `inhomogeneousCochains A`, whose objects are `(Fin n
 unnecessarily unwieldy in low degree. Moreover, cohomology of a complex is defined as an abstract
 cokernel, whereas the definitions here are explicit quotients of cocycles by coboundaries.
 
+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`.
@@ -29,12 +31,13 @@ for `n = 0, 1, 2`.
 1-coboundaries (i.e. `B¹(G, A) := Im(d⁰: A → Fun(G, A))`).
 * `groupCohomology.H2 A`: 2-cocycles (i.e. `Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)`) modulo
 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.
 
 ## TODO
 
 * Identify `Hn A` as defined in this file with `groupCohomology A n` for `n = 0, 1, 2`.
-* Properties of `H1`, like the isomorphism `H1(G, A) ≃ Hom(G, A)` when the representation
-is trivial
+* Hilbert's theorem 90
 * The relationship between `H2` and group extensions
 * The inflation-restriction exact sequence
 * Nonabelian group cohomology
@@ -55,22 +58,22 @@ section Cochains
 
 /-- The 0th object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
 to `A` as a `k`-module. -/
-def zeroCochainsLinearEquiv : (inhomogeneousCochains A).X 0 ≃ₗ[k] A :=
+def zeroCochainsLequiv : (inhomogeneousCochains A).X 0 ≃ₗ[k] A :=
   LinearEquiv.funUnique (Fin 0 → G) k A
 
 /-- The 1st object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
 to `Fun(G, A)` as a `k`-module. -/
-def oneCochainsLinearEquiv : (inhomogeneousCochains A).X 1 ≃ₗ[k] G → A :=
+def oneCochainsLequiv : (inhomogeneousCochains A).X 1 ≃ₗ[k] G → A :=
   LinearEquiv.funCongrLeft k A (Equiv.funUnique (Fin 1) G).symm
 
 /-- The 2nd object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
 to `Fun(G², A)` as a `k`-module. -/
-def twoCochainsLinearEquiv : (inhomogeneousCochains A).X 2 ≃ₗ[k] G × G → A :=
+def twoCochainsLequiv : (inhomogeneousCochains A).X 2 ≃ₗ[k] G × G → A :=
   LinearEquiv.funCongrLeft k A <| (piFinTwoEquiv fun _ => G).symm
 
 /-- The 3rd object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
 to `Fun(G³, A)` as a `k`-module. -/
-def threeCochainsLinearEquiv : (inhomogeneousCochains A).X 3 ≃ₗ[k] G × G × G → A :=
+def threeCochainsLequiv : (inhomogeneousCochains A).X 3 ≃ₗ[k] G × G × G → A :=
   LinearEquiv.funCongrLeft k A <| ((Equiv.piFinSucc 2 G).trans
     ((Equiv.refl G).prodCongr (piFinTwoEquiv fun _ => G))).symm
 
@@ -90,6 +93,10 @@ theorem dZero_ker_eq_invariants : LinearMap.ker (dZero A) = invariants A.ρ := b
   simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, Function.funext_iff]
   rfl
 
+@[simp] theorem dZero_eq_zero [A.IsTrivial] : dZero A = 0 := by
+  ext
+  simp only [dZero_apply, apply_eq_self, sub_self, LinearMap.zero_apply, Pi.zero_apply]
+
 /-- The 1st differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
 `k`-linear map `Fun(G, A) → Fun(G × G, A)`. It sends
 `(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).` -/
@@ -124,10 +131,10 @@ square commutes:
   v                    v
   A ---- dZero ---> Fun(G, A)
 ```
-where the vertical arrows are `zeroCochainsLinearEquiv` and `oneCochainsLinearEquiv` respectively.
+where the vertical arrows are `zeroCochainsLequiv` and `oneCochainsLequiv` respectively.
 -/
-theorem dZero_comp_eq : dZero A ∘ₗ (zeroCochainsLinearEquiv A) =
-    oneCochainsLinearEquiv A ∘ₗ (inhomogeneousCochains A).d 0 1 := by
+theorem dZero_comp_eq : dZero A ∘ₗ (zeroCochainsLequiv A) =
+    oneCochainsLequiv A ∘ₗ (inhomogeneousCochains A).d 0 1 := by
   ext x y
   show A.ρ y (x default) - x default = _ + ({0} : Finset _).sum _
   simp_rw [Fin.coe_fin_one, zero_add, pow_one, neg_smul, one_smul,
@@ -145,10 +152,10 @@ square commutes:
     v                      v
   Fun(G, A) -dOne-> Fun(G × G, A)
 ```
-where the vertical arrows are `oneCochainsLinearEquiv` and `twoCochainsLinearEquiv` respectively.
+where the vertical arrows are `oneCochainsLequiv` and `twoCochainsLequiv` respectively.
 -/
-theorem dOne_comp_eq : dOne A ∘ₗ oneCochainsLinearEquiv A =
-    twoCochainsLinearEquiv A ∘ₗ (inhomogeneousCochains A).d 1 2 := by
+theorem dOne_comp_eq : dOne A ∘ₗ oneCochainsLequiv A =
+    twoCochainsLequiv A ∘ₗ (inhomogeneousCochains A).d 1 2 := by
   ext x y
   show A.ρ y.1 (x _) - x _ + x _ =  _ + _
   rw [Fin.sum_univ_two]
@@ -167,11 +174,10 @@ square commutes:
         v                         v
   Fun(G × G, A) --dTwo--> Fun(G × G × G, A)
 ```
-where the vertical arrows are `twoCochainsLinearEquiv` and `threeCochainsLinearEquiv` respectively.
+where the vertical arrows are `twoCochainsLequiv` and `threeCochainsLequiv` respectively.
 -/
 theorem dTwo_comp_eq :
-    dTwo A ∘ₗ twoCochainsLinearEquiv A =
-      threeCochainsLinearEquiv A ∘ₗ (inhomogeneousCochains A).d 2 3 := by
+    dTwo A ∘ₗ twoCochainsLequiv A = threeCochainsLequiv A ∘ₗ (inhomogeneousCochains A).d 2 3 := by
   ext x y
   show A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _
   dsimp
@@ -210,49 +216,83 @@ def twoCocycles : Submodule k (G × G → A) := LinearMap.ker (dTwo A)
 variable {A}
 
 theorem mem_oneCocycles_def (f : G → A) :
-    f ∈ oneCocycles A ↔ ∀ g : G × G, A.ρ g.1 (f g.2) - f (g.1 * g.2) + f g.1 = 0 :=
-  LinearMap.mem_ker.trans Function.funext_iff
+    f ∈ oneCocycles A ↔ ∀ g h : G, A.ρ g (f h) - f (g * h) + f g = 0 :=
+  LinearMap.mem_ker.trans $ by
+    rw [Function.funext_iff]
+    simp only [dOne_apply, Pi.zero_apply, Prod.forall]
 
 theorem mem_oneCocycles_iff (f : G → A) :
-    f ∈ oneCocycles A ↔ ∀ g : G × G, f (g.1 * g.2) = A.ρ g.1 (f g.2) + f g.1 := by
+    f ∈ oneCocycles A ↔ ∀ g h : G, f (g * h) = A.ρ g (f h) + f g := by
   simp_rw [mem_oneCocycles_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]
 
-theorem oneCocycles_map_one (f : oneCocycles A) : f.1 1 = 0 := by
-  have := (mem_oneCocycles_def f.1).1 f.2 (1, 1)
+@[simp] theorem oneCocycles_map_one (f : oneCocycles A) : f.1 1 = 0 := by
+  have := (mem_oneCocycles_def f.1).1 f.2 1 1
   simpa only [map_one, LinearMap.one_apply, mul_one, sub_self, zero_add] using this
 
-theorem oneCocycles_map_inv (f : oneCocycles A) (g : G) :
+@[simp] theorem oneCocycles_map_inv (f : oneCocycles A) (g : G) :
     A.ρ g (f.1 g⁻¹) = - f.1 g := by
   rw [← add_eq_zero_iff_eq_neg, ← oneCocycles_map_one f, ← mul_inv_self g,
-    (mem_oneCocycles_iff f.1).1 f.2 (g, g⁻¹)]
+    (mem_oneCocycles_iff f.1).1 f.2 g g⁻¹]
+
+theorem oneCocycles_map_mul_of_isTrivial [A.IsTrivial] (f : oneCocycles A) (g h : G) :
+    f.1 (g * h) = f.1 g + f.1 h := by
+  rw [(mem_oneCocycles_iff f.1).1 f.2, apply_eq_self A.ρ g (f.1 h), add_comm]
+
+theorem mem_oneCocycles_of_addMonoidHom [A.IsTrivial] (f : Additive G →+ A) :
+    f ∘ Additive.ofMul ∈ oneCocycles A :=
+  (mem_oneCocycles_iff _).2 fun g h => by
+    simp only [Function.comp_apply, ofMul_mul, map_add,
+      oneCocycles_map_mul_of_isTrivial, apply_eq_self A.ρ g (f (Additive.ofMul h)),
+      add_comm (f (Additive.ofMul g))]
+
+variable (A)
+
+/-- When `A : Rep k G` is a trivial representation of `G`, `Z¹(G, A)` is isomorphic to the
+group homs `G → A`. -/
+@[simps] def oneCocyclesLequivOfIsTrivial [hA : A.IsTrivial] :
+    oneCocycles A ≃ₗ[k] Additive G →+ A where
+  toFun f :=
+    { toFun := f.1 ∘ Additive.toMul
+      map_zero' := oneCocycles_map_one f
+      map_add' := oneCocycles_map_mul_of_isTrivial f }
+  map_add' x y := rfl
+  map_smul' r x := rfl
+  invFun f :=
+    { val := f
+      property := mem_oneCocycles_of_addMonoidHom f }
+  left_inv f := by ext; rfl
+  right_inv f := by ext; rfl
+
+variable {A}
 
 theorem mem_twoCocycles_def (f : G × G → A) :
-    f ∈ twoCocycles A ↔ ∀ g : G × G × G,
-      A.ρ g.1 (f (g.2.1, g.2.2)) - f (g.1 * g.2.1, g.2.2) +
-        f (g.1, g.2.1 * g.2.2) - f (g.1, g.2.1) = 0 :=
-  LinearMap.mem_ker.trans Function.funext_iff
+    f ∈ twoCocycles A ↔ ∀ g h j : G,
+      A.ρ g (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0 :=
+  LinearMap.mem_ker.trans $ by
+    rw [Function.funext_iff]
+    simp only [dTwo_apply, Prod.mk.eta, Pi.zero_apply, Prod.forall]
 
 theorem mem_twoCocycles_iff (f : G × G → A) :
-    f ∈ twoCocycles A ↔ ∀ g : G × G × G,
-      f (g.1 * g.2.1, g.2.2) + f (g.1, g.2.1) =
-        A.ρ g.1 (f (g.2.1, g.2.2)) + f (g.1, g.2.1 * g.2.2) := by
+    f ∈ twoCocycles A ↔ ∀ g h j : G,
+      f (g * h, j) + f (g, h) =
+        A.ρ g (f (h, j)) + f (g, h * j) := by
   simp_rw [mem_twoCocycles_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
-    add_comm (f (Prod.fst _, _))]
+    add_comm (f (_ * _, _))]
 
 theorem twoCocycles_map_one_fst (f : twoCocycles A) (g : G) :
     f.1 (1, g) = f.1 (1, 1) := by
-  have := ((mem_twoCocycles_iff f.1).1 f.2 (1, (1, g))).symm
+  have := ((mem_twoCocycles_iff f.1).1 f.2 1 1 g).symm
   simpa only [map_one, LinearMap.one_apply, one_mul, add_right_inj, this]
 
 theorem twoCocycles_map_one_snd (f : twoCocycles A) (g : G) :
     f.1 (g, 1) = A.ρ g (f.1 (1, 1)) := by
-  have := (mem_twoCocycles_iff f.1).1 f.2 (g, (1, 1))
+  have := (mem_twoCocycles_iff f.1).1 f.2 g 1 1
   simpa only [mul_one, add_left_inj, this]
 
 lemma twoCocycles_ρ_map_inv_sub_map_inv (f : twoCocycles A) (g : G) :
     A.ρ g (f.1 (g⁻¹, g)) - f.1 (g, g⁻¹)
       = f.1 (1, 1) - f.1 (g, 1) := by
-  have := (mem_twoCocycles_iff f.1).1 f.2 (g, g⁻¹, g)
+  have := (mem_twoCocycles_iff f.1).1 f.2 g g⁻¹ g
   simp only [mul_right_inv, mul_left_inv, twoCocycles_map_one_fst _ g]
     at this
   exact sub_eq_sub_iff_add_eq_add.2 this.symm
@@ -276,7 +316,7 @@ variable {A}
 
 theorem mem_oneCoboundaries_of_dZero_apply (x : A) :
     ⟨dZero A x, LinearMap.ext_iff.1 (dOne_comp_dZero A) x⟩ ∈ oneCoboundaries A :=
-LinearMap.mem_range_self _ _
+  LinearMap.mem_range_self _ _
 
 theorem mem_oneCoboundaries_of_mem_range (f : G → A) (h : f ∈ LinearMap.range (dZero A)) :
     ⟨f, LinearMap.range_le_ker_iff.2 (dOne_comp_dZero A) h⟩ ∈ oneCoboundaries A := by
@@ -286,9 +326,14 @@ theorem mem_range_of_mem_oneCoboundaries (f : oneCocycles A) (h : f ∈ oneCobou
     f.1 ∈ LinearMap.range (dZero A) := by
   rcases h with ⟨x, rfl⟩; exact ⟨x, 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_twoCoboundaries_of_dOne_apply (x : G → A) :
     ⟨dOne A x, LinearMap.ext_iff.1 (dTwo_comp_dOne A) x⟩ ∈ twoCoboundaries A :=
-LinearMap.mem_range_self _ _
+  LinearMap.mem_range_self _ _
 
 theorem mem_twoCoboundaries_of_mem_range (f : G × G → A) (h : f ∈ LinearMap.range (dOne A)) :
     ⟨f, LinearMap.range_le_ker_iff.2 (dTwo_comp_dOne A) h⟩ ∈ twoCoboundaries A := by
@@ -322,4 +367,42 @@ abbrev H2 := twoCocycles A ⧸ twoCoboundaries A
 def H2_π : twoCocycles A →ₗ[k] H2 A := (twoCoboundaries A).mkQ
 
 end Cohomology
+section H0
+
+/-- When the representation on `A` is trivial, then `H⁰(G, A)` is all of `A.` -/
+def H0LequivOfIsTrivial [A.IsTrivial] :
+    H0 A ≃ₗ[k] A := LinearEquiv.ofTop _ (invariants_eq_top A.ρ)
+
+@[simp] theorem H0LequivOfIsTrivial_eq_subtype [A.IsTrivial] :
+    H0LequivOfIsTrivial A = A.ρ.invariants.subtype := rfl
+
+theorem H0LequivOfIsTrivial_apply [A.IsTrivial] (x : H0 A) :
+    H0LequivOfIsTrivial A x = x := rfl
+
+@[simp] theorem H0LequivOfIsTrivial_symm_apply [A.IsTrivial] (x : A) :
+    (H0LequivOfIsTrivial A).symm x = x := rfl
+
+end H0
+section H1
+
+/-- When `A : Rep k G` is a trivial representation of `G`, `H¹(G, A)` is isomorphic to the
+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)
+
+theorem H1LequivOfIsTrivial_comp_H1_π [A.IsTrivial] :
+    (H1LequivOfIsTrivial A).comp (H1_π A) = oneCocyclesLequivOfIsTrivial A := by
+  ext; rfl
+
+@[simp] theorem H1LequivOfIsTrivial_H1_π_apply_apply
+    [A.IsTrivial] (f : oneCocycles A) (x : Additive G) :
+    H1LequivOfIsTrivial A (H1_π A f) x = f.1 (Additive.toMul x) := rfl
+
+@[simp] theorem H1LequivOfIsTrivial_symm_apply [A.IsTrivial] (f : Additive G →+ A) :
+    (H1LequivOfIsTrivial A).symm f = H1_π A ((oneCocyclesLequivOfIsTrivial A).symm f) :=
+  rfl
+
+end H1
 end groupCohomology

Mathlib/RepresentationTheory/Invariants.lean

@@ -91,6 +91,10 @@ theorem invariants_eq_inter : (invariants ρ).carrier = ⋂ g : G, Function.fixe
   ext; simp [Function.IsFixedPt]
 #align representation.invariants_eq_inter Representation.invariants_eq_inter
 
+theorem invariants_eq_top [ρ.IsTrivial] :
+    invariants ρ = ⊤ :=
+eq_top_iff.2 (fun x _ g => ρ.apply_eq_self g x)
+
 variable [Fintype G] [Invertible (Fintype.card G : k)]
 
 /-- The action of `average k G` gives a projection map onto the subspace of invariants.

Mathlib/RepresentationTheory/Rep.lean

@@ -136,6 +136,15 @@ theorem trivial_def {V : Type u} [AddCommGroup V] [Module k V] (g : G) (v : V) :
 set_option linter.uppercaseLean3 false in
 #align Rep.trivial_def Rep.trivial_def
 
+/-- A predicate for representations that fix every element. -/
+abbrev IsTrivial (A : Rep k G) := A.ρ.IsTrivial
+
+instance {V : Type u} [AddCommGroup V] [Module k V] :
+    IsTrivial (Rep.trivial k G V) where
+
+instance {V : Type u} [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] :
+    IsTrivial (Rep.of ρ) where
+
 -- Porting note: the two following instances were found automatically in mathlib3
 noncomputable instance : PreservesLimits (forget₂ (Rep k G) (ModuleCat.{u} k)) :=
   Action.instPreservesLimitsForget.{u} _ _