diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean index 133a748199f31..1750fbe37fcdf 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean @@ -61,6 +61,16 @@ def tensorHom {M N M' N' : ModuleCat R} (f : M ⟶ N) (g : M' ⟶ N') : TensorProduct.map f g #align Module.monoidal_category.tensor_hom ModuleCat.MonoidalCategory.tensorHom +/-- (implementation) left whiskering for R-modules -/ +def whiskerLeft (M : ModuleCat R) {N₁ N₂ : ModuleCat R} (f : N₁ ⟶ N₂) : + tensorObj M N₁ ⟶ tensorObj M N₂ := + f.lTensor M + +/-- (implementation) right whiskering for R-modules -/ +def whiskerRight {M₁ M₂ : ModuleCat R} (f : M₁ ⟶ M₂) (N : ModuleCat R) : + tensorObj M₁ N ⟶ tensorObj M₂ N := + f.rTensor N + theorem tensor_id (M N : ModuleCat R) : tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (M ⊗ N)) := by -- Porting note: even with high priority ext fails to find this apply TensorProduct.ext @@ -187,22 +197,24 @@ end MonoidalCategory open MonoidalCategory -instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) where +instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom -- data - tensorObj := tensorObj - tensorHom := @tensorHom _ _ - tensorUnit' := ModuleCat.of R R - associator := associator - leftUnitor := leftUnitor - rightUnitor := rightUnitor + (tensorObj := MonoidalCategory.tensorObj) + (tensorHom := @tensorHom _ _) + (whiskerLeft := @whiskerLeft _ _) + (whiskerRight := @whiskerRight _ _) + (tensorUnit' := ModuleCat.of R R) + (associator := associator) + (leftUnitor := leftUnitor) + (rightUnitor := rightUnitor) -- properties - tensor_id M N := tensor_id M N - tensor_comp f g h := MonoidalCategory.tensor_comp f g h - associator_naturality f g h := MonoidalCategory.associator_naturality f g h - leftUnitor_naturality f := MonoidalCategory.leftUnitor_naturality f - rightUnitor_naturality f := rightUnitor_naturality f - pentagon M N K L := pentagon M N K L - triangle M N := triangle M N + (tensor_id := fun M N ↦ tensor_id M N) + (tensor_comp := fun f g h ↦ MonoidalCategory.tensor_comp f g h) + (associator_naturality := fun f g h ↦ MonoidalCategory.associator_naturality f g h) + (leftUnitor_naturality := fun f ↦ MonoidalCategory.leftUnitor_naturality f) + (rightUnitor_naturality := fun f ↦ rightUnitor_naturality f) + (pentagon := fun M N K L ↦ pentagon M N K L) + (triangle := fun M N ↦ triangle M N) #align Module.monoidal_category ModuleCat.monoidalCategory /-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative ring. -/ diff --git a/Mathlib/CategoryTheory/Bicategory/End.lean b/Mathlib/CategoryTheory/Bicategory/End.lean index a27ab4ccb101a..0797bd0acacba 100644 --- a/Mathlib/CategoryTheory/Bicategory/End.lean +++ b/Mathlib/CategoryTheory/Bicategory/End.lean @@ -39,7 +39,8 @@ open Bicategory attribute [local simp] EndMonoidal in instance (X : C) : MonoidalCategory (EndMonoidal X) where tensorObj f g := f ≫ g - tensorHom {f g} h i η θ := η ▷ h ≫ g ◁ θ + whiskerLeft {f g h} η := f ◁ η + whiskerRight {f g} η h := η ▷ h tensorUnit' := 𝟙 _ associator f g h := α_ f g h leftUnitor f := λ_ f diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean index b0f37f1b380d9..5176d59083667 100644 --- a/Mathlib/CategoryTheory/Monoidal/Category.lean +++ b/Mathlib/CategoryTheory/Monoidal/Category.lean @@ -21,25 +21,25 @@ The tensor product can be expressed as a functor via `tensor : C × C ⥤ C`. The unitors and associator are gathered together as natural isomorphisms in `leftUnitor_nat_iso`, `rightUnitor_nat_iso` and `associator_nat_iso`. -Some consequences of the definition are proved in other files, -e.g. `(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom` in `CategoryTheory.Monoidal.UnitorsEqual`. +Some consequences of the definition are proved in other files after proving the coherence theorem, +e.g. `(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom` in `CategoryTheory.Monoidal.CoherenceLemmas`. -## Implementation -Dealing with unitors and associators is painful, and at this stage we do not have a useful -implementation of coherence for monoidal categories. +## Implementation notes -In an effort to lessen the pain, we put some effort into choosing the right `simp` lemmas. -Generally, the rule is that the component index of a natural transformation "weighs more" -in considering the complexity of an expression than does a structural isomorphism (associator, etc). +In the definition of monoidal categories, we also provide the whiskering operators: +* `whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : X ⊗ Y₁ ⟶ X ⊗ Y₂`, denoted by `X ◁ f`, +* `whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : X₁ ⊗ Y ⟶ X₂ ⊗ Y`, denoted by `f ▷ Y`. +These are products of an object and a morphism (the terminology "whiskering" +is borrowed from 2-category theory). The tensor product of morphisms `tensorHom` can be defined +in terms of the whiskerings. There are two possible such definitions, which are related by +the exchange property of the whiskerings. These two definitions are accessed by `tensorHom_def` +and `tensorHom_def'`. By default, `tensorHom` is defined so that `tensorHom_def` holds +definitionally. -As an example when we prove Proposition 2.2.4 of - -we state it as a `@[simp]` lemma as -``` -(λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ⊗ (𝟙 Y) -``` +If you want to provide `tensorHom` and define `whiskerLeft` and `whiskerRight` in terms of it, +you can use the alternative constructor `CategoryTheory.MonoidalCategory.ofTensorHom`. -This is far from completely effective, but seems to prove a useful principle. +The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories. ## References * Tensor categories, Etingof, Gelaki, Nikshych, Ostrik, @@ -73,8 +73,17 @@ See . class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where /-- curried tensor product of objects -/ tensorObj : C → C → C - /-- curried tensor product of morphisms -/ - tensorHom : ∀ {X₁ Y₁ X₂ Y₂ : C}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂) + /-- left whiskering for morphisms -/ + whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂ + /-- right whiskering for morphisms -/ + whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y + /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/ + -- By default, it is defined in terms of whiskerings. + tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂) := + whiskerRight f X₂ ≫ whiskerLeft Y₁ g + tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : + tensorHom f g = whiskerRight f X₂ ≫ whiskerLeft Y₁ g := by + aesop_cat /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/ tensor_id : ∀ X₁ X₂ : C, tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂) := by aesop_cat /-- @@ -87,29 +96,33 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where aesop_cat -- Porting note: Adding a prime here, so I can later define `tensorUnit` unprimed with explicit -- argument `C` - /-- The tensor unity in the monoidal structure `𝟙_C` -/ + /-- The tensor unity in the monoidal structure `𝟙_ C` -/ tensorUnit' : C /-- The associator isomorphism `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)` -/ associator : ∀ X Y Z : C, tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) + whiskerLeft_id : ∀ (X Y : C), whiskerLeft X (𝟙 Y) = 𝟙 (tensorObj X Y) := by + aesop_cat + id_whiskerRight : ∀ (X Y : C), whiskerRight (𝟙 X) Y = 𝟙 (tensorObj X Y) := by + aesop_cat /-- Naturality of the associator isomorphism: `(f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)` -/ associator_naturality : ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by aesop_cat - /-- The left unitor: `𝟙_C ⊗ X ≃ X` -/ + /-- The left unitor: `𝟙_ C ⊗ X ≃ X` -/ leftUnitor : ∀ X : C, tensorObj tensorUnit' X ≅ X /-- - Naturality of the left unitor, commutativity of `𝟙_C ⊗ X ⟶ 𝟙_C ⊗ Y ⟶ Y` and `𝟙_C ⊗ X ⟶ X ⟶ Y` + Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y` -/ leftUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f := by aesop_cat - /-- The right unitor: `X ⊗ 𝟙_C ≃ X` -/ + /-- The right unitor: `X ⊗ 𝟙_ C ≃ X` -/ rightUnitor : ∀ X : C, tensorObj X tensorUnit' ≅ X /-- - Naturality of the right unitor: commutativity of `X ⊗ 𝟙_C ⟶ Y ⊗ 𝟙_C ⟶ Y` and `X ⊗ 𝟙_C ⟶ X ⟶ Y` + Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y` -/ rightUnitor_naturality : ∀ {X Y : C} (f : X ⟶ Y), @@ -134,6 +147,9 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where aesop_cat #align category_theory.monoidal_category CategoryTheory.MonoidalCategory +attribute [reassoc] MonoidalCategory.tensorHom_def +attribute [reassoc, simp] MonoidalCategory.whiskerLeft_id +attribute [reassoc, simp] MonoidalCategory.id_whiskerRight attribute [simp] MonoidalCategory.tensor_id attribute [reassoc] MonoidalCategory.tensor_comp attribute [simp] MonoidalCategory.tensor_comp @@ -146,7 +162,7 @@ attribute [reassoc (attr := simp)] MonoidalCategory.triangle -- Porting Note: This is here to make `tensorUnit` explicitly depend on `C`, which was done in -- Lean 3 using the `[]` notation in the `tensorUnit'` field. open CategoryTheory.MonoidalCategory in -/-- The tensor unity in the monoidal structure `𝟙_C` -/ +/-- The tensor unity in the monoidal structure `𝟙_ C` -/ abbrev MonoidalCategory.tensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] : C := tensorUnit' (C := C) @@ -155,6 +171,12 @@ namespace MonoidalCategory /-- Notation for `tensorObj`, the tensor product of objects in a monoidal category -/ scoped infixr:70 " ⊗ " => tensorObj +/-- Notation for the `whiskerLeft` operator of monoidal categories -/ +scoped infixr:81 " ◁ " => whiskerLeft + +/-- Notation for the `whiskerRight` operator of monoidal categories -/ +scoped infixl:81 " ▷ " => whiskerRight + /-- Notation for `tensorHom`, the tensor product of morphisms in a monoidal category -/ scoped infixr:70 " ⊗ " => tensorHom @@ -170,6 +192,25 @@ scoped notation "λ_" => leftUnitor /-- Notation for the `rightUnitor`: `X ⊗ 𝟙_C ≃ X` -/ scoped notation "ρ_" => rightUnitor +variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C] + +theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : + (𝟙 X) ⊗ f = X ◁ f := by + simp [tensorHom_def] + +theorem tensorHom_id {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : + f ⊗ (𝟙 Y) = f ▷ Y := by + simp [tensorHom_def] + +theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : + W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g := by + simp [← id_tensorHom, ← tensorHom_id, ← tensor_comp] + +@[reassoc] +theorem tensorHom_def' {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : + f ⊗ g = X₁ ◁ g ≫ f ▷ Y₂ := + whisker_exchange f g ▸ tensorHom_def f g + end MonoidalCategory open scoped MonoidalCategory @@ -395,6 +436,70 @@ theorem tensor_inv_hom_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) rw [← tensor_comp, IsIso.inv_hom_id, comp_tensor_id] #align category_theory.monoidal_category.tensor_inv_hom_id' CategoryTheory.MonoidalCategory.tensor_inv_hom_id' +/-- +A constructor for monoidal categories that requires `tensorHom` instead of `whiskerLeft` and +`whiskerRight`. +-/ +def ofTensorHom + (tensorObj : C → C → C) + (tensorHom : ∀ {X₁ Y₁ X₂ Y₂ : C}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)) + (whiskerLeft : ∀ (X : C) {Y₁ Y₂ : C} (_f : Y₁ ⟶ Y₂), tensorObj X Y₁ ⟶ tensorObj X Y₂ := + fun X _ _ f ↦ tensorHom (𝟙 X) f) + (whiskerRight : ∀ {X₁ X₂ : C} (_f : X₁ ⟶ X₂) (Y : C), tensorObj X₁ Y ⟶ tensorObj X₂ Y := + fun f Y ↦ tensorHom f (𝟙 Y)) + (tensor_id : ∀ X₁ X₂ : C, tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂) := by + aesop_cat) + (id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f := by + aesop_cat) + (tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y := by + aesop_cat) + (tensor_comp : + ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂), + tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ := by + aesop_cat) + (tensorUnit' : C) + (associator : ∀ X Y Z : C, tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)) + (associator_naturality : + ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃), + tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = + (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by + aesop_cat) + (leftUnitor : ∀ X : C, tensorObj tensorUnit' X ≅ X) + (leftUnitor_naturality : + ∀ {X Y : C} (f : X ⟶ Y), + tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f := by + aesop_cat) + (rightUnitor : ∀ X : C, tensorObj X tensorUnit' ≅ X) + (rightUnitor_naturality : + ∀ {X Y : C} (f : X ⟶ Y), + tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f := by + aesop_cat) + (pentagon : + ∀ W X Y Z : C, + tensorHom (associator W X Y).hom (𝟙 Z) ≫ + (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom = + (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom := by + aesop_cat) + (triangle : + ∀ X Y : C, + (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom = + tensorHom (rightUnitor X).hom (𝟙 Y) := by + aesop_cat) : + MonoidalCategory C where + tensorObj := tensorObj + tensorHom := tensorHom + whiskerLeft X _ _ f := whiskerLeft X f + whiskerRight f X := whiskerRight f X + tensorHom_def := by intros; simp [← id_tensorHom, ←tensorHom_id, ← tensor_comp] + tensorUnit' := tensorUnit' + leftUnitor := leftUnitor + rightUnitor := rightUnitor + associator := associator + whiskerLeft_id := by intros; simp [← id_tensorHom, ← tensor_id] + id_whiskerRight := by intros; simp [← tensorHom_id, tensor_id] + pentagon := by intros; simp [← id_tensorHom, ← tensorHom_id, pentagon] + triangle := by intros; simp [← id_tensorHom, ← tensorHom_id, triangle] + end section @@ -612,6 +717,9 @@ attribute [local simp] associator_naturality leftUnitor_naturality rightUnitor_n instance prodMonoidal : MonoidalCategory (C₁ × C₂) where tensorObj X Y := (X.1 ⊗ Y.1, X.2 ⊗ Y.2) tensorHom f g := (f.1 ⊗ g.1, f.2 ⊗ g.2) + whiskerLeft X _ _ f := (whiskerLeft X.1 f.1, whiskerLeft X.2 f.2) + whiskerRight f X := (whiskerRight f.1 X.1, whiskerRight f.2 X.2) + tensorHom_def := by simp [tensorHom_def] tensorUnit' := (𝟙_ C₁, 𝟙_ C₂) associator X Y Z := (α_ X.1 Y.1 Z.1).prod (α_ X.2 Y.2 Z.2) leftUnitor := fun ⟨X₁, X₂⟩ => (λ_ X₁).prod (λ_ X₂) diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean index cf98e943b68a9..c4fde65113ca1 100644 --- a/Mathlib/CategoryTheory/Monoidal/Center.lean +++ b/Mathlib/CategoryTheory/Monoidal/Center.lean @@ -226,6 +226,10 @@ attribute [local simp] Center.associator Center.leftUnitor Center.rightUnitor instance : MonoidalCategory (Center C) where tensorObj X Y := tensorObj X Y tensorHom f g := tensorHom f g + -- Todo: replace it by `X.1 ◁ f.f` + whiskerLeft X _ _ f := tensorHom (𝟙 X) f + -- Todo: replace it by `f.f ▷ Y.1` + whiskerRight f Y := tensorHom f (𝟙 Y) tensorUnit' := tensorUnit associator := associator leftUnitor := leftUnitor diff --git a/Mathlib/CategoryTheory/Monoidal/Discrete.lean b/Mathlib/CategoryTheory/Monoidal/Discrete.lean index 6f7c69ce4bdf3..b69000f60d044 100644 --- a/Mathlib/CategoryTheory/Monoidal/Discrete.lean +++ b/Mathlib/CategoryTheory/Monoidal/Discrete.lean @@ -30,6 +30,8 @@ instance Discrete.monoidal : MonoidalCategory (Discrete M) where tensorUnit' := Discrete.mk 1 tensorObj X Y := Discrete.mk (X.as * Y.as) + whiskerLeft X _ _ f := eqToHom (by dsimp; rw [eq_of_hom f]) + whiskerRight f X := eqToHom (by dsimp; rw [eq_of_hom f]) tensorHom f g := eqToHom (by dsimp; rw [eq_of_hom f, eq_of_hom g]) leftUnitor X := Discrete.eqToIso (one_mul X.as) rightUnitor X := Discrete.eqToIso (mul_one X.as) diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean index c4d28e456bb3d..65aaf70882a47 100644 --- a/Mathlib/CategoryTheory/Monoidal/End.lean +++ b/Mathlib/CategoryTheory/Monoidal/End.lean @@ -32,6 +32,8 @@ with tensor product given by composition of functors -/ def endofunctorMonoidalCategory : MonoidalCategory (C ⥤ C) where tensorObj F G := F ⋙ G + whiskerLeft X _ _ F := whiskerLeft X F + whiskerRight F X := whiskerRight F X tensorHom α β := α ◫ β tensorUnit' := 𝟭 C associator F G H := Functor.associator F G H diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean index 2083f7832bfe5..a5cf2907343ea 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean @@ -159,6 +159,28 @@ instance : MonoidalCategory (F C) where Quotient.map₂ Hom.tensor <| by intro _ _ h _ _ h' exact HomEquiv.tensor h h' + whiskerLeft := fun X _ _ f => + Quotient.map (fun f' => Hom.tensor (Hom.id X) f') + (fun _ _ h => HomEquiv.tensor (HomEquiv.refl (Hom.id X)) h) f + whiskerRight := fun f Y => + Quotient.map (fun f' => Hom.tensor f' (Hom.id Y)) + (fun _ _ h => HomEquiv.tensor h (HomEquiv.refl (Hom.id Y))) f + tensorHom_def := by + rintro W X Y Z ⟨f⟩ ⟨g⟩ + apply Quotient.sound + calc Hom.tensor f g + _ ≈ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g) := by + apply HomEquiv.tensor (HomEquiv.comp_id f).symm (HomEquiv.id_comp g).symm + _ ≈ Hom.comp (Hom.tensor f (Hom.id Y)) (Hom.tensor (Hom.id X) g) := by + apply HomEquiv.tensor_comp + whiskerLeft_id := by + rintro X Y + apply Quotient.sound + apply HomEquiv.tensor_id + id_whiskerRight := by + intro X Y + apply Quotient.sound + apply HomEquiv.tensor_id tensor_id X Y := Quotient.sound tensor_id tensor_comp := @fun X₁ Y₁ Z₁ X₂ Y₂ Z₂ => by rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩ diff --git a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean index dfbe63d4ad3e6..03a4e27d040a4 100644 --- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean @@ -57,6 +57,22 @@ def tensorHom : tensorObj F F' ⟶ tensorObj G G' where naturality X Y f := by dsimp; rw [← tensor_comp, α.naturality, β.naturality, tensor_comp] #align category_theory.monoidal.functor_category.tensor_hom CategoryTheory.Monoidal.FunctorCategory.tensorHom +/-- (An auxiliary definition for `functorCategoryMonoidal`.) -/ +@[simps] +def whiskerLeft (F) (β : F' ⟶ G') : tensorObj F F' ⟶ tensorObj F G' where + app X := F.obj X ◁ β.app X + naturality X Y f := by + simp only [← id_tensorHom] + apply (tensorHom (𝟙 F) β).naturality + +/-- (An auxiliary definition for `functorCategoryMonoidal`.) -/ +@[simps] +def whiskerRight (F') : tensorObj F F' ⟶ tensorObj G F' where + app X := α.app X ▷ F'.obj X + naturality X Y f := by + simp only [← tensorHom_id] + apply (tensorHom α (𝟙 F')).naturality + end FunctorCategory open CategoryTheory.Monoidal.FunctorCategory @@ -68,6 +84,9 @@ where `(F ⊗ G).obj X = F.obj X ⊗ G.obj X`. instance functorCategoryMonoidal : MonoidalCategory (C ⥤ D) where tensorObj F G := tensorObj F G tensorHom α β := tensorHom α β + whiskerLeft F _ _ α := FunctorCategory.whiskerLeft F α + whiskerRight α F := FunctorCategory.whiskerRight α F + tensorHom_def := by intros; ext; simp [tensorHom_def] tensorUnit' := (CategoryTheory.Functor.const C).obj (𝟙_ D) leftUnitor F := NatIso.ofComponents fun X => λ_ (F.obj X) rightUnitor F := NatIso.ofComponents fun X => ρ_ (F.obj X) diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean index f5263d9c40d90..b1e1e697de66b 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean @@ -475,15 +475,15 @@ theorem mul_rightUnitor {M : Mon_ C} : simp only [Category.assoc, Category.id_comp] #align Mon_.mul_right_unitor Mon_.mul_rightUnitor -instance monMonoidal : MonoidalCategory (Mon_ C) where - tensorObj M N := +instance monMonoidal : MonoidalCategory (Mon_ C) := .ofTensorHom + (tensorObj := fun M N ↦ { X := M.X ⊗ N.X one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) one_mul := Mon_tensor_one_mul M N mul_one := Mon_tensor_mul_one M N - mul_assoc := Mon_tensor_mul_assoc M N } - tensorHom f g := + mul_assoc := Mon_tensor_mul_assoc M N }) + (tensorHom := fun f g ↦ { hom := f.hom ⊗ g.hom one_hom := by dsimp @@ -492,18 +492,18 @@ instance monMonoidal : MonoidalCategory (Mon_ C) where dsimp slice_rhs 1 2 => rw [tensor_μ_natural] slice_lhs 2 3 => rw [← tensor_comp, Hom.mul_hom f, Hom.mul_hom g, tensor_comp] - simp only [Category.assoc] } - tensor_id := by intros; ext; apply tensor_id - tensor_comp := by intros; ext; apply tensor_comp - tensorUnit' := trivial C - associator M N P := isoOfIso (α_ M.X N.X P.X) one_associator mul_associator - associator_naturality := by intros; ext; dsimp; apply associator_naturality - leftUnitor M := isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor - leftUnitor_naturality := by intros; ext; dsimp; apply leftUnitor_naturality - rightUnitor M := isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor - rightUnitor_naturality := by intros; ext; dsimp; apply rightUnitor_naturality - pentagon := by intros; ext; dsimp; apply pentagon - triangle := by intros; ext; dsimp; apply triangle + simp only [Category.assoc] }) + (tensor_id := by intros; ext; apply tensor_id) + (tensor_comp := by intros; ext; apply tensor_comp) + (tensorUnit' := trivial C) + (associator := fun M N P ↦ isoOfIso (α_ M.X N.X P.X) one_associator mul_associator) + (associator_naturality := by intros; ext; dsimp; apply associator_naturality) + (leftUnitor := fun M ↦ isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor) + (leftUnitor_naturality := by intros; ext; dsimp; apply leftUnitor_naturality) + (rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor) + (rightUnitor_naturality := by intros; ext; dsimp; apply rightUnitor_naturality) + (pentagon := by intros; ext; dsimp; apply pentagon) + (triangle := by intros; ext; dsimp; apply triangle) #align Mon_.Mon_monoidal Mon_.monMonoidal end Mon_ diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean index 9e64c577827c1..44e1b1f1c70c3 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean @@ -331,20 +331,20 @@ end MonoidalOfChosenFiniteProducts open MonoidalOfChosenFiniteProducts /-- A category with a terminal object and binary products has a natural monoidal structure. -/ -def monoidalOfChosenFiniteProducts : MonoidalCategory C where - tensorUnit' := 𝒯.cone.pt - tensorObj X Y := tensorObj ℬ X Y - tensorHom f g := tensorHom ℬ f g - tensor_id := tensor_id ℬ - tensor_comp f₁ f₂ g₁ g₂ := tensor_comp ℬ f₁ f₂ g₁ g₂ - associator X Y Z := BinaryFan.associatorOfLimitCone ℬ X Y Z - leftUnitor X := BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit - rightUnitor X := BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit - pentagon := pentagon ℬ - triangle := triangle 𝒯 ℬ - leftUnitor_naturality f := leftUnitor_naturality 𝒯 ℬ f - rightUnitor_naturality f := rightUnitor_naturality 𝒯 ℬ f - associator_naturality f₁ f₂ f₃ := associator_naturality ℬ f₁ f₂ f₃ +def monoidalOfChosenFiniteProducts : MonoidalCategory C := .ofTensorHom + (tensorUnit' := 𝒯.cone.pt) + (tensorObj := tensorObj ℬ) + (tensorHom := tensorHom ℬ) + (tensor_id := tensor_id ℬ) + (tensor_comp := tensor_comp ℬ) + (associator := BinaryFan.associatorOfLimitCone ℬ) + (leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit) + (rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit) + (pentagon := pentagon ℬ) + (triangle := triangle 𝒯 ℬ) + (leftUnitor_naturality := leftUnitor_naturality 𝒯 ℬ) + (rightUnitor_naturality := rightUnitor_naturality 𝒯 ℬ) + (associator_naturality := associator_naturality ℬ) #align category_theory.monoidal_of_chosen_finite_products CategoryTheory.monoidalOfChosenFiniteProducts namespace MonoidalOfChosenFiniteProducts diff --git a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean index ba99a75e5ebfd..0290e568dc308 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean +++ b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean @@ -45,39 +45,21 @@ open CategoryTheory.Limits section /-- A category with a terminal object and binary products has a natural monoidal structure. -/ -def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C where - tensorUnit' := ⊤_ C - tensorObj X Y := X ⨯ Y - tensorHom f g := Limits.prod.map f g - associator := prod.associator - leftUnitor P := prod.leftUnitor P - rightUnitor P := prod.rightUnitor P - pentagon := prod.pentagon - triangle := prod.triangle - associator_naturality := @prod.associator_naturality _ _ _ +def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C := + .ofTensorHom + (tensorUnit' := ⊤_ C) + (tensorObj := fun X Y ↦ X ⨯ Y) + (tensorHom := fun f g ↦ Limits.prod.map f g) + (associator := prod.associator) + (leftUnitor := fun P ↦ prod.leftUnitor P) + (rightUnitor := fun P ↦ prod.rightUnitor P) + (pentagon := prod.pentagon) + (triangle := prod.triangle) + (associator_naturality := @prod.associator_naturality _ _ _) #align category_theory.monoidal_of_has_finite_products CategoryTheory.monoidalOfHasFiniteProducts end -section - -attribute [local instance] monoidalOfHasFiniteProducts - -open MonoidalCategory - -/-- The monoidal structure coming from finite products is symmetric. --/ -@[simps] -def symmetricOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : SymmetricCategory C where - braiding X Y := Limits.prod.braiding X Y - braiding_naturality f g := by dsimp [tensorHom]; simp - hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteProducts]; simp - hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteProducts]; simp - symmetry X Y := by dsimp; simp; rfl -#align category_theory.symmetric_of_has_finite_products CategoryTheory.symmetricOfHasFiniteProducts - -end - namespace monoidalOfHasFiniteProducts variable [HasTerminal C] [HasBinaryProducts C] @@ -126,42 +108,47 @@ theorem associator_hom (X Y Z : C) : rfl #align category_theory.monoidal_of_has_finite_products.associator_hom CategoryTheory.monoidalOfHasFiniteProducts.associator_hom -end monoidalOfHasFiniteProducts - -section - -/-- A category with an initial object and binary coproducts has a natural monoidal structure. -/ -def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C where - tensorUnit' := ⊥_ C - tensorObj X Y := X ⨿ Y - tensorHom f g := Limits.coprod.map f g - associator := coprod.associator - leftUnitor := coprod.leftUnitor - rightUnitor := coprod.rightUnitor - pentagon := coprod.pentagon - triangle := coprod.triangle - associator_naturality := @coprod.associator_naturality _ _ _ -#align category_theory.monoidal_of_has_finite_coproducts CategoryTheory.monoidalOfHasFiniteCoproducts +theorem associator_inv (X Y Z : C) : + (α_ X Y Z).inv = + prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd) := + rfl -end +end monoidalOfHasFiniteProducts section -attribute [local instance] monoidalOfHasFiniteCoproducts +attribute [local instance] monoidalOfHasFiniteProducts open MonoidalCategory -/-- The monoidal structure coming from finite coproducts is symmetric. +/-- The monoidal structure coming from finite products is symmetric. -/ @[simps] -def symmetricOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : - SymmetricCategory C where - braiding := Limits.coprod.braiding +def symmetricOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : SymmetricCategory C where + braiding X Y := Limits.prod.braiding X Y braiding_naturality f g := by dsimp [tensorHom]; simp - hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteCoproducts]; simp - hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteCoproducts]; simp - symmetry X Y := by dsimp; simp; rfl -#align category_theory.symmetric_of_has_finite_coproducts CategoryTheory.symmetricOfHasFiniteCoproducts + hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_hom]; simp + hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_inv]; simp + symmetry X Y := by dsimp; simp +#align category_theory.symmetric_of_has_finite_products CategoryTheory.symmetricOfHasFiniteProducts + +end + +section + +/-- A category with an initial object and binary coproducts has a natural monoidal structure. -/ +def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C := + .ofTensorHom + (tensorUnit' := ⊥_ C) + (tensorObj := fun X Y ↦ X ⨿ Y) + (tensorHom := fun f g ↦ Limits.coprod.map f g) + (associator := coprod.associator) + (leftUnitor := coprod.leftUnitor) + (rightUnitor := coprod.rightUnitor) + (pentagon := coprod.pentagon) + (triangle := coprod.triangle) + (associator_naturality := @coprod.associator_naturality _ _ _) +#align category_theory.monoidal_of_has_finite_coproducts CategoryTheory.monoidalOfHasFiniteCoproducts end @@ -212,6 +199,31 @@ theorem associator_hom (X Y Z : C) : rfl #align category_theory.monoidal_of_has_finite_coproducts.associator_hom CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom +theorem associator_inv (X Y Z : C) : + (α_ X Y Z).inv = + coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) := + rfl + end monoidalOfHasFiniteCoproducts +section + +attribute [local instance] monoidalOfHasFiniteCoproducts + +open MonoidalCategory + +/-- The monoidal structure coming from finite coproducts is symmetric. +-/ +@[simps] +def symmetricOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : + SymmetricCategory C where + braiding := Limits.coprod.braiding + braiding_naturality f g := by dsimp [tensorHom]; simp + hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteCoproducts.associator_hom]; simp + hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteCoproducts.associator_inv]; simp + symmetry X Y := by dsimp; simp +#align category_theory.symmetric_of_has_finite_coproducts CategoryTheory.symmetricOfHasFiniteCoproducts + +end + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Monoidal/Opposite.lean b/Mathlib/CategoryTheory/Monoidal/Opposite.lean index e6ddb78353085..6d7823eb1c6c4 100644 --- a/Mathlib/CategoryTheory/Monoidal/Opposite.lean +++ b/Mathlib/CategoryTheory/Monoidal/Opposite.lean @@ -170,7 +170,10 @@ open Opposite MonoidalCategory instance monoidalCategoryOp : MonoidalCategory Cᵒᵖ where tensorObj X Y := op (unop X ⊗ unop Y) + whiskerLeft X _ _ f := (X.unop ◁ f.unop).op + whiskerRight f X := (f.unop ▷ X.unop).op tensorHom f g := (f.unop ⊗ g.unop).op + tensorHom_def f g := Quiver.Hom.unop_inj (tensorHom_def' _ _) tensorUnit' := op (𝟙_ C) associator X Y Z := (α_ (unop X) (unop Y) (unop Z)).symm.op leftUnitor X := (λ_ (unop X)).symm.op @@ -192,7 +195,10 @@ theorem op_tensorUnit : 𝟙_ Cᵒᵖ = op (𝟙_ C) := instance monoidalCategoryMop : MonoidalCategory Cᴹᵒᵖ where tensorObj X Y := mop (unmop Y ⊗ unmop X) + whiskerLeft X _ _ f := (f.unmop ▷ X.unmop).mop + whiskerRight f X := (X.unmop ◁ f.unmop).mop tensorHom f g := (g.unmop ⊗ f.unmop).mop + tensorHom_def f g := unmop_inj (tensorHom_def' _ _) tensorUnit' := mop (𝟙_ C) associator X Y Z := (α_ (unmop Z) (unmop Y) (unmop X)).symm.mop leftUnitor X := (ρ_ (unmop X)).mop diff --git a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean index 9b30b98669b33..26d93468261c0 100644 --- a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean +++ b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean @@ -53,13 +53,16 @@ When `P` is a monoidal predicate, the full subcategory for `P` inherits the mono -/ instance fullMonoidalSubcategory : MonoidalCategory (FullSubcategory P) where tensorObj X Y := ⟨X.1 ⊗ Y.1, prop_tensor X.2 Y.2⟩ - tensorHom := @fun X₁ Y₁ X₂ Y₂ f g => by - change X₁.1 ⊗ X₂.1 ⟶ Y₁.1 ⊗ Y₂.1 - change X₁.1 ⟶ Y₁.1 at f; change X₂.1 ⟶ Y₂.1 at g; exact f ⊗ g + tensorHom f g := f ⊗ g + tensorHom_def f g := tensorHom_def (C := C) f g + whiskerLeft := fun X _ _ f ↦ X.1 ◁ f + whiskerRight := fun f Y ↦ (fun f ↦ f ▷ Y.1) f tensorUnit' := ⟨𝟙_ C, prop_id⟩ associator X Y Z := ⟨(α_ X.1 Y.1 Z.1).hom, (α_ X.1 Y.1 Z.1).inv, hom_inv_id (α_ X.1 Y.1 Z.1), inv_hom_id (α_ X.1 Y.1 Z.1)⟩ + whiskerLeft_id X Y := whiskerLeft_id X.1 Y.1 + id_whiskerRight X Y := id_whiskerRight X.1 Y.1 leftUnitor X := ⟨(λ_ X.1).hom, (λ_ X.1).inv, hom_inv_id (λ_ X.1), inv_hom_id (λ_ X.1)⟩ rightUnitor X := ⟨(ρ_ X.1).hom, (ρ_ X.1).inv, hom_inv_id (ρ_ X.1), inv_hom_id (ρ_ X.1)⟩ tensor_id X Y := tensor_id X.1 Y.1 diff --git a/Mathlib/CategoryTheory/Monoidal/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean index 36c509c98a257..32ec7208db3c3 100644 --- a/Mathlib/CategoryTheory/Monoidal/Transport.lean +++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean @@ -41,6 +41,9 @@ variable {D : Type u₂} [Category.{v₂} D] @[simps] def transport (e : C ≌ D) : MonoidalCategory.{v₂} D where tensorObj X Y := e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y) + whiskerLeft := fun X _ _ f ↦ e.functor.map (e.inverse.obj X ◁ e.inverse.map f) + whiskerRight := fun f X ↦ e.functor.map (e.inverse.map f ▷ e.inverse.obj X) + tensorHom_def := by simp [tensorHom_def] tensorHom f g := e.functor.map (e.inverse.map f ⊗ e.inverse.map g) tensorUnit' := e.functor.obj (𝟙_ C) associator X Y Z :=