refactor(representation_theory/group_cohomology_resolution): refactor k[G^{n + 1}] isomorphism (#18271)

Amelia Livingston · Amelia Livingston · commit c04bc6e93e23 · 2023-03-30T00:32:10.000Z
This refactors the isomorphism $k[G^{n + 1}] \cong k[G] \otimes_k k[G^n]$ (where $G$ acts by left multiplication on $k[G^{n + 1}]$ and $k[G]$ but trivially on $k[G^n]$) to use an isomorphism of $G$-sets $G^{n + 1} \cong G \times G^n.$
diff --git a/src/representation_theory/Action.lean b/src/representation_theory/Action.lean
@@ -14,6 +14,7 @@ import category_theory.monoidal.rigid.of_equivalence
 import category_theory.monoidal.rigid.functor_category
 import category_theory.monoidal.linear
 import category_theory.monoidal.braided
+import category_theory.monoidal.types
 import category_theory.abelian.functor_category
 import category_theory.abelian.transfer
 import category_theory.conj
@@ -405,6 +406,13 @@ begin
   simp,
 end
 
+/-- Given an object `X` isomorphic to the tensor unit of `V`, `X` equipped with the trivial action
+is isomorphic to the tensor unit of `Action V G`. -/
+def tensor_unit_iso {X : V} (f : 𝟙_ V ≅ X) :
+  𝟙_ (Action V G) ≅ Action.mk X 1 :=
+Action.mk_iso f (λ g, by simp only [monoid_hom.one_apply, End.one_def, category.id_comp f.hom,
+  tensor_unit_rho, category.comp_id])
+
 variables (V G)
 
 /-- When `V` is monoidal the forgetful functor `Action V G` to `V` is monoidal. -/
@@ -653,6 +661,47 @@ def of_mul_action_limit_cone {ι : Type v} (G : Type (max v u)) [monoid G]
       congr,
     end } }
 
