feat(representation_theory/group_cohomology_resolution): add isomorphism with nth inhomogeneous cochains (#18159)

Amelia Livingston · joelriou · Amelia Livingston · commit 3dec44d0b621 · 2023-03-27T02:38:29.000Z
Given a $k$-linear $G$-representation $A,$ this defines the $k$-linear isomorphism between functions $G^n \to A$ and representation morphisms $Hom(k[G^{n + 1}], A),$ called `Rep.diagonal_hom_equiv`.



Co-authored-by: Joël Riou &lt;joel.riou@universite-paris-saclay.fr&gt;
diff --git a/src/category_theory/linear/basic.lean b/src/category_theory/linear/basic.lean
@@ -130,6 +130,28 @@ instance {X Y : C} (f : X ⟶ Y) [mono f] (r : R) [invertible r] : mono (r • f
   simpa [smul_smul] using congr_arg (λ f, ⅟r • f) H,
 end⟩
 
+/-- Given isomorphic objects `X ≅ Y, W ≅ Z` in a `k`-linear category, we have a `k`-linear
+isomorphism between `Hom(X, W)` and `Hom(Y, Z).` -/
+def hom_congr (k : Type*) {C : Type*} [category C] [semiring k]
+  [preadditive C] [linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) :
+  (X ⟶ W) ≃ₗ[k] (Y ⟶ Z) :=
+{ inv_fun := (left_comp k W f₁.hom).comp (right_comp k Y f₂.symm.hom),
+  left_inv := λ x, by simp only [iso.symm_hom, linear_map.to_fun_eq_coe, linear_map.coe_comp,
+    function.comp_app, left_comp_apply, right_comp_apply, category.assoc, iso.hom_inv_id,
+    category.comp_id, iso.hom_inv_id_assoc],
+  right_inv := λ x, by simp only [iso.symm_hom, linear_map.coe_comp, function.comp_app,
+    right_comp_apply, left_comp_apply, linear_map.to_fun_eq_coe, iso.inv_hom_id_assoc,
+    category.assoc, iso.inv_hom_id, category.comp_id],
+  ..(right_comp k Y f₂.hom).comp (left_comp k W f₁.symm.hom) }
+
+lemma hom_congr_apply (k : Type*) {C : Type*} [category C] [semiring k]
+  [preadditive C] [linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : X ⟶ W) :
+  hom_congr k f₁ f₂ f = (f₁.inv ≫ f) ≫ f₂.hom := rfl
+
+lemma hom_congr_symm_apply (k : Type*) {C : Type*} [category C] [semiring k]
+  [preadditive C] [linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) :
+  (hom_congr k f₁ f₂).symm f = f₁.hom ≫ f ≫ f₂.inv := rfl
+
 end
 
 section
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
@@ -344,7 +344,7 @@ theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) :
 end lsum
 
 section
-variables (M) (R) (X : Type*)
+variables (M) (R) (X : Type*) (S) [module S M] [smul_comm_class R S M]
 
 /--
 A slight rearrangement from `lsum` gives us
@@ -362,6 +362,24 @@ lemma lift_apply (f) (g) :
   ((lift M R X) f) g = g.sum (λ x r, r • f x) :=
 rfl
 
+/-- Given compatible `S` and `R`-module structures on `M` and a type `X`, the set of functions
+`X → M` is `S`-linearly equivalent to the `R`-linear maps from the free `R`-module
+on `X` to `M`. -/
+noncomputable def llift : (X → M) ≃ₗ[S] ((X →₀ R) →ₗ[R] M) :=
+{ map_smul' :=
+  begin
+    intros,
+    dsimp,
+    ext,
+    simp only [coe_comp, function.comp_app, lsingle_apply, lift_apply, pi.smul_apply,
+      sum_single_index, zero_smul, one_smul, linear_map.smul_apply],
+  end, ..lift M R X }
+
+@[simp] lemma llift_apply (f : X → M) (x : X →₀ R) :
+  llift M R S X f x = lift M R X f x := rfl
+
+@[simp] lemma llift_symm_apply (f : (X →₀ R) →ₗ[R] M) (x : X) :
+  (llift M R S X).symm f x = f (single x 1) := rfl
 end
 
 section lmap_domain
diff --git a/src/representation_theory/Action.lean b/src/representation_theory/Action.lean
@@ -504,12 +504,12 @@ rfl
 rfl
 
 @[simp] lemma functor_category_monoidal_equivalence.functor_map {A B : Action V G} (f : A ⟶ B) :
-  (functor_category_monoidal_equivalence _ _).1.1.map f
+  (functor_category_monoidal_equivalence _ _).map f
     = functor_category_equivalence.functor.map f := rfl
 
 @[simp] lemma functor_category_monoidal_equivalence.inverse_map
   {A B : single_obj G ⥤ V} (f : A ⟶ B) :
-  (functor_category_monoidal_equivalence _ _).1.inv.map f
+  (functor_category_monoidal_equivalence _ _).inv.map f
     = functor_category_equivalence.inverse.map f := rfl
 
 variables (H : Group.{u})
diff --git a/src/representation_theory/Rep.lean b/src/representation_theory/Rep.lean
@@ -68,12 +68,26 @@ lemma coe_of {V : Type u} [add_comm_group V] [module k V] (ρ : G →* (V →ₗ
 @[simp] lemma of_ρ {V : Type u} [add_comm_group V] [module k V] (ρ : G →* (V →ₗ[k] V)) :
   (of ρ).ρ = ρ := rfl
 
+@[simp] lemma Action_ρ_eq_ρ {A : Rep k G} : Action.ρ A = A.ρ := rfl
+
+/-- Allows us to apply lemmas about the underlying `ρ`, which would take an element `g : G` rather
+than `g : Mon.of G` as an argument. -/
+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
+
 -- Verify that limits are calculated correctly.
 noncomputable example : preserves_limits (forget₂ (Rep k G) (Module.{u} k)) :=
 by apply_instance
 noncomputable example : preserves_colimits (forget₂ (Rep k G) (Module.{u} k)) :=
 by apply_instance
 
+@[simp] lemma monoidal_category.braiding_hom_apply {A B : Rep k G} (x : A) (y : B) :
+  Action.hom.hom (β_ A B).hom (tensor_product.tmul k x y) = tensor_product.tmul k y x := rfl
+
+@[simp] lemma monoidal_category.braiding_inv_apply {A B : Rep k G} (x : A) (y : B) :
+  Action.hom.hom (β_ A B).inv (tensor_product.tmul k y x) = tensor_product.tmul k x y := rfl
+
 section linearization
 
 variables (k G)
@@ -117,6 +131,56 @@ 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 _
 
+variables {k G}
+
+/-- Given an element `x : A`, there is a natural morphism of representations `k[G] ⟶ A` sending
+`g ↦ A.ρ(g)(x).` -/
+@[simps] noncomputable def left_regular_hom (A : Rep k G) (x : A) :
+  Rep.of_mul_action k G G ⟶ A :=
+{ hom := finsupp.lift _ _ _ (λ g, A.ρ g x),
+  comm' := λ g,
+  begin
+    refine finsupp.lhom_ext' (λ y, linear_map.ext_ring _),
+    simpa only [linear_map.comp_apply, Module.comp_def, finsupp.lsingle_apply,
+      finsupp.lift_apply, Action_ρ_eq_ρ, of_ρ_apply, representation.of_mul_action_single,
+      finsupp.sum_single_index, zero_smul, one_smul, smul_eq_mul, A.ρ.map_mul],
+  end }
+
+lemma left_regular_hom_apply {A : Rep k G} (x : A) :
+  (left_regular_hom A x).hom (finsupp.single 1 1) = x :=
+begin
+  simpa only [left_regular_hom_hom, finsupp.lift_apply, finsupp.sum_single_index, one_smul,
+    A.ρ.map_one, zero_smul],
+end
+
+/-- Given a `k`-linear `G`-representation `A`, there is a `k`-linear isomorphism between
+representation morphisms `Hom(k[G], A)` and `A`. -/
+@[simps] noncomputable def left_regular_hom_equiv (A : Rep k G) :
+  (Rep.of_mul_action k G G ⟶ A) ≃ₗ[k] A :=
+{ to_fun := λ f, f.hom (finsupp.single 1 1),
+  map_add' := λ x y, rfl,
+  map_smul' := λ r x, rfl,
+  inv_fun := λ x, left_regular_hom A x,
+  left_inv := λ f,
+  begin
+    refine Action.hom.ext _ _ (finsupp.lhom_ext' (λ (x : G), linear_map.ext_ring _)),
+    have : f.hom (((of_mul_action k G G).ρ) x (finsupp.single (1 : G) (1 : k)))
+      = A.ρ x (f.hom (finsupp.single (1 : G) (1 : k))) :=
+      linear_map.ext_iff.1 (f.comm x) (finsupp.single 1 1),
+    simp only [linear_map.comp_apply, finsupp.lsingle_apply,
+      left_regular_hom_hom, finsupp.lift_apply, finsupp.sum_single_index, one_smul, ←this,
+      zero_smul, of_ρ_apply, representation.of_mul_action_single x (1 : G) (1 : k), smul_eq_mul,
+      mul_one],
+  end,
+  right_inv := λ x, left_regular_hom_apply x }
+
+lemma left_regular_hom_equiv_symm_single {A : Rep k G} (x : A) (g : G) :
+  ((left_regular_hom_equiv A).symm x).hom (finsupp.single g 1) = A.ρ g x :=
+begin
+  simp only [left_regular_hom_equiv_symm_apply, left_regular_hom_hom,
+    finsupp.lift_apply, finsupp.sum_single_index, zero_smul, one_smul],
+end
+
 end linearization
 end
 section
@@ -162,8 +226,7 @@ rfl
 `G`-representation `B,` the `k`-linear map underlying the resulting map `B ⟶ iHom(A, A ⊗ B)` is
 given by flipping the arguments in the natural `k`-bilinear map `A →ₗ[k] B →ₗ[k] A ⊗ B`. -/
 @[simp] lemma ihom_coev_app_hom :
-  Action.hom.hom ((ihom.coev A).app B) =
-    (tensor_product.mk _ _ _).flip :=
+  Action.hom.hom ((ihom.coev A).app B) = (tensor_product.mk _ _ _).flip :=
 begin
   refine linear_map.ext (λ x, linear_map.ext (λ y, _)),
   simpa only [ihom_coev_app_def, functor.map_comp, comp_hom,
@@ -208,9 +271,79 @@ the identity map on `Homₖ(A, B).` -/
   tensor_product.uncurry _ _ _ _ linear_map.id.flip :=
 monoidal_closed_uncurry_hom _
 
+variables (A B C)
+
+/-- There is a `k`-linear isomorphism between the sets of representation morphisms`Hom(A ⊗ B, C)`
+and `Hom(B, Homₖ(A, C))`. -/
+noncomputable def monoidal_closed.linear_hom_equiv :
+  (A ⊗ B ⟶ C) ≃ₗ[k] (B ⟶ (A ⟶[Rep k G] C)) :=
+{ map_add' := λ f g, rfl,
+  map_smul' := λ r f, rfl, ..(ihom.adjunction A).hom_equiv _ _ }
+
+/-- There is a `k`-linear isomorphism between the sets of representation morphisms`Hom(A ⊗ B, C)`
+and `Hom(A, Homₖ(B, C))`. -/
+noncomputable def monoidal_closed.linear_hom_equiv_comm :
+  (A ⊗ B ⟶ C) ≃ₗ[k] (A ⟶ (B ⟶[Rep k G] C)) :=
+(linear.hom_congr k (β_ A B) (iso.refl _)) ≪≫ₗ
+  monoidal_closed.linear_hom_equiv _ _ _
+
+variables {A B C}
+
+lemma monoidal_closed.linear_hom_equiv_hom (f : A ⊗ B ⟶ C) :
+  (monoidal_closed.linear_hom_equiv A B C f).hom =
+  (tensor_product.curry f.hom).flip :=
+monoidal_closed_curry_hom _
+
+lemma monoidal_closed.linear_hom_equiv_comm_hom (f : A ⊗ B ⟶ C) :
+  (monoidal_closed.linear_hom_equiv_comm A B C f).hom =
+ tensor_product.curry f.hom :=
+begin
+  dunfold monoidal_closed.linear_hom_equiv_comm,
+  refine linear_map.ext (λ x, linear_map.ext (λ y, _)),
+  simp only [linear_equiv.trans_apply, monoidal_closed.linear_hom_equiv_hom,
+    linear.hom_congr_apply, iso.refl_hom, iso.symm_hom, linear_map.to_fun_eq_coe,
+    linear_map.coe_comp, function.comp_app, linear.left_comp_apply, linear.right_comp_apply,
+    category.comp_id, Action.comp_hom, linear_map.flip_apply, tensor_product.curry_apply,
+    Module.coe_comp, function.comp_app, monoidal_category.braiding_inv_apply],
+end
+
+lemma monoidal_closed.linear_hom_equiv_symm_hom (f : B ⟶ (A ⟶[Rep k G] C)) :
+  ((monoidal_closed.linear_hom_equiv A B C).symm f).hom =
+  tensor_product.uncurry k A B C f.hom.flip :=
+monoidal_closed_uncurry_hom _
+
+lemma monoidal_closed.linear_hom_equiv_comm_symm_hom (f : A ⟶ (B ⟶[Rep k G] C)) :
+  ((monoidal_closed.linear_hom_equiv_comm A B C).symm f).hom =
+  tensor_product.uncurry k A B C f.hom :=
+begin
+  dunfold monoidal_closed.linear_hom_equiv_comm,
+  refine tensor_product.algebra_tensor_module.curry_injective
+    (linear_map.ext (λ x, linear_map.ext (λ y, _))),
+  simp only [linear_equiv.trans_symm, linear_equiv.trans_apply, linear.hom_congr_symm_apply,
+    iso.refl_inv, linear_map.coe_comp, function.comp_app, category.comp_id, Action.comp_hom,
+    monoidal_closed.linear_hom_equiv_symm_hom, tensor_product.algebra_tensor_module.curry_apply,
+    linear_map.coe_restrict_scalars, linear_map.to_fun_eq_coe, linear_map.flip_apply,
+    tensor_product.curry_apply, Module.coe_comp, function.comp_app,
+    monoidal_category.braiding_hom_apply, tensor_product.uncurry_apply],
+end
+
 end
 end Rep
+namespace representation
+variables {k G : Type u} [comm_ring k] [monoid G] {V W : Type u}
+  [add_comm_group V] [add_comm_group W] [module k V] [module k W]
+  (ρ : representation k G V) (τ : representation k G W)
+
+/-- Tautological isomorphism to help Lean in typechecking. -/
+def Rep_of_tprod_iso : Rep.of (ρ.tprod τ) ≅ Rep.of ρ ⊗ Rep.of τ := iso.refl _
+
+lemma Rep_of_tprod_iso_apply (x : tensor_product k V W) :
+  (Rep_of_tprod_iso ρ τ).hom.hom x = x := rfl
+
+lemma Rep_of_tprod_iso_inv_apply (x : tensor_product k V W) :
+  (Rep_of_tprod_iso ρ τ).inv.hom x = x := rfl
 
+end representation
 /-!
 # The categorical equivalence `Rep k G ≌ Module.{u} (monoid_algebra k G)`.
 -/
diff --git a/src/representation_theory/basic.lean b/src/representation_theory/basic.lean
@@ -245,6 +245,10 @@ variables {k G H}
 
 lemma of_mul_action_def (g : G) : of_mul_action k G H g = finsupp.lmap_domain k k ((•) g) := rfl
 
+lemma of_mul_action_single (g : G) (x : H) (r : k) :
+  of_mul_action k G H g (finsupp.single x r) = finsupp.single (g • x) r :=
+finsupp.map_domain_single
+
 end mul_action
 section group
 
diff --git a/src/representation_theory/group_cohomology_resolution.lean b/src/representation_theory/group_cohomology_resolution.lean
@@ -169,12 +169,12 @@ variables {k G n}
 
 @[simp] lemma to_tensor_single (f : Gⁿ⁺¹) (m : k) :
   (to_tensor k G n).hom (single f m) = single (f 0) m ⊗ₜ single (λ i, (f i)⁻¹ * f i.succ) 1 :=
-to_tensor_aux_single _ _
+by apply to_tensor_aux_single f m
 
 @[simp] lemma of_tensor_single (g : G) (m : k) (x : Gⁿ →₀ k) :
   (of_tensor k G n).hom ((single g m) ⊗ₜ x) =
   finsupp.lift (Rep.of_mul_action k G Gⁿ⁺¹) k Gⁿ (λ f, single (g • partial_prod f) m) x :=
-of_tensor_aux_single _ _ _
+by apply of_tensor_aux_single g m x
 
 lemma of_tensor_single' (g : G →₀ k) (x : Gⁿ) (m : k) :
   (of_tensor k G n).hom (g ⊗ₜ single x m) =
@@ -233,6 +233,58 @@ module.free.of_basis (of_mul_action_basis k G n)
 
 end basis
 end group_cohomology.resolution
+namespace Rep
+variables (n) [group G]
+open group_cohomology.resolution
+
+/-- Given a `k`-linear `G`-representation `A`, the set of representation morphisms
+`Hom(k[Gⁿ⁺¹], A)` is `k`-linearly isomorphic to the set of functions `Gⁿ → A`. -/
+noncomputable def diagonal_hom_equiv (A : Rep k G) :
+  (Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A) ≃ₗ[k] ((fin n → G) → A) :=
+linear.hom_congr k ((equiv_tensor k G n).trans
+  ((representation.of_mul_action k G G).Rep_of_tprod_iso 1)) (iso.refl _) ≪≫ₗ
+  ((Rep.monoidal_closed.linear_hom_equiv_comm _ _ _) ≪≫ₗ (Rep.left_regular_hom_equiv _))
+  ≪≫ₗ (finsupp.llift A k k (fin n → G)).symm
+
+variables {n}
+
+/-- Given a `k`-linear `G`-representation `A`, `diagonal_hom_equiv` is a `k`-linear isomorphism of
+the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that this
+sends a morphism of representations `f : k[Gⁿ⁺¹] ⟶ A` to the function
+`(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).` -/
+lemma diagonal_hom_equiv_apply {A : Rep k G} (f : Rep.of_mul_action k G (fin (n + 1) → G) ⟶ A)
+  (x : fin n → G) : diagonal_hom_equiv n A f x = f.hom (finsupp.single (fin.partial_prod x) 1) :=
+begin
+  unfold diagonal_hom_equiv,
+  simpa only [linear_equiv.trans_apply, Rep.left_regular_hom_equiv_apply,
+    monoidal_closed.linear_hom_equiv_comm_hom, finsupp.llift_symm_apply, tensor_product.curry_apply,
+    linear.hom_congr_apply, iso.refl_hom, iso.trans_inv, Action.comp_hom, Module.comp_def,
+    linear_map.comp_apply, equiv_tensor_inv_def, representation.Rep_of_tprod_iso_inv_apply,
+    of_tensor_single (1 : G) (1 : k) (finsupp.single x (1 : k)), finsupp.lift_apply,
+    finsupp.sum_single_index, one_smul, zero_smul],
+end
+
+/-- Given a `k`-linear `G`-representation `A`, `diagonal_hom_equiv` is a `k`-linear isomorphism of
+the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that the
+inverse map sends a function `f : Gⁿ → A` to the representation morphism sending
+`(g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`, where `ρ` is the representation attached
+to `A`. -/
+lemma diagonal_hom_equiv_symm_apply {A : Rep k G} (f : (fin n → G) → A) (x : fin (n + 1) → G) :
+  ((diagonal_hom_equiv n A).symm f).hom (finsupp.single x 1)
+    = A.ρ (x 0) (f (λ (i : fin n), (x ↑i)⁻¹ * x i.succ)) :=
+begin
+  unfold diagonal_hom_equiv,
+  simp only [linear_equiv.trans_symm, linear_equiv.symm_symm, linear_equiv.trans_apply,
+    Rep.left_regular_hom_equiv_symm_apply, linear.hom_congr_symm_apply, Action.comp_hom,
+    iso.refl_inv, category.comp_id, Rep.monoidal_closed.linear_hom_equiv_comm_symm_hom,
+    iso.trans_hom, Module.comp_def, linear_map.comp_apply, representation.Rep_of_tprod_iso_apply,
+    equiv_tensor_def, to_tensor_single x (1 : k), tensor_product.uncurry_apply,
+    Rep.left_regular_hom_hom, finsupp.lift_apply, Rep.ihom_obj_ρ, representation.lin_hom_apply,
+    finsupp.sum_single_index, zero_smul, one_smul, Rep.of_ρ,
+    monoid_hom.one_apply, linear_map.one_apply, finsupp.llift_apply A k k],
+end
+
+end Rep
 variables (G)
 
 /-- The simplicial `G`-set sending `[n]` to `Gⁿ⁺¹` equipped with the diagonal action of `G`. -/
