feat(representation_theory/Rep): describe monoidal closed structure (#…

…18148)

The monoidal closed structure on `Rep k G` defines an internal hom of representations; we show this agrees with `representation.lin_hom`. Moreover, the maps defining the hom-set bijection come from the tensor-hom adjunction for $k$-modules.

src/algebra/category/Module/monoidal.lean

@@ -307,6 +307,9 @@ instance : monoidal_closed (Module.{u} R) :=
       adj := adjunction.mk_of_hom_equiv
       { hom_equiv := λ N P, monoidal_closed_hom_equiv M N P, } } } }
 
+lemma ihom_map_apply {M N P : Module.{u} R} (f : N ⟶ P) (g : Module.of R (M ⟶ N)) :
+  (ihom M).map f g = g ≫ f := rfl
+
 -- I can't seem to express the function coercion here without writing `@coe_fn`.
 @[simp]
 lemma monoidal_closed_curry {M N P : Module.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
@@ -318,6 +321,27 @@ rfl
 lemma monoidal_closed_uncurry {M N P : Module.{u} R}
   (f : N ⟶ (M ⟶[Module.{u} R] P)) (x : M) (y : N) :
   monoidal_closed.uncurry f (x ⊗ₜ[R] y) = (@coe_fn _ _ linear_map.has_coe_to_fun (f y)) x :=
-by { simp only [monoidal_closed.uncurry, ihom.adjunction, is_left_adjoint.adj], simp, }
+rfl
+
+/-- Describes the counit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this
+should give a map `M ⊗ Hom(M, N) ⟶ N`, so we flip the order of the arguments in the identity map
+`Hom(M, N) ⟶ (M ⟶ N)` and uncurry the resulting map `M ⟶ Hom(M, N) ⟶ N.` -/
+lemma ihom_ev_app (M N : Module.{u} R) :
+  (ihom.ev M).app N = tensor_product.uncurry _ _ _ _ linear_map.id.flip :=
+begin
+  ext,
+  exact Module.monoidal_closed_uncurry _ _ _,
+end
+
+/-- Describes the unit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this should
+define a map `N ⟶ Hom(M, M ⊗ N)`, which is given by flipping the arguments in the natural
+`R`-bilinear map `M ⟶ N ⟶ M ⊗ N`. -/
+lemma ihom_coev_app (M N : Module.{u} R) :
+  (ihom.coev M).app N = (tensor_product.mk _ _ _).flip :=
+rfl
+
+lemma monoidal_closed_pre_app {M N : Module.{u} R} (P : Module.{u} R) (f : N ⟶ M) :
+  (monoidal_closed.pre f).app P = linear_map.lcomp R _ f :=
+rfl
 
 end Module

src/algebra/category/Mon/basic.lean

@@ -80,6 +80,8 @@ instance (M : Mon) : monoid M := M.str
 
 @[simp, to_additive] lemma coe_of (R : Type u) [monoid R] : (Mon.of R : Type u) = R := rfl
 
+@[to_additive] instance {G : Type*} [group G] : group (Mon.of G) := by assumption
+
 end Mon
 
 /-- The category of commutative monoids and monoid morphisms. -/

src/category_theory/closed/functor_category.lean

@@ -70,4 +70,13 @@ with the pointwise monoidal structure, is monoidal closed. -/
 @[simps] instance monoidal_closed : monoidal_closed (D ⥤ C) :=
 { closed' := by apply_instance }
 
+lemma ihom_map (F : D ⥤ C) {G H : D ⥤ C} (f : G ⟶ H) :
+  (ihom F).map f = (closed_ihom F).map f := rfl
+
+lemma ihom_ev_app (F G : D ⥤ C) :
+  (ihom.ev F).app G = (closed_counit F).app G := rfl
+
+lemma ihom_coev_app (F G : D ⥤ C) :
+  (ihom.coev F).app G = (closed_unit F).app G := rfl
+
 end category_theory.functor

src/category_theory/closed/monoidal.lean

@@ -264,6 +264,32 @@ def of_equiv (F : monoidal_functor C D) [is_equivalence F.to_functor] [h : monoi
       exact adjunction.left_adjoint_of_nat_iso i,
     end } }
 
+/-- Suppose we have a monoidal equivalence `F : C ≌ D`, with `D` monoidal closed. We can pull the
+monoidal closed instance back along the equivalence. For `X, Y, Z : C`, this lemma describes the
+resulting currying map `Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z))`. (`X ⟶[C] Z` is defined to be
+`F⁻¹(F(X) ⟶[D] F(Z))`, so currying in `C` is given by essentially conjugating currying in
+`D` by `F.`) -/
+lemma of_equiv_curry_def (F : monoidal_functor C D) [is_equivalence F.to_functor]
+  [h : monoidal_closed D] {X Y Z : C} (f : X ⊗ Y ⟶ Z) :
+  @monoidal_closed.curry _ _ _ _ _ _ ((monoidal_closed.of_equiv F).1 _) f =
+  (F.1.1.adjunction.hom_equiv Y ((ihom _).obj _)) (monoidal_closed.curry
+  (F.1.1.inv.adjunction.hom_equiv (F.1.1.obj X ⊗ F.1.1.obj Y) Z
+  ((comp_inv_iso (F.comm_tensor_left X)).hom.app Y ≫ f))) := rfl
+
+/-- Suppose we have a monoidal equivalence `F : C ≌ D`, with `D` monoidal closed. We can pull the
+monoidal closed instance back along the equivalence. For `X, Y, Z : C`, this lemma describes the
+resulting uncurrying map `Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z)`. (`X ⟶[C] Z` is
+defined to be `F⁻¹(F(X) ⟶[D] F(Z))`, so uncurrying in `C` is given by essentially conjugating
+uncurrying in `D` by `F.`) -/
+lemma of_equiv_uncurry_def
+  (F : monoidal_functor C D) [is_equivalence F.to_functor] [h : monoidal_closed D] {X Y Z : C}
+  (f : Y ⟶ (@ihom _ _ _ X $ (monoidal_closed.of_equiv F).1 X).obj Z) :
+  @monoidal_closed.uncurry _ _ _ _ _ _ ((monoidal_closed.of_equiv F).1 _) f =
+  (comp_inv_iso (F.comm_tensor_left X)).inv.app Y ≫ (F.1.1.inv.adjunction.hom_equiv
+  (F.1.1.obj X ⊗ F.1.1.obj Y) Z).symm (monoidal_closed.uncurry
+  ((F.1.1.adjunction.hom_equiv Y ((ihom (F.1.1.obj X)).obj (F.1.1.obj Z))).symm f)) :=
+rfl
+
 end of_equiv
 
 end monoidal_closed

src/representation_theory/Action.lean

@@ -206,6 +206,12 @@ def functor_category_equivalence : Action V G ≌ (single_obj G ⥤ V) :=
 
 attribute [simps] functor_category_equivalence
 
+lemma functor_category_equivalence.functor_def :
+  (functor_category_equivalence V G).functor = functor_category_equivalence.functor := rfl
+
+lemma functor_category_equivalence.inverse_def :
+  (functor_category_equivalence V G).inverse = functor_category_equivalence.inverse := rfl
+
 instance [has_finite_products V] : has_finite_products (Action V G) :=
 { out := λ n, adjunction.has_limits_of_shape_of_equivalence
     (Action.functor_category_equivalence _ _).functor }
@@ -453,6 +459,59 @@ monoidal.from_transported (Action.functor_category_equivalence _ _).symm
 instance : is_equivalence ((functor_category_monoidal_equivalence V G).to_functor) :=
 by { change is_equivalence (Action.functor_category_equivalence _ _).functor, apply_instance, }
 
+@[simp] lemma functor_category_monoidal_equivalence.μ_app (A B : Action V G) :
+  ((functor_category_monoidal_equivalence V G).μ A B).app punit.star = 𝟙 _ :=
+begin
+  dunfold functor_category_monoidal_equivalence,
+  simp only [monoidal.from_transported_to_lax_monoidal_functor_μ],
+  show (𝟙 A.V ⊗ 𝟙 B.V) ≫ 𝟙 (A.V ⊗ B.V) ≫ (𝟙 A.V ⊗ 𝟙 B.V) = 𝟙 (A.V ⊗ B.V),
+  simp only [monoidal_category.tensor_id, category.comp_id],
+end
+
+@[simp] lemma functor_category_monoidal_equivalence.μ_iso_inv_app (A B : Action V G) :
+  ((functor_category_monoidal_equivalence V G).μ_iso A B).inv.app punit.star = 𝟙 _ :=
+begin
+  rw [←nat_iso.app_inv, ←is_iso.iso.inv_hom],
+  refine is_iso.inv_eq_of_hom_inv_id _,
+  rw [category.comp_id, nat_iso.app_hom, monoidal_functor.μ_iso_hom,
+    functor_category_monoidal_equivalence.μ_app],
+end
+
+@[simp] lemma functor_category_monoidal_equivalence.ε_app :
+  (functor_category_monoidal_equivalence V G).ε.app punit.star = 𝟙 _ :=
+begin
+  dunfold functor_category_monoidal_equivalence,
+  simp only [monoidal.from_transported_to_lax_monoidal_functor_ε],
+  show 𝟙 (monoidal_category.tensor_unit V) ≫ _ = 𝟙 (monoidal_category.tensor_unit V),
+  rw [nat_iso.is_iso_inv_app, category.id_comp],
+  exact is_iso.inv_id,
+end
+
+@[simp] lemma functor_category_monoidal_equivalence.inv_counit_app_hom (A : Action V G) :
+  ((functor_category_monoidal_equivalence _ _).inv.adjunction.counit.app A).hom = 𝟙 _ :=
+rfl
+
+@[simp] lemma functor_category_monoidal_equivalence.counit_app (A : single_obj G ⥤ V) :
+  ((functor_category_monoidal_equivalence _ _).adjunction.counit.app A).app punit.star = 𝟙 _ := rfl
+
+@[simp] lemma functor_category_monoidal_equivalence.inv_unit_app_app
+  (A : single_obj G ⥤ V) :
+  ((functor_category_monoidal_equivalence _ _).inv.adjunction.unit.app A).app
+  punit.star = 𝟙 _ := rfl
+
+@[simp] lemma functor_category_monoidal_equivalence.unit_app_hom (A : Action V G) :
+  ((functor_category_monoidal_equivalence _ _).adjunction.unit.app A).hom = 𝟙 _ :=
+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_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_equivalence.inverse.map f := rfl
+
 variables (H : Group.{u})
 
 instance [right_rigid_category V] : right_rigid_category (single_obj (H : Mon.{u}) ⥤ V) :=

src/representation_theory/Rep.lean

@@ -9,6 +9,7 @@ import algebra.category.Module.abelian
 import algebra.category.Module.colimits
 import algebra.category.Module.monoidal
 import algebra.category.Module.adjunctions
+import category_theory.closed.functor_category
 
 /-!
 # `Rep k G` is the category of `k`-linear representations of `G`.
@@ -39,8 +40,9 @@ instance (k G : Type u) [comm_ring k] [monoid G] : linear k (Rep k G) :=
 by apply_instance
 
 namespace Rep
-
-variables {k G : Type u} [comm_ring k] [monoid G]
+variables {k G : Type u} [comm_ring k]
+section
+variables [monoid G]
 
 instance : has_coe_to_sort (Rep k G) (Type u) := concrete_category.has_coe_to_sort _
 
@@ -116,6 +118,97 @@ noncomputable def linearization_of_mul_action_iso (n : ℕ) :
     ≅ of_mul_action k G (fin n → G) := iso.refl _
 
 end linearization
+end
+section
+open Action
+variables [group G] (A B C : Rep k G)
+
+noncomputable instance : monoidal_closed (Rep k G) :=
+monoidal_closed.of_equiv (functor_category_monoidal_equivalence _ _)
+
+/-- Explicit description of the 'internal Hom' `iHom(A, B)` of two representations `A, B`:
+this is `F⁻¹(iHom(F(A), F(B)))`, where `F` is an equivalence
+`Rep k G ≌ (single_obj G ⥤ Module k)`. Just used to prove `Rep.ihom_obj_ρ`. -/
+lemma ihom_obj_ρ_def :
+  ((ihom A).obj B).ρ = (functor_category_equivalence.inverse.obj
+  ((functor_category_equivalence.functor.obj A).closed_ihom.obj
+  (functor_category_equivalence.functor.obj B))).ρ := rfl
+
+/-- Given `k`-linear `G`-representations `(A, ρ₁), (B, ρ₂)`, the 'internal Hom' is the
+representation on `Homₖ(A, B)` sending `g : G` and `f : A →ₗ[k] B` to `(ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹)`. -/
+@[simp] lemma ihom_obj_ρ :
+  ((ihom A).obj B).ρ = A.ρ.lin_hom B.ρ :=
+begin
+  refine monoid_hom.ext (λ g, _),
+  simpa only [ihom_obj_ρ_def, functor_category_equivalence.inverse_obj_ρ_apply,
+    functor.closed_ihom_obj_map, ←functor.map_inv, single_obj.inv_as_inv],
+end
+
+@[simp] lemma ihom_map_hom {B C : Rep k G} (f : B ⟶ C) :
+  ((ihom A).map f).hom = linear_map.llcomp k A B C f.hom :=
+rfl
+
+/-- Unfolds the unit in the adjunction `A ⊗ - ⊣ iHom(A, -)`; just used to prove
+`Rep.ihom_coev_app_hom`. -/
+lemma ihom_coev_app_def :
+  (ihom.coev A).app B = functor_category_equivalence.unit_iso.hom.app B ≫
+  functor_category_equivalence.inverse.map
+  ((functor_category_equivalence.functor.obj A).closed_unit.app _ ≫
+  (functor_category_equivalence.functor.obj A).closed_ihom.map
+  ((functor_category_monoidal_equivalence (Module.{u} k) (Mon.of G)).μ A B)) :=
+rfl
+
+/-- Describes the unit in the adjunction `A ⊗ - ⊣ iHom(A, -)`; given another `k`-linear
+`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 :=
+begin
+  refine linear_map.ext (λ x, linear_map.ext (λ y, _)),
+  simpa only [ihom_coev_app_def, functor.map_comp, comp_hom,
+    functor_category_equivalence.inverse_map_hom, functor.closed_ihom_map_app,
+    functor_category_monoidal_equivalence.μ_app],
+end
+
+variables {A B C}
+
+/-- Given a `k`-linear `G`-representation `A`, the adjunction `A ⊗ - ⊣ iHom(A, -)` defines a
+bijection `Hom(A ⊗ B, C) ≃ Hom(B, iHom(A, C))` for all `B, C`. Given `f : A ⊗ B ⟶ C`, this lemma
+describes the `k`-linear map underlying `f`'s image under the bijection. It is given by currying the
+`k`-linear map underlying `f`, giving a map `A →ₗ[k] B →ₗ[k] C`, then flipping the arguments. -/
+@[simp] lemma monoidal_closed_curry_hom (f : A ⊗ B ⟶ C) :
+  (monoidal_closed.curry f).hom = (tensor_product.curry f.hom).flip :=
+begin
+  rw [monoidal_closed.curry_eq, comp_hom, ihom_coev_app_hom],
+  refl,
+end
+
+/-- Given a `k`-linear `G`-representation `A`, the adjunction `A ⊗ - ⊣ iHom(A, -)` defines a
+bijection `Hom(A ⊗ B, C) ≃ Hom(B, iHom(A, C))` for all `B, C`. Given `f : B ⟶ iHom(A, C)`, this
+lemma describes the `k`-linear map underlying `f`'s image under the bijection. It is given by
+flipping the arguments of the `k`-linear map underlying `f`, giving a map `A →ₗ[k] B →ₗ[k] C`, then
+uncurrying. -/
+@[simp] lemma monoidal_closed_uncurry_hom (f : B ⟶ (ihom A).obj C) :
+  (monoidal_closed.uncurry f).hom = tensor_product.uncurry _ _ _ _ f.hom.flip :=
+begin
+  simp only [monoidal_closed.of_equiv_uncurry_def, comp_inv_iso_inv_app,
+    monoidal_functor.comm_tensor_left_inv_app, comp_hom,
+    functor_category_monoidal_equivalence.inverse_map, functor_category_equivalence.inverse_map_hom,
+    functor_category_monoidal_equivalence.μ_iso_inv_app],
+  ext,
+  refl,
+end
+
+/-- Describes the counit in the adjunction `A ⊗ - ⊣ iHom(A, -)`; given another `k`-linear
+`G`-representation `B,` the `k`-linear map underlying the resulting morphism `A ⊗ iHom(A, B) ⟶ B`
+is given by uncurrying the map `A →ₗ[k] (A →ₗ[k] B) →ₗ[k] B` defined by flipping the arguments in
+the identity map on `Homₖ(A, B).` -/
+@[simp] lemma ihom_ev_app_hom : Action.hom.hom ((ihom.ev A).app B) =
+  tensor_product.uncurry _ _ _ _ linear_map.id.flip :=
+monoidal_closed_uncurry_hom _
+
+end
 end Rep
 
 /-!