From bd2a2c1c3ef01bd2ffc6b7101db12e5ecafd2f5f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 20 Sep 2023 13:30:18 +0000 Subject: [PATCH 1/3] refactor(CategoryTheory/Monoidal): make `ofTensorHom` the default constructor It seems all the users wish they had this constructor anyway, so lets just make it the default. --- .../Category/ModuleCat/Monoidal/Basic.lean | 32 ++--- Mathlib/CategoryTheory/Monoidal/Category.lean | 112 +++++------------- .../CategoryTheory/Monoidal/Free/Basic.lean | 22 ---- .../Monoidal/FunctorCategory.lean | 3 +- Mathlib/CategoryTheory/Monoidal/Mon_.lean | 32 ++--- .../OfChosenFiniteProducts/Basic.lean | 28 ++--- .../Monoidal/OfHasFiniteProducts.lean | 42 ++++--- .../CategoryTheory/Monoidal/Subcategory.lean | 5 +- 8 files changed, 97 insertions(+), 179 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean index f40fcac2a0d35..5ecfa39f0fa10 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean @@ -197,24 +197,24 @@ end MonoidalCategory open MonoidalCategory -instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom +instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) where -- data - (tensorObj := MonoidalCategory.tensorObj) - (tensorHom := @tensorHom _ _) - (whiskerLeft := @whiskerLeft _ _) - (whiskerRight := @whiskerRight _ _) - (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 := 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) + 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/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean index 76f882ac725d2..84bc7aeb37516 100644 --- a/Mathlib/CategoryTheory/Monoidal/Category.lean +++ b/Mathlib/CategoryTheory/Monoidal/Category.lean @@ -33,11 +33,7 @@ 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. - -If you want to provide `tensorHom` and define `whiskerLeft` and `whiskerRight` in terms of it, -you can use the alternative constructor `CategoryTheory.MonoidalCategory.ofTensorHom`. +and `tensorHom_def'`. The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories. @@ -73,16 +69,21 @@ See . class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where /-- curried tensor product of objects -/ tensorObj : C → C → C + /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/ + tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : 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₂ + -- By default, it is defined in terms of tensorHom. + whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂ := + tensorHom (𝟙 X) f + whiskerLeft_def (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : + whiskerLeft X f = tensorHom (𝟙 X) f := by + aesop_cat /-- 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 + -- By default, it is defined in terms of tensorHom. + whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y := + tensorHom f (𝟙 Y) + whiskerRight_def {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : + whiskerRight f Y = tensorHom f (𝟙 Y) := 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 @@ -100,10 +101,6 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where 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₃), @@ -147,9 +144,6 @@ 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 @@ -194,6 +188,17 @@ scoped notation "ρ_" => rightUnitor variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C] +@[reassoc] +theorem tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : + f ⊗ g = (f ▷ X₂) ≫ (Y₁ ◁ g) := by + rw [whiskerRight_def, whiskerLeft_def, ←tensor_comp, comp_id, id_comp] + +@[reassoc, simp] +theorem whiskerLeft_id (X Y : C) : X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by rw [whiskerLeft_def, tensor_id] + +@[reassoc, simp] +theorem id_whiskerRight (X Y : C) : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by rw [whiskerRight_def, tensor_id] + theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : (𝟙 X) ⊗ f = X ◁ f := by simp [tensorHom_def] @@ -437,70 +442,6 @@ 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 @@ -719,8 +660,9 @@ 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) + whiskerLeft_def := by simp [whiskerLeft_def] whiskerRight f X := (whiskerRight f.1 X.1, whiskerRight f.2 X.2) - tensorHom_def := by simp [tensorHom_def] + whiskerRight_def := by simp [whiskerRight_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/Free/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean index a5cf2907343ea..2083f7832bfe5 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean @@ -159,28 +159,6 @@ 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 e09f916db2b91..432836bde2c45 100644 --- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean @@ -85,8 +85,9 @@ instance functorCategoryMonoidal : MonoidalCategory (C ⥤ D) where tensorObj F G := tensorObj F G tensorHom α β := tensorHom α β whiskerLeft F _ _ α := FunctorCategory.whiskerLeft F α + whiskerLeft_def F _ _ α := by ext; simp [whiskerLeft_def] whiskerRight α F := FunctorCategory.whiskerRight α F - tensorHom_def := by intros; ext; simp [tensorHom_def] + whiskerRight_def α F := by ext; simp [whiskerRight_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 b1e1e697de66b..703614d23886a 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) := .ofTensorHom - (tensorObj := fun M N ↦ +instance monMonoidal : MonoidalCategory (Mon_ C) where + 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 := fun 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) := .ofTensorHom 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 := 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) + 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 44e1b1f1c70c3..affae78fbb2ee 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 := .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 ℬ) +def monoidalOfChosenFiniteProducts : MonoidalCategory C where + 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 0290e568dc308..31a2dd2f5a170 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean +++ b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean @@ -45,17 +45,16 @@ 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 := - .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 _ _ _) +def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C where + 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 @@ -137,17 +136,16 @@ 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 _ _ _) +def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C where + 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 diff --git a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean index afd44e24ee1b6..03527aa5af629 100644 --- a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean +++ b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean @@ -54,15 +54,14 @@ 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 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 + whiskerRight_def {_ _} _f Y := whiskerRight_def _ Y.1 + whiskerLeft_def X {_ _} _g := whiskerLeft_def X.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 From e8c5e202e134456356a642baa0c2b10e51b072ca Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 20 Sep 2023 13:48:48 +0000 Subject: [PATCH 2/3] fix --- Mathlib/CategoryTheory/Bicategory/End.lean | 1 + Mathlib/CategoryTheory/Monoidal/Opposite.lean | 6 ++++-- Mathlib/CategoryTheory/Monoidal/Transport.lean | 3 ++- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Bicategory/End.lean b/Mathlib/CategoryTheory/Bicategory/End.lean index 3875bd2817165..8eb3bf1f76f47 100644 --- a/Mathlib/CategoryTheory/Bicategory/End.lean +++ b/Mathlib/CategoryTheory/Bicategory/End.lean @@ -41,6 +41,7 @@ instance (X : C) : MonoidalCategory (EndMonoidal X) where tensorObj f g := f ≫ g whiskerLeft {f g h} η := f ◁ η whiskerRight {f g} η h := η ▷ h + tensorHom {X₁ Y₁ X₂ Y₂} f g := (f ▷ X₂) ≫ (Y₁ ◁ g) tensorUnit' := 𝟙 _ associator f g h := α_ f g h leftUnitor f := λ_ f diff --git a/Mathlib/CategoryTheory/Monoidal/Opposite.lean b/Mathlib/CategoryTheory/Monoidal/Opposite.lean index 6d7823eb1c6c4..b223cbe651713 100644 --- a/Mathlib/CategoryTheory/Monoidal/Opposite.lean +++ b/Mathlib/CategoryTheory/Monoidal/Opposite.lean @@ -171,9 +171,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 + whiskerLeft_def X _ _ f := Quiver.Hom.unop_inj <| whiskerLeft_def _ _ whiskerRight f X := (f.unop ▷ X.unop).op + whiskerRight_def f X := Quiver.Hom.unop_inj <| whiskerRight_def _ _ 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 @@ -196,9 +197,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 + whiskerLeft_def X _ _ f := unmop_inj <| whiskerRight_def _ _ whiskerRight f X := (X.unmop ◁ f.unmop).mop + whiskerRight_def f X := unmop_inj <| whiskerLeft_def _ _ 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/Transport.lean b/Mathlib/CategoryTheory/Monoidal/Transport.lean index 319b431464a36..d4ab96882b518 100644 --- a/Mathlib/CategoryTheory/Monoidal/Transport.lean +++ b/Mathlib/CategoryTheory/Monoidal/Transport.lean @@ -42,8 +42,9 @@ variable {D : Type u₂} [Category.{v₂} D] 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) + whiskerLeft_def := by simp [whiskerLeft_def] whiskerRight := fun f X ↦ e.functor.map (e.inverse.map f ▷ e.inverse.obj X) - tensorHom_def := by simp [tensorHom_def] + whiskerRight_def := by simp [whiskerRight_def] tensorHom f g := e.functor.map (e.inverse.map f ⊗ e.inverse.map g) tensorUnit' := e.functor.obj (𝟙_ C) associator X Y Z := From e46eac1b051641de9e7a83445a20dd180755f8f5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 20 Sep 2023 16:57:06 +0100 Subject: [PATCH 3/3] lintfix --- Mathlib/CategoryTheory/Monoidal/Category.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean index 84bc7aeb37516..066460b38acf4 100644 --- a/Mathlib/CategoryTheory/Monoidal/Category.lean +++ b/Mathlib/CategoryTheory/Monoidal/Category.lean @@ -144,6 +144,9 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where aesop_cat #align category_theory.monoidal_category CategoryTheory.MonoidalCategory +-- these are `def`s but should be lemmas, which would be ignored by the linter. +attribute [nolint docBlame] MonoidalCategory.whiskerRight_def MonoidalCategory.whiskerLeft_def + attribute [simp] MonoidalCategory.tensor_id attribute [reassoc] MonoidalCategory.tensor_comp attribute [simp] MonoidalCategory.tensor_comp