feat(RepresentationTheory/*): Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G) (leanprover-community#21736)

The first of 2 PRs refactoring group cohomology to use the bar resolution. Given a comm ring `k` and a group `G`, the bar resolution is the projective resolution of `k` as a trivial `G`-representation whose `n`th object is `Gⁿ →₀ k[G]`, with representation defined pointwise by the left regular representation on k[G], and whose differentials send `(g₀, ..., gₙ)` to `g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for `j = 0, ... , n - 1`.
The refactor means we can reuse this material to set up group homology. 

This PR defines an isomorphism between the objects in the standard resolution and the bar resolution, i.e. an isomorphism of representations `k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G])`, called `Rep.diagonalSuccIsoFree`.

Moves:
- groupCohomology.resolution.actionDiagonalSucc -> Action.diagonalSuccIsoTensorTrivial
- groupCohomology.resolution.diagonalSucc -> Rep.diagonalSuccIsoTensorTrivial



Co-authored-by: 101damnations <[email protected]>

Author: Amelia Livingston

Mathlib/CategoryTheory/Action/Basic.lean

@@ -63,16 +63,15 @@ variable (G : Type*) [Monoid G]
 
 section
 
+/-- The action defined by sending every group element to the identity. -/
+@[simps]
+def trivial (X : V) : Action V G := { V := X, ρ := 1 }
+
 instance inhabited' : Inhabited (Action (Type*) G) :=
   ⟨⟨PUnit, 1⟩⟩
 
-/-- The trivial representation of a group. -/
-def trivial : Action AddCommGrp G where
-  V := AddCommGrp.of PUnit
-  ρ := 1
-
 instance : Inhabited (Action AddCommGrp G) :=
-  ⟨trivial G⟩
+  ⟨trivial G <| AddCommGrp.of PUnit⟩
 
 end
 

Mathlib/CategoryTheory/Action/Concrete.lean

@@ -24,7 +24,23 @@ open CategoryTheory Limits
 
 namespace Action
 
+section
+variable {G : Type u} [Group G] {A : Action (Type u) G}
+
+@[simp]
+theorem ρ_inv_self_apply (g : G) (x : A.V) :
+    A.ρ g⁻¹ (A.ρ g x) = x :=
+  show (A.ρ g⁻¹ * A.ρ g) x = x by simp [← map_mul, Function.End.one_def]
+
+@[simp]
+theorem ρ_self_inv_apply (g : G) (x : A.V) :
+    A.ρ g (A.ρ g⁻¹ x) = x :=
+  show (A.ρ g * A.ρ g⁻¹) x = x by simp [← map_mul, Function.End.one_def]
+
+end
+
 /-- Bundles a type `H` with a multiplicative action of `G` as an `Action`. -/
+@[simps -isSimp]
 def ofMulAction (G : Type*) (H : Type u) [Monoid G] [MulAction G H] : Action (Type u) G where
   V := H
   ρ := @MulAction.toEndHom _ _ _ (by assumption)
@@ -58,13 +74,11 @@ def ofMulActionLimitCone {ι : Type v} (G : Type max v u) [Monoid G] (F : ι →
         rfl }
 
 /-- The `G`-set `G`, acting on itself by left multiplication. -/
-@[simps!]
-def leftRegular (G : Type u) [Monoid G] : Action (Type u) G :=
+abbrev leftRegular (G : Type u) [Monoid G] : Action (Type u) G :=
   Action.ofMulAction G G
 
 /-- The `G`-set `Gⁿ`, acting on itself by left multiplication. -/
-@[simps!]
-def diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) G :=
+abbrev diagonal (G : Type u) [Monoid G] (n : ℕ) : Action (Type u) G :=
   Action.ofMulAction G (Fin n → G)
 
 /-- We have `Fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication. -/

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.CategoryTheory.Monoidal.Linear
 import Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
@@ -189,48 +190,86 @@ end
 
 end Monoidal
 
+section
+
 open MonoidalCategory
 
-/-- Given `X : Action (Type u) G` for `G` a group, then `G × X` (with `G` acting as left
-multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to
-`G × X` (with `G` acting as left multiplication on the first factor and trivially on the second).
-The isomorphism is given by `(g, x) ↦ (g, g⁻¹ • x)`. -/
-@[simps]
-noncomputable def leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type u) G) :
-    leftRegular G ⊗ X ≅ leftRegular G ⊗ Action.mk X.V 1 where
-  hom :=
-    { hom := fun g => ⟨g.1, (X.ρ (g.1⁻¹ : G) g.2 : X.V)⟩
-      comm := fun (g : G) => by
-        funext ⟨(x₁ : G), (x₂ : X.V)⟩
-        refine Prod.ext rfl ?_
-        change (X.ρ ((g * x₁)⁻¹ : G) * X.ρ g) x₂ = X.ρ _ _
-        rw [mul_inv_rev, ← X.ρ.map_mul, inv_mul_cancel_right] }
-  inv :=
-    { hom := fun g => ⟨g.1, X.ρ g.1 g.2⟩
-      comm := fun (g : G) => by
-        funext ⟨(x₁ : G), (x₂ : X.V)⟩
-        refine Prod.ext rfl ?_
-        simp [leftRegular] }
-  hom_inv_id := by
-    apply Hom.ext
-    funext x
-    refine Prod.ext rfl ?_
-    change (X.ρ x.1 * X.ρ (x.1⁻¹ : G)) x.2 = x.2
-    rw [← X.ρ.map_mul, mul_inv_cancel, X.ρ.map_one, End.one_def, types_id_apply]
-  inv_hom_id := by
-    apply Hom.ext
-    funext x
-    refine Prod.ext rfl ?_
-    change (X.ρ (x.1⁻¹ : G) * X.ρ x.1) x.2 = x.2
-    rw [← X.ρ.map_mul, inv_mul_cancel, X.ρ.map_one, End.one_def, types_id_apply]
+variable (G : Type u)
 
 /-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
 each factor. -/
 @[simps!]
-noncomputable def diagonalSucc (G : Type*) [Monoid G] (n : ℕ) :
+noncomputable def diagonalSuccIsoTensorDiagonal [Monoid G] (n : ℕ) :
     diagonal G (n + 1) ≅ leftRegular G ⊗ diagonal G n :=
   mkIso (Fin.consEquiv _).symm.toIso fun _ => rfl
 
+@[deprecated (since := "2025-06-02")] alias diagonalSucc := diagonalSuccIsoTensorDiagonal
+
+variable [Group G]
+
+/-- Given `X : Action (Type u) G` for `G` a group, then `G × X` (with `G` acting as left
+multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to
+`G × X` (with `G` acting as left multiplication on the first factor and trivially on the second).
+The isomorphism is given by `(g, x) ↦ (g, g⁻¹ • x)`. -/
+@[simps!]
+noncomputable def leftRegularTensorIso (X : Action (Type u) G) :
+    leftRegular G ⊗ X ≅ leftRegular G ⊗ trivial G X.V :=
+  mkIso (Equiv.toIso {
+    toFun g := ⟨g.1, (X.ρ (g.1⁻¹ : G) g.2 : X.V)⟩
+    invFun g := ⟨g.1, X.ρ g.1 g.2⟩
+    left_inv _ := Prod.ext rfl <| by simp
+    right_inv _ := Prod.ext rfl <| by simp }) <| fun _ => by
+      ext _
+      simp only [tensorObj_V, tensor_ρ, types_comp_apply, tensor_apply, ofMulAction_apply]
+      simp
+
+/-- An isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on `Gⁿ⁺¹` and
+`G` but trivially on `Gⁿ`. The map sends `(g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`,
+and the inverse is `(g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).` -/
+noncomputable def diagonalSuccIsoTensorTrivial :
+    ∀ n : ℕ, diagonal G (n + 1) ≅ leftRegular G ⊗ trivial G (Fin n → G)
+  | 0 =>
+    diagonalOneIsoLeftRegular G ≪≫
+      (ρ_ _).symm ≪≫ tensorIso (Iso.refl _) (tensorUnitIso (Equiv.ofUnique PUnit _).toIso)
+  | n + 1 =>
+    diagonalSuccIsoTensorDiagonal _ _ ≪≫
+      tensorIso (Iso.refl _) (diagonalSuccIsoTensorTrivial n) ≪≫
+        leftRegularTensorIso _ _ ≪≫
+          tensorIso (Iso.refl _)
+            (mkIso (Fin.insertNthEquiv (fun _ => G) 0).toIso fun _ => rfl)
+
+variable {G}
+
+@[simp]
+theorem diagonalSuccIsoTensorTrivial_hom_hom_apply {n : ℕ} (f : Fin (n + 1) → G) :
+    (diagonalSuccIsoTensorTrivial G n).hom.hom f =
+      (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) := by
+  induction' n with n hn
+  · exact Prod.ext rfl (funext fun x => Fin.elim0 x)
+  · refine Prod.ext rfl (funext fun x => ?_)
+    induction' x using Fin.cases
+    <;> simp_all only [tensorObj_V, diagonalSuccIsoTensorTrivial, Iso.trans_hom, tensorIso_hom,
+      Iso.refl_hom, id_tensorHom, comp_hom, whiskerLeft_hom, types_comp_apply, whiskerLeft_apply,
+      leftRegularTensorIso_hom_hom, tensor_ρ, tensor_apply, ofMulAction_apply]
+    <;> simp [ofMulAction_V, types_tensorObj_def, Fin.tail, Fin.castSucc_fin_succ]
+
+@[simp]
+theorem diagonalSuccIsoTensorTrivial_inv_hom_apply {n : ℕ} (g : G) (f : Fin n → G) :
+    (diagonalSuccIsoTensorTrivial G n).inv.hom (g, f) =
+      (g • Fin.partialProd f : Fin (n + 1) → G) := by
+  induction' n with n hn generalizing g
+  · funext (x : Fin 1)
+    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
+      ofMulAction_V]
+  · funext x
+    induction' x using Fin.cases
+    <;> simp_all only [diagonalSuccIsoTensorTrivial, Iso.trans_inv, comp_hom, mkIso_inv_hom,
+        tensorObj_V, types_comp_apply, leftRegularTensorIso_inv_hom, tensor_ρ, tensor_apply,
+        ofMulAction_apply]
+    <;> simp_all [types_tensorObj_def, mul_assoc, Fin.partialProd_succ', ofMulAction_V]
+
+end
+
 end Action
 
 namespace CategoryTheory.Functor

Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

@@ -25,6 +25,10 @@ instance typesCartesianMonoidalCategory : CartesianMonoidalCategory (Type u) :=
 
 instance : BraidedCategory (Type u) := .ofCartesianMonoidalCategory
 
+theorem types_tensorObj_def {X Y : Type u} : X ⊗ Y = (X × Y) := rfl
+
+theorem types_tensorUnit_def : 𝟙_ (Type u) = PUnit := rfl
+
 @[simp]
 theorem tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : W ⊗ Y) :
     (f ⊗ g) p = (f p.1, g p.2) :=