+/-- The `G`-set `G`, acting on itself by left multiplication. -/
+@[simps] def left_regular (G : Type u) [monoid G] : Action (Type u) (Mon.of G) :=
+Action.of_mul_action G G
+
+/-- The `G`-set `Gⁿ`, acting on itself by left multiplication. -/
+@[simps] def diagonal (G : Type u) [monoid G] (n : ℕ) : Action (Type u) (Mon.of G) :=
+Action.of_mul_action G (fin n → G)
+
+/-- We have `fin 1 → G ≅ G` as `G`-sets, with `G` acting by left multiplication. -/
+def diagonal_one_iso_left_regular (G : Type u) [monoid G] :
+  diagonal G 1 ≅ left_regular G := Action.mk_iso (equiv.fun_unique _ _).to_iso (λ g, rfl)
+
+/-- Given `X : Action (Type u) (Mon.of 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] def left_regular_tensor_iso (G : Type u) [group G]
+  (X : Action (Type u) (Mon.of G)) :
+  left_regular G ⊗ X ≅ left_regular G ⊗ Action.mk X.V 1 :=
+{ hom :=
+  { hom := λ g, ⟨g.1, (X.ρ (g.1⁻¹ : G) g.2 : X.V)⟩,
+    comm' := λ g, funext $ λ x, prod.ext rfl $
+      show (X.ρ ((g * x.1)⁻¹ : G) * X.ρ g) x.2 = _,
+      by simpa only [mul_inv_rev, ←X.ρ.map_mul, inv_mul_cancel_right] },
+  inv :=
+  { hom := λ g, ⟨g.1, X.ρ g.1 g.2⟩,
+    comm' := λ g, funext $ λ x, prod.ext rfl $
+      by simpa only [tensor_rho, types_comp_apply, tensor_apply, left_regular_ρ_apply, map_mul] },
+  hom_inv_id' := hom.ext _ _ (funext $ λ x, prod.ext rfl $
+    show (X.ρ x.1 * X.ρ (x.1⁻¹ : G)) x.2 = _,
+      by simpa only [←X.ρ.map_mul, mul_inv_self, X.ρ.map_one]),
+  inv_hom_id' := hom.ext _ _ (funext $ λ x, prod.ext rfl $
+    show (X.ρ (x.1⁻¹ : G) * X.ρ x.1) _ = _,
+      by simpa only [←X.ρ.map_mul, inv_mul_self, X.ρ.map_one]) }
+
+/-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
+each factor. -/
+@[simps] def diagonal_succ (G : Type u) [monoid G] (n : ℕ) :
+  diagonal G (n + 1) ≅ left_regular G ⊗ diagonal G n :=
+mk_iso (equiv.pi_fin_succ_above_equiv _ 0).to_iso (λ g, rfl)
+
 end Action
 
 namespace category_theory.functor
@@ -689,10 +738,11 @@ namespace category_theory.monoidal_functor
 
 open Action
 variables {V} {W : Type (u+1)} [large_category W] [monoidal_category V] [monoidal_category W]
+  (F : monoidal_functor V W) (G : Mon.{u})
 
 /-- A monoidal functor induces a monoidal functor between
 the categories of `G`-actions within those categories. -/
-@[simps] def map_Action (F : monoidal_functor V W) (G : Mon.{u}) :
+@[simps] def map_Action :
   monoidal_functor (Action V G) (Action W G) :=
 { ε :=
   { hom := F.ε,
@@ -709,4 +759,20 @@ the categories of `G`-actions within those categories. -/
   right_unitality' := by { intros, ext, dsimp, simp, dsimp, simp, },
   ..F.to_functor.map_Action G, }
 
+@[simp] lemma map_Action_ε_inv_hom :
+  (inv (F.map_Action G).ε).hom = inv F.ε :=
+begin
+  ext,
+  simp only [←F.map_Action_to_lax_monoidal_functor_ε_hom G, ←Action.comp_hom,
+    is_iso.hom_inv_id, id_hom],
+end
+
+@[simp] lemma map_Action_μ_inv_hom (X Y : Action V G) :
+  (inv ((F.map_Action G).μ X Y)).hom = inv (F.μ X.V Y.V) :=
+begin
+  ext,
+  simpa only [←F.map_Action_to_lax_monoidal_functor_μ_hom G, ←Action.comp_hom,
+    is_iso.hom_inv_id, id_hom],
+end
+
 end category_theory.monoidal_functor
diff --git a/src/representation_theory/Rep.lean b/src/representation_theory/Rep.lean
@@ -76,6 +76,17 @@ lemma of_ρ_apply {V : Type u} [add_comm_group V] [module k V]
   (ρ : representation k G V) (g : Mon.of G) :
   (Rep.of ρ).ρ g = ρ (g : G) := rfl
 
+variables (k G)
+
+/-- The trivial `k`-linear `G`-representation on a `k`-module `V.` -/
+def trivial (V : Type u) [add_comm_group V] [module k V] : Rep k G :=
+Rep.of (@representation.trivial k G V _ _ _ _)
+
+variables {k G}
+
+lemma trivial_def {V : Type u} [add_comm_group V] [module k V] (g : G) (v : V) :
+  (trivial k G V).ρ g v = v := rfl
+
 -- Verify that limits are calculated correctly.
 noncomputable example : preserves_limits (forget₂ (Rep k G) (Module.{u} k)) :=
 by apply_instance
@@ -101,35 +112,75 @@ noncomputable def linearization :
 variables {k G}
 
 @[simp] lemma linearization_obj_ρ (X : Action (Type u) (Mon.of G)) (g : G) (x : X.V →₀ k) :
-  ((linearization k G).1.1.obj X).ρ g x = finsupp.lmap_domain k k (X.ρ g) x := rfl
+  ((linearization k G).obj X).ρ g x = finsupp.lmap_domain k k (X.ρ g) x := rfl
 
 @[simp] lemma linearization_of (X : Action (Type u) (Mon.of G)) (g : G) (x : X.V) :
-  ((linearization k G).1.1.obj X).ρ g (finsupp.single x (1 : k))
+  ((linearization k G).obj X).ρ g (finsupp.single x (1 : k))
     = finsupp.single (X.ρ g x) (1 : k) :=
 by rw [linearization_obj_ρ, finsupp.lmap_domain_apply, finsupp.map_domain_single]
 
-variables (X Y : Action (Type u) (Mon.of G)) (f : X ⟶ Y)
+variables {X Y : Action (Type u) (Mon.of G)} (f : X ⟶ Y)
 
 @[simp] lemma linearization_map_hom :
-  ((linearization k G).1.1.map f).hom = finsupp.lmap_domain k k f.hom := rfl
+  ((linearization k G).map f).hom = finsupp.lmap_domain k k f.hom := rfl
 
-lemma linearization_map_hom_of (x : X.V) :
-  ((linearization k G).1.1.map f).hom (finsupp.single x (1 : k))
-    = finsupp.single (f.hom x) (1 : k) :=
+lemma linearization_map_hom_single (x : X.V) (r : k) :
+  ((linearization k G).map f).hom (finsupp.single x r)
+    = finsupp.single (f.hom x) r :=
 by rw [linearization_map_hom, finsupp.lmap_domain_apply, finsupp.map_domain_single]
 
+@[simp] lemma linearization_μ_hom (X Y : Action (Type u) (Mon.of G)) :
+  ((linearization k G).μ X Y).hom = (finsupp_tensor_finsupp' k X.V Y.V).to_linear_map :=
+rfl
+
+@[simp] lemma linearization_μ_inv_hom (X Y : Action (Type u) (Mon.of G)) :
+  (inv ((linearization k G).μ X Y)).hom = (finsupp_tensor_finsupp' k X.V Y.V).symm.to_linear_map :=
+begin
+  simp_rw [←Action.forget_map, functor.map_inv, Action.forget_map, linearization_μ_hom],
+  apply is_iso.inv_eq_of_hom_inv_id _,
+  exact linear_map.ext (λ x, linear_equiv.symm_apply_apply _ _),
+end
+
+@[simp] lemma linearization_ε_hom :
+  (linearization k G).ε.hom = finsupp.lsingle punit.star :=
+rfl
+
+@[simp] lemma linearization_ε_inv_hom_apply (r : k) :
+  (inv (linearization k G).ε).hom (finsupp.single punit.star r) = r :=
+begin
+  simp_rw [←Action.forget_map, functor.map_inv, Action.forget_map],
+  rw [←finsupp.lsingle_apply punit.star r],
+  apply is_iso.hom_inv_id_apply _ _,
+end
+
+variables (k G)
+
+/-- The linearization of a type `X` on which `G` acts trivially is the trivial `G`-representation
+on `k[X]`. -/
+@[simps] noncomputable def linearization_trivial_iso (X : Type u) :
+  (linearization k G).obj (Action.mk X 1) ≅ trivial k G (X →₀ k) :=
+Action.mk_iso (iso.refl _) $ λ g, by { ext1, ext1, exact linearization_of _ _ _ }
+
 variables (k G)
 
 /-- Given a `G`-action on `H`, this is `k[H]` bundled with the natural representation
 `G →* End(k[H])` as a term of type `Rep k G`. -/
 noncomputable abbreviation of_mul_action (H : Type u) [mul_action G H] : Rep k G :=
 of $ representation.of_mul_action k G H
 
+/-- The `k`-linear `G`-representation on `k[G]`, induced by left multiplication. -/
+noncomputable def left_regular : Rep k G :=
+of_mul_action k G G
+
+/-- The `k`-linear `G`-representation on `k[Gⁿ]`, induced by left multiplication. -/
+noncomputable def diagonal (n : ℕ) : Rep k G :=
+of_mul_action k G (fin n → G)
+
 /-- The linearization of a type `H` with a `G`-action is definitionally isomorphic to the
 `k`-linear `G`-representation on `k[H]` induced by the `G`-action on `H`. -/
-noncomputable def linearization_of_mul_action_iso (n : ℕ) :
-  (linearization k G).1.1.obj (Action.of_mul_action G (fin n → G))
-    ≅ of_mul_action k G (fin n → G) := iso.refl _
+noncomputable def linearization_of_mul_action_iso (H : Type u) [mul_action G H] :
+  (linearization k G).obj (Action.of_mul_action G H)
+    ≅ of_mul_action k G H := iso.refl _
 
 variables {k G}
 
diff --git a/src/representation_theory/basic.lean b/src/representation_theory/basic.lean
@@ -47,15 +47,15 @@ namespace representation
 
 section trivial
 
-variables {k G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
+variables (k : Type*) {G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
 
 /--
-The trivial representation of `G` on the one-dimensional module `k`.
+The trivial representation of `G` on a `k`-module V.
 -/
-def trivial : representation k G k := 1
+def trivial : representation k G V := 1
 
 @[simp]
-lemma trivial_def (g : G) (v : k) : trivial g v = v := rfl
+lemma trivial_def (g : G) (v : V) : trivial k g v = v := rfl
 
 end trivial
 
diff --git a/src/representation_theory/group_cohomology_resolution.lean b/src/representation_theory/group_cohomology_resolution.lean
