From 8f6143476d00c3e462e5b41dc65bbf5c3a749d71 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 13:58:23 +0900 Subject: [PATCH 1/6] natural_left and natural_right --- .../Category/ModuleCat/Adjunctions.lean | 14 +-- Mathlib/CategoryTheory/Monoidal/Braided.lean | 17 ++- .../CategoryTheory/Monoidal/Free/Basic.lean | 16 ++- Mathlib/CategoryTheory/Monoidal/Functor.lean | 103 ++++++++++++++---- .../CategoryTheory/Monoidal/Functorial.lean | 49 +++++++-- .../CategoryTheory/Monoidal/Transport.lean | 8 +- .../RepresentationTheory/Action/Monoidal.lean | 38 ++++--- 7 files changed, 183 insertions(+), 62 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index eb84e96c61313..1e26354059210 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -186,15 +186,15 @@ theorem associativity (X Y Z : Type u) : -- In fact, it's strong monoidal, but we don't yet have a typeclass for that. /-- The free R-module functor is lax monoidal. -/ @[simps] -instance : LaxMonoidal.{u} (free R).obj where +instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom -- Send `R` to `PUnit →₀ R` - ε := ε R + (ε := ε R) -- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R` - μ X Y := (μ R X Y).hom - μ_natural {_} {_} {_} {_} f g := μ_natural R f g - left_unitality := left_unitality R - right_unitality := right_unitality R - associativity := associativity R + (μ := fun X Y => (μ R X Y).hom) + (μ_natural := fun {_} {_} {_} {_} f g ↦ μ_natural R f g) + (left_unitality := left_unitality R) + (right_unitality := right_unitality R) + (associativity := associativity R) instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩ diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean index b695987d6521e..03dd2419c9437 100644 --- a/Mathlib/CategoryTheory/Monoidal/Braided.lean +++ b/Mathlib/CategoryTheory/Monoidal/Braided.lean @@ -421,6 +421,18 @@ theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : simp only [assoc] #align category_theory.tensor_μ_natural CategoryTheory.tensor_μ_natural +@[reassoc] +theorem tensor_μ_natural_left {X₁ X₂ Y₁ Y₂ : C} (f₁: X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) : + ((f₁ ⊗ f₂) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) = + tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ ((f₁ ⊗ 𝟙 Z₁) ⊗ (f₂ ⊗ 𝟙 Z₂)) := by + convert tensor_μ_natural C f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1; simp + +@[reassoc] +theorem tensor_μ_natural_right (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) : + (𝟙 (Z₁ ⊗ Z₂) ⊗ (f₁ ⊗ f₂)) ≫ tensor_μ C (Z₁, Z₂) (Y₁, Y₂) = + tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ ((𝟙 Z₁ ⊗ f₁) ⊗ (𝟙 Z₂ ⊗ f₂)) := by + convert tensor_μ_natural C (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1; simp + theorem tensor_left_unitality (X₁ X₂ : C) : (λ_ (X₁ ⊗ X₂)).hom = ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫ @@ -566,8 +578,9 @@ theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) : def tensorMonoidal : MonoidalFunctor (C × C) C := { tensor C with ε := (λ_ (𝟙_ C)).inv - μ := fun X Y => tensor_μ C X Y - μ_natural := fun f g => tensor_μ_natural C f.1 f.2 g.1 g.2 + μ := tensor_μ C + μ_natural_left := fun f Z => tensor_μ_natural_left C f.1 f.2 Z.1 Z.2 + μ_natural_right := fun Z f => tensor_μ_natural_right C Z.1 Z.2 f.1 f.2 associativity := fun X Y Z => tensor_associativity C X.1 X.2 Y.1 Y.2 Z.1 Z.2 left_unitality := fun ⟨X₁, X₂⟩ => tensor_left_unitality C X₁ X₂ right_unitality := fun ⟨X₁, X₂⟩ => tensor_right_unitality C X₁ X₂ diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean index 24d89ec94ffd5..432c9356b3d34 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean @@ -341,13 +341,17 @@ def project : MonoidalFunctor (F C) D where map_comp := by rintro _ _ _ ⟨_⟩ ⟨_⟩; rfl ε := 𝟙 _ μ X Y := 𝟙 _ - μ_natural := @fun _ _ _ _ f g => by + μ_natural_left := fun f _ => by induction' f using Quotient.recOn - · induction' g using Quotient.recOn - · dsimp - simp - rfl - · rfl + · dsimp + simp + rfl + · rfl + μ_natural_right := fun _ f => by + induction' f using Quotient.recOn + · dsimp + simp + rfl · rfl #align category_theory.free_monoidal_category.project CategoryTheory.FreeMonoidalCategory.project diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean index b1a9c8b5ab8bb..eccbc1df584e2 100644 --- a/Mathlib/CategoryTheory/Monoidal/Functor.lean +++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean @@ -69,9 +69,13 @@ structure LaxMonoidalFunctor extends C ⥤ D where ε : 𝟙_ D ⟶ obj (𝟙_ C) /-- tensorator -/ μ : ∀ X Y : C, obj X ⊗ obj Y ⟶ obj (X ⊗ Y) - μ_natural : - ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), - (map f ⊗ map g) ≫ μ Y Y' = μ X X' ≫ map (f ⊗ g) := by + μ_natural_left : + ∀ {X Y : C} (f : X ⟶ Y) (X' : C), + (map f ⊗ 𝟙 (obj X')) ≫ μ Y X' = μ X X' ≫ map (f ⊗ 𝟙 X') := by + aesop_cat + μ_natural_right : + ∀ {X Y : C} (X' : C) (f : X ⟶ Y) , + (𝟙 (obj X') ⊗ map f) ≫ μ X' Y = μ X' X ≫ map (𝟙 X' ⊗ f) := by aesop_cat /-- associativity of the tensorator -/ associativity : @@ -93,7 +97,8 @@ structure LaxMonoidalFunctor extends C ⥤ D where initialize_simps_projections LaxMonoidalFunctor (+toFunctor, -obj, -map) --Porting note: was `[simp, reassoc.1]` -attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural +attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural_left +attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural_right attribute [simp] LaxMonoidalFunctor.left_unitality @@ -109,6 +114,59 @@ section variable {C D} +@[reassoc (attr := simp)] +theorem LaxMonoidalFunctor.μ_natural (F : LaxMonoidalFunctor C D) {X Y X' Y' : C} + (f : X ⟶ Y) (g : X' ⟶ Y') : + (F.map f ⊗ F.map g) ≫ F.μ Y Y' = F.μ X X' ≫ F.map (f ⊗ g) := by + rw [← tensor_id_comp_id_tensor_assoc] + rw [F.μ_natural_right, F.μ_natural_left_assoc] + rw [← F.map_comp, tensor_id_comp_id_tensor] + +/-- +A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of +`whiskerLeft` and `whiskerRight`. +-/ +@[simps] +def LaxMonoidalFunctor.ofTensorHom (F : C ⥤ D) + /- unit morphism -/ + (ε : 𝟙_ D ⟶ F.obj (𝟙_ C)) + /- tensorator -/ + (μ : ∀ X Y : C, F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)) + (μ_natural : + ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), + (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g) := by + aesop_cat) + /- associativity of the tensorator -/ + (associativity : + ∀ X Y Z : C, + (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom = + (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by + aesop_cat) + /- unitality -/ + (left_unitality : + ∀ X : C, (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom := + by aesop_cat) + (right_unitality : + ∀ X : C, (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom := + by aesop_cat) : + LaxMonoidalFunctor C D where + obj := F.obj + map := F.map + map_id := F.map_id + map_comp := F.map_comp + ε := ε + μ := μ + μ_natural_left := fun f X' => by + simp_rw [← F.map_id, μ_natural] + μ_natural_right := fun X' f => by + simp_rw [← F.map_id, μ_natural] + associativity := fun X Y Z => by + simp_rw [associativity] + left_unitality := fun X => by + simp_rw [left_unitality] + right_unitality := fun X => by + simp_rw [right_unitality] + --Porting note: was `[simp, reassoc.1]` @[reassoc (attr := simp)] theorem LaxMonoidalFunctor.left_unitality_inv (F : LaxMonoidalFunctor C D) (X : C) : @@ -320,10 +378,12 @@ def comp : LaxMonoidalFunctor.{v₁, v₃} C E := { F.toFunctor ⋙ G.toFunctor with ε := G.ε ≫ G.map F.ε μ := fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y) - μ_natural := @fun _ _ _ _ f g => by - simp only [Functor.comp_map, assoc] - rw [← Category.assoc, LaxMonoidalFunctor.μ_natural, Category.assoc, ← map_comp, ← map_comp, - ← LaxMonoidalFunctor.μ_natural] + μ_natural_left := by + intro X Y f X' + simp_rw [comp_obj, F.comp_map, μ_natural_left_assoc, assoc, ← G.map_comp, μ_natural_left] + μ_natural_right := by + intro X Y f X' + simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right] associativity := fun X Y Z => by dsimp rw [id_tensor_comp] @@ -482,17 +542,18 @@ end MonoidalFunctor /-- If we have a right adjoint functor `G` to a monoidal functor `F`, then `G` has a lax monoidal structure as well. -/ -@[simps] +@[simp] noncomputable def monoidalAdjoint (F : MonoidalFunctor C D) {G : D ⥤ C} (h : F.toFunctor ⊣ G) : - LaxMonoidalFunctor D C where - toFunctor := G - ε := h.homEquiv _ _ (inv F.ε) - μ X Y := h.homEquiv _ (X ⊗ Y) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)) - μ_natural := @fun X Y X' Y' f g => by + LaxMonoidalFunctor D C := LaxMonoidalFunctor.ofTensorHom + (F := G) + (ε := h.homEquiv _ _ (inv F.ε)) + (μ := fun X Y ↦ + h.homEquiv _ (X ⊗ Y) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y))) + (μ_natural := @fun X Y X' Y' f g => by rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq, assoc, IsIso.eq_inv_comp, ← F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ← - tensor_comp, Adjunction.counit_naturality, Adjunction.counit_naturality, tensor_comp] - associativity X Y Z := by + tensor_comp, Adjunction.counit_naturality, Adjunction.counit_naturality, tensor_comp]) + (associativity := fun X Y Z ↦ by dsimp only rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, Equiv.apply_eq_iff_eq, ← @@ -505,21 +566,21 @@ noncomputable def monoidalAdjoint (F : MonoidalFunctor C D) {G : D ⥤ C} (h : F tensor_comp_assoc, id_comp, id_comp, h.homEquiv_unit, h.homEquiv_unit, Functor.map_comp, assoc, assoc, h.counit_naturality, h.left_triangle_components_assoc, Functor.map_comp, assoc, h.counit_naturality, h.left_triangle_components_assoc] - simp - left_unitality X := by + simp) + (left_unitality := fun X ↦ by rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq, h.homEquiv_counit, F.map_leftUnitor, h.homEquiv_unit, assoc, assoc, assoc, F.map_tensor, assoc, assoc, IsIso.hom_inv_id_assoc, ← tensor_comp_assoc, Functor.map_id, id_comp, Functor.map_comp, assoc, h.counit_naturality, h.left_triangle_components_assoc, ← leftUnitor_naturality, ← tensor_comp_assoc, id_comp, comp_id] - simp - right_unitality X := by + simp) + (right_unitality := fun X ↦ by rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq, h.homEquiv_counit, F.map_rightUnitor, assoc, assoc, ← rightUnitor_naturality, ← tensor_comp_assoc, comp_id, id_comp, h.homEquiv_unit, F.map_tensor, assoc, assoc, assoc, IsIso.hom_inv_id_assoc, Functor.map_comp, Functor.map_id, ← tensor_comp_assoc, assoc, h.counit_naturality, h.left_triangle_components_assoc, id_comp] - simp + simp) #align category_theory.monoidal_adjoint CategoryTheory.monoidalAdjoint /-- If a monoidal functor `F` is an equivalence of categories then its inverse is also monoidal. -/ diff --git a/Mathlib/CategoryTheory/Monoidal/Functorial.lean b/Mathlib/CategoryTheory/Monoidal/Functorial.lean index 2e729969ef121..06c3599861972 100644 --- a/Mathlib/CategoryTheory/Monoidal/Functorial.lean +++ b/Mathlib/CategoryTheory/Monoidal/Functorial.lean @@ -55,11 +55,14 @@ class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where ε : 𝟙_ D ⟶ F (𝟙_ C) /-- tensorator -/ μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y) - /-- naturality -/ - μ_natural : - ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), - (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by - aesop_cat + μ_natural_left : + ∀ {X Y : C} (f : X ⟶ Y) (X' : C), + (map F f ⊗ 𝟙 (F X')) ≫ μ Y X' = μ X X' ≫ map F (f ⊗ 𝟙 X') := by + aesop_cat + μ_natural_right : + ∀ {X Y : C} (X' : C) (f : X ⟶ Y) , + (𝟙 (F X') ⊗ map F f) ≫ μ X' Y = μ X' X ≫ map F (𝟙 X' ⊗ f) := by + aesop_cat /-- associativity of the tensorator -/ associativity : ∀ X Y Z : C, @@ -74,9 +77,39 @@ class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where aesop_cat #align category_theory.lax_monoidal CategoryTheory.LaxMonoidal -attribute [simp] LaxMonoidal.μ_natural - -attribute [simp] LaxMonoidal.μ_natural +/-- An unbundled description of lax monoidal functors. -/ +abbrev LaxMonoidal.ofTensorHom (F : C → D) [Functorial.{v₁, v₂} F] + /- unit morphism -/ + (ε : 𝟙_ D ⟶ F (𝟙_ C)) + /- tensorator -/ + (μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)) + /- naturality -/ + (μ_natural : + ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), + (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by + aesop_cat) + /- associativity of the tensorator -/ + (associativity : + ∀ X Y Z : C, + (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom = + (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by + aesop_cat) + /- left unitality -/ + (left_unitality : ∀ X : C, (λ_ (F X)).hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom := by + aesop_cat) + /- right unitality -/ + (right_unitality : ∀ X : C, (ρ_ (F X)).hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom := by + aesop_cat) : + LaxMonoidal.{v₁, v₂} F where + ε := ε + μ := μ + μ_natural_left f X := by intros; simpa using μ_natural f (𝟙 X) + μ_natural_right X f := by intros; simpa using μ_natural (𝟙 X) f + associativity X Y Z := by intros; simpa using associativity X Y Z + left_unitality X := by intros; simpa using left_unitality X + right_unitality X := by intros; simpa using right_unitality X + +attribute [simp, nolint simpNF] LaxMonoidal.μ_natural_left LaxMonoidal.μ_natural_right -- The unitality axioms cannot be used as simp lemmas because they require -- higher-order matching to figure out the `F` and `X` from `F X`. diff --git a/Mathlib/CategoryTheory/Monoidal/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean index c0f3e4a6b90d1..6afb99b0e151e 100644 --- a/Mathlib/CategoryTheory/Monoidal/Transport.lean +++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean @@ -150,7 +150,8 @@ def fromInduced [MonoidalCategoryStruct D] (F : D ⥤ C) [Faithful F] { toFunctor := F ε := fData.εIso.hom μ := fun X Y => (fData.μIso X Y).hom - μ_natural := by cases fData; aesop_cat + μ_natural_left := by cases fData; aesop_cat + μ_natural_right := by cases fData; aesop_cat associativity := by cases fData; aesop_cat left_unitality := by cases fData; aesop_cat right_unitality := by cases fData; aesop_cat } @@ -224,9 +225,8 @@ def toTransported (e : C ≌ D) : MonoidalFunctor C (Transported e) := monoidalInverse (fromTransported e) #align category_theory.monoidal.to_transported CategoryTheory.Monoidal.toTransported -instance (e : C ≌ D) : IsEquivalence (toTransported e).toFunctor := by - dsimp [toTransported] - infer_instance +instance (e : C ≌ D) : IsEquivalence (toTransported e).toFunctor := + inferInstanceAs (IsEquivalence e.functor) /-- The unit isomorphism upgrades to a monoidal isomorphism. -/ @[simps! hom inv] diff --git a/Mathlib/RepresentationTheory/Action/Monoidal.lean b/Mathlib/RepresentationTheory/Action/Monoidal.lean index ef0eb9e025b10..df738c059cf51 100644 --- a/Mathlib/RepresentationTheory/Action/Monoidal.lean +++ b/Mathlib/RepresentationTheory/Action/Monoidal.lean @@ -384,32 +384,42 @@ namespace CategoryTheory.MonoidalFunctor open Action variable {W : Type (u + 1)} [LargeCategory W] [MonoidalCategory V] [MonoidalCategory W] - (F : MonoidalFunctor V W) (G : MonCat.{u}) -/-- A monoidal functor induces a monoidal functor between +/-- A lax monoidal functor induces a lax monoidal functor between the categories of `G`-actions within those categories. -/ -@[simps] -def mapAction : MonoidalFunctor (Action V G) (Action W G) where - toFunctor := F.toFunctor.mapAction G - ε := +@[simps!] +def mapActionLax (F : LaxMonoidalFunctor V W) (G : MonCat.{u}) : + LaxMonoidalFunctor (Action V G) (Action W G) := .ofTensorHom + (F := F.toFunctor.mapAction G) + (ε := { hom := F.ε comm := fun g => by dsimp [FunctorCategoryEquivalence.inverse, Functor.mapAction] - rw [Category.id_comp, F.map_id, Category.comp_id] } - μ := fun X Y => + rw [Category.id_comp, F.map_id, Category.comp_id] }) + (μ := fun X Y => { hom := F.μ X.V Y.V - comm := fun g => F.toLaxMonoidalFunctor.μ_natural (X.ρ g) (Y.ρ g) } + comm := fun g => F.μ_natural (X.ρ g) (Y.ρ g) }) -- using `dsimp` before `simp` speeds these up - μ_natural {X Y X' Y'} f g := by ext; dsimp; simp - associativity X Y Z := by ext; dsimp; simp - left_unitality X := by ext; dsimp; simp - right_unitality X := by + (μ_natural := @fun {X Y X' Y'} f g ↦ by ext; dsimp; simp) + (associativity := fun X Y Z ↦ by ext; dsimp; simp) + (left_unitality := fun X ↦ by ext; dsimp; simp) + (right_unitality := fun X ↦ by ext dsimp simp only [MonoidalCategory.rightUnitor_conjugation, LaxMonoidalFunctor.right_unitality, Category.id_comp, Category.assoc, LaxMonoidalFunctor.right_unitality_inv_assoc, Category.comp_id, Iso.hom_inv_id] - rw [← F.map_comp, Iso.inv_hom_id, F.map_id, Category.comp_id] + rw [← F.map_comp, Iso.inv_hom_id, F.map_id, Category.comp_id]) + +variable (F : MonoidalFunctor V W) (G : MonCat.{u}) + +/-- A monoidal functor induces a monoidal functor between +the categories of `G`-actions within those categories. -/ +@[simps!] +def mapAction : MonoidalFunctor (Action V G) (Action W G) := + { mapActionLax F.toLaxMonoidalFunctor G with + ε_isIso := by dsimp [mapActionLax]; infer_instance + μ_isIso := by dsimp [mapActionLax]; infer_instance } set_option linter.uppercaseLean3 false in #align category_theory.monoidal_functor.map_Action CategoryTheory.MonoidalFunctor.mapAction From bb22bf4a5d5c0b740ff8a1575a7c6a0f7c6b9f73 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 14:11:15 +0900 Subject: [PATCH 2/6] fix --- .../CategoryTheory/Bicategory/SingleObj.lean | 6 ++++- Mathlib/CategoryTheory/Monoidal/Limits.lean | 26 +++++++++---------- 2 files changed, 18 insertions(+), 14 deletions(-) diff --git a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean index a03f03a51fc63..af6f3b9fb5e0d 100644 --- a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean +++ b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean @@ -86,7 +86,11 @@ def endMonoidalStarFunctor : MonoidalFunctor (EndMonoidal (MonoidalSingleObj.sta map f := f ε := 𝟙 _ μ X Y := 𝟙 _ - μ_natural f g := by + μ_natural_left f g := by + simp_rw [Category.id_comp, Category.comp_id] + -- Should we provide further simp lemmas so this goal becomes visible? + exact (tensor_id_comp_id_tensor _ _).symm + μ_natural_right f g := by simp_rw [Category.id_comp, Category.comp_id] -- Should we provide further simp lemmas so this goal becomes visible? exact (tensor_id_comp_id_tensor _ _).symm diff --git a/Mathlib/CategoryTheory/Monoidal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Limits.lean index 7eb9628895f66..b5553b1312089 100644 --- a/Mathlib/CategoryTheory/Monoidal/Limits.lean +++ b/Mathlib/CategoryTheory/Monoidal/Limits.lean @@ -47,24 +47,24 @@ theorem limitFunctorial_map {F G : J ⥤ C} (α : F ⟶ G) : variable [MonoidalCategory.{v} C] @[simps] -instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where - ε := +instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F := .ofTensorHom + (ε := limit.lift _ { pt := _ - π := { app := fun j => 𝟙 _ } } - μ F G := + π := { app := fun j => 𝟙 _ } }) + (μ := fun F G => limit.lift (F ⊗ G) { pt := limit F ⊗ limit G π := { app := fun j => limit.π F j ⊗ limit.π G j naturality := fun j j' f => by dsimp - simp only [Category.id_comp, ← tensor_comp, limit.w] } } - μ_natural f g := by + simp only [Category.id_comp, ← tensor_comp, limit.w] } }) + (μ_natural:= fun f g => by ext; dsimp simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.tensorHom_app, limit.lift_map, - NatTrans.comp_app, Category.assoc, ← tensor_comp, limMap_π] - associativity X Y Z := by + NatTrans.comp_app, Category.assoc, ← tensor_comp, limMap_π]) + (associativity := fun X Y Z => by ext j; dsimp simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.associator_hom_app, limit.lift_map, NatTrans.comp_app, Category.assoc] @@ -78,8 +78,8 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where slice_rhs 2 3 => rw [← id_tensor_comp, limit.lift_π] dsimp - dsimp; simp - left_unitality X := by + dsimp; simp) + (left_unitality := fun X => by ext j; dsimp simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt, Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj, @@ -90,8 +90,8 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where erw [limit.lift_π] dsimp slice_rhs 2 3 => rw [leftUnitor_naturality] - simp - right_unitality X := by + simp) + (right_unitality := fun X => by ext j; dsimp simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt, Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj, @@ -102,7 +102,7 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where erw [limit.lift_π] dsimp slice_rhs 2 3 => rw [rightUnitor_naturality] - simp + simp) #align category_theory.limits.limit_lax_monoidal CategoryTheory.Limits.limitLaxMonoidal /-- The limit functor `F ↦ limit F` bundled as a lax monoidal functor. -/ From 77289772e7c683d9c4a8c1f57f13619dcddd9986 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 14:22:25 +0900 Subject: [PATCH 3/6] fix --- Mathlib/CategoryTheory/Monoidal/End.lean | 11 ++++++++-- .../Monoidal/Types/Coyoneda.lean | 20 +++++++++---------- 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean index a09755c78db1e..c426b59108526 100644 --- a/Mathlib/CategoryTheory/Monoidal/End.lean +++ b/Mathlib/CategoryTheory/Monoidal/End.lean @@ -97,11 +97,18 @@ def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C { tensoringRight C with ε := (rightUnitorNatIso C).inv μ := fun X Y => { app := fun Z => (α_ Z X Y).hom } - μ_natural := fun f g => by + μ_natural_left := fun f X => by ext Z dsimp - simp only [← id_tensor_comp_tensor_id g f, id_tensor_comp, ← tensor_id, Category.assoc, + simp only [← id_tensor_comp_tensor_id f (𝟙 X), id_tensor_comp, ← tensor_id, Category.assoc, associator_naturality, associator_naturality_assoc] + simp only [tensor_id, Category.id_comp] + μ_natural_right := fun X g => by + ext Z + dsimp + simp only [← id_tensor_comp_tensor_id (𝟙 X) g, id_tensor_comp, ← tensor_id, Category.assoc, + associator_naturality, associator_naturality_assoc] + simp only [tensor_id, Category.comp_id] associativity := fun X Y Z => by ext W simp [pentagon] diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean index 6638151e9fc14..e421ed3e56026 100644 --- a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean +++ b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean @@ -36,23 +36,23 @@ open MonoidalCategory /-- `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`. -/ noncomputable def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] : - LaxMonoidalFunctor C (Type v) := - { coyoneda.obj (op (𝟙_ C)) with - ε := fun _p => 𝟙 _ - μ := fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ p.2) - μ_natural := by aesop_cat - associativity := fun X Y Z => by + LaxMonoidalFunctor C (Type v) := .ofTensorHom + (F := coyoneda.obj (op (𝟙_ C))) + (ε := fun _p => 𝟙 _) + (μ := fun X Y p => (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ p.2)) + (μ_natural := by aesop_cat) + (associativity := fun X Y Z => by ext ⟨⟨f, g⟩, h⟩; dsimp at f g h dsimp; simp only [Iso.cancel_iso_inv_left, Category.assoc] conv_lhs => rw [← Category.id_comp h, tensor_comp, Category.assoc, associator_naturality, ← Category.assoc, unitors_inv_equal, triangle_assoc_comp_right_inv] - conv_rhs => rw [← Category.id_comp f, tensor_comp] - left_unitality := by aesop_cat - right_unitality := fun X => by + conv_rhs => rw [← Category.id_comp f, tensor_comp]) + (left_unitality := by aesop_cat) + (right_unitality := fun X => by ext ⟨f, ⟨⟩⟩; dsimp at f dsimp; simp only [Category.assoc] - rw [rightUnitor_naturality, unitors_inv_equal, Iso.inv_hom_id_assoc] } + rw [rightUnitor_naturality, unitors_inv_equal, Iso.inv_hom_id_assoc]) #align category_theory.coyoneda_tensor_unit CategoryTheory.coyonedaTensorUnit end CategoryTheory From e6717dc41eef93deaf930ff6c6c6d0ebc8b19046 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 14:26:45 +0900 Subject: [PATCH 4/6] add comment --- Mathlib/CategoryTheory/Monoidal/End.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean index c426b59108526..04b6ffaff04e4 100644 --- a/Mathlib/CategoryTheory/Monoidal/End.lean +++ b/Mathlib/CategoryTheory/Monoidal/End.lean @@ -97,6 +97,7 @@ def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C { tensoringRight C with ε := (rightUnitorNatIso C).inv μ := fun X Y => { app := fun Z => (α_ Z X Y).hom } + -- The proof will be automated after merging #6307. μ_natural_left := fun f X => by ext Z dsimp From c182a28d6d9909fa91cf1d3cab08553238c1c0af Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 14:26:49 +0900 Subject: [PATCH 5/6] fix --- Mathlib/CategoryTheory/Shift/Basic.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index 62863ff34b0b9..6cc9f67df5a7d 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -129,8 +129,13 @@ def hasShiftMk (h : ShiftMkCore C A) : HasShift C A := ⟨{ Discrete.functor h.F with ε := h.zero.inv μ := fun m n => (h.add m.as n.as).inv - μ_natural := by - rintro ⟨X⟩ ⟨Y⟩ ⟨X'⟩ ⟨Y'⟩ ⟨⟨⟨rfl⟩⟩⟩ ⟨⟨⟨rfl⟩⟩⟩ + μ_natural_left := by + rintro ⟨X⟩ ⟨Y⟩ ⟨⟨⟨rfl⟩⟩⟩ ⟨X'⟩ + ext + dsimp + simp + μ_natural_right := by + rintro ⟨X⟩ ⟨Y⟩ ⟨X'⟩ ⟨⟨⟨rfl⟩⟩⟩ ext dsimp simp From 4b0ed2e155e9d518dbd4e7576604d28ec613af25 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 25 Jan 2024 14:29:49 +0900 Subject: [PATCH 6/6] add comment --- Mathlib/CategoryTheory/Bicategory/SingleObj.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean index af6f3b9fb5e0d..931fb282c6e6f 100644 --- a/Mathlib/CategoryTheory/Bicategory/SingleObj.lean +++ b/Mathlib/CategoryTheory/Bicategory/SingleObj.lean @@ -86,6 +86,7 @@ def endMonoidalStarFunctor : MonoidalFunctor (EndMonoidal (MonoidalSingleObj.sta map f := f ε := 𝟙 _ μ X Y := 𝟙 _ + -- The proof will be automated after merging #6307. μ_natural_left f g := by simp_rw [Category.id_comp, Category.comp_id] -- Should we provide further simp lemmas so this goal becomes visible?