(Lax) monoidal functors #
A lax monoidal functor F between monoidal categories C and D
is a functor between the underlying categories equipped with morphisms
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)(called the unit morphism)μ X Y : (F.obj X) ⊗ (F.obj Y) ⟶ F.obj (X ⊗ Y)(called the tensorator, or strength). satisfying various axioms. This is implemented as a typeclassF.LaxMonoidal.
Similarly, we define the typeclass F.OplaxMonoidal. For these oplax monoidal functors,
we have similar data η and δ, but with morphisms in the opposite direction.
A monoidal functor (F.Monoidal) is defined here as the combination of F.LaxMonoidal
and F.OplaxMonoidal, with the additional conditions that ε/η and μ/δ are
inverse isomorphisms.
We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.
See Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean for monoidal natural
transformations.
We show in Mathlib.CategoryTheory.Monoidal.Mon_ that lax monoidal functors take monoid objects
to monoid objects.
References #
class
CategoryTheory.Functor.LaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
:
Type (max u₁ v₂)
A functor F : C ⥤ D between monoidal categories is lax monoidal if it is
equipped with morphisms ε : 𝟙_ D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y),
satisfying the appropriate coherences.
the unit morphism of a lax monoidal functor
- μ (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)
the tensorator of a lax monoidal functor
- μ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ F Y X') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.whiskerRight f X'))
- μ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ F X' Y) = CategoryStruct.comp (μ F X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
- associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z)))
associativity of the tensorator
- left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
- right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))
Instances
theorem
CategoryTheory.Functor.LaxMonoidal.ext_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.LaxMonoidal}
:
theorem
CategoryTheory.Functor.LaxMonoidal.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.LaxMonoidal}
(ε : ε F = ε F)
(μ : μ F = μ F)
:
x = y
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
{X Y : C}
(X' : C)
(f : X ⟶ Y)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryStruct.comp (μ F X' Y) h) = CategoryStruct.comp (μ F X' X) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h)
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
{X Y : C}
(f : X ⟶ Y)
(X' : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (μ F Y X') h) = CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.associativity_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h))
associativity of the tensorator
theorem
CategoryTheory.Functor.LaxMonoidal.right_unitality_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))
theorem
CategoryTheory.Functor.LaxMonoidal.left_unitality_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.μ_natural
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ F Y Y') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.tensorHom f g))
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (μ F Y Y') h) = CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h)
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.left_unitality_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X : C)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X))
(μ F (MonoidalCategoryStruct.tensorUnit C) X)) = F.map (MonoidalCategoryStruct.leftUnitor X).inv
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.left_unitality_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.right_unitality_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X : C)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F))
(μ F X (MonoidalCategoryStruct.tensorUnit C))) = F.map (MonoidalCategoryStruct.rightUnitor X).inv
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.associativity_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(F.map (MonoidalCategoryStruct.associator X Y Z).inv)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(μ F (MonoidalCategoryStruct.tensorObj X Y) Z))
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h))
theorem
CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f) (μ F (MonoidalCategoryStruct.tensorUnit C) X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f)
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
(F.map (MonoidalCategoryStruct.leftUnitor X).inv))
theorem
CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f)
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f)
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h))
theorem
CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F)) (μ F X (MonoidalCategoryStruct.tensorUnit C)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D))
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
(F.map (MonoidalCategoryStruct.rightUnitor X).inv))
theorem
CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D))
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h))
theorem
CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f)
(MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f)
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X)
(F.map (MonoidalCategoryStruct.leftUnitor X).hom))
theorem
CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f)
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (ε F) f)
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))
theorem
CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D))
(MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C))
(F.map (MonoidalCategoryStruct.rightUnitor X).hom))
theorem
CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
{X : C}
{Y : D}
(f : Y ⟶ F.obj X)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D))
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (ε F))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))
theorem
CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(μ F (MonoidalCategoryStruct.tensorObj X Y) Z) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(F.map (MonoidalCategoryStruct.associator X Y Z).inv)))
theorem
CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h)))
theorem
CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(μ F X (MonoidalCategoryStruct.tensorObj Y Z)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(F.map (MonoidalCategoryStruct.associator X Y Z).hom)))
theorem
CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)))
@[implicit_reducible]
def
CategoryTheory.Functor.LaxMonoidal.ofTensorHom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(ε : MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μ : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μ_natural :
∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ Y Y') = CategoryStruct.comp (μ X X') (F.map (MonoidalCategoryStruct.tensorHom f g)) := by
cat_disch)
(associativity :
∀ (X Y Z : C),
CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (μ X Y) (CategoryStruct.id (F.obj Z)))
(CategoryStruct.comp (μ (MonoidalCategoryStruct.tensorObj X Y) Z)
(F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) (μ Y Z))
(μ X (MonoidalCategoryStruct.tensorObj Y Z))) := by
cat_disch)
(left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ε (CategoryStruct.id (F.obj X)))
(CategoryStruct.comp (μ (MonoidalCategoryStruct.tensorUnit C) X)
(F.map (MonoidalCategoryStruct.leftUnitor X).hom)) := by
cat_disch)
(right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (F.obj X)) ε)
(CategoryStruct.comp (μ X (MonoidalCategoryStruct.tensorUnit C))
(F.map (MonoidalCategoryStruct.rightUnitor X).hom)) := by
cat_disch)
:
A constructor for lax monoidal functors whose axioms are described by tensorHom instead of
whiskerLeft and whiskerRight.
Instances For
@[implicit_reducible]
instance
CategoryTheory.Functor.LaxMonoidal.id
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.id_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(x✝ x✝¹ : C)
:
μ (Functor.id C) x✝ x✝¹ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((Functor.id C).obj x✝) ((Functor.id C).obj x✝¹))
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.id_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[implicit_reducible]
instance
CategoryTheory.Functor.LaxMonoidal.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(F.comp G).LaxMonoidal
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.comp_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.LaxMonoidal]
[G.LaxMonoidal]
:
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.comp_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.LaxMonoidal]
[G.LaxMonoidal]
(X Y : C)
:
class
CategoryTheory.Functor.OplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
:
Type (max u₁ v₂)
A functor F : C ⥤ D between monoidal categories is oplax monoidal if it is
equipped with morphisms η : F.obj (𝟙_ C) ⟶ 𝟙 _D and δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y,
satisfying the appropriate coherences.
the counit morphism of a lax monoidal functor
- δ (X Y : C) : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)
the cotensorator of an oplax monoidal functor
- δ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ F Y X')
- δ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ F X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ F X' Y)
- oplax_associativity (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))
associativity of the tensorator
- oplax_left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))
- oplax_right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))
Instances
theorem
CategoryTheory.Functor.OplaxMonoidal.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.OplaxMonoidal}
(η : η F = η F)
(δ : δ F = δ F)
:
x = y
theorem
CategoryTheory.Functor.OplaxMonoidal.ext_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.OplaxMonoidal}
:
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
{X Y : C}
(X' : C)
(f : X ⟶ Y)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X') (F.obj Y) ⟶ Z)
:
CategoryStruct.comp (δ F X' X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (CategoryStruct.comp (δ F X' Y) h)
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
{X Y : C}
(f : X ⟶ Y)
(X' : C)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X') ⟶ Z)
:
CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (CategoryStruct.comp (δ F Y X') h)
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.associativity
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))
Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_associativity.
associativity of the tensorator
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.associativity_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶ Z✝)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) h))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.left_unitality
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X : C)
:
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X)
(MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))
Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality.
theorem
CategoryTheory.Functor.OplaxMonoidal.left_unitality_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X : C)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) (F.obj X) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv h = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)) h))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.right_unitality
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X : C)
:
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C))
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))
Alias of CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality.
theorem
CategoryTheory.Functor.OplaxMonoidal.right_unitality_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.OplaxMonoidal]
(X : C)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv h = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)) h))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_natural
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
:
CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (δ F Y Y')
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Y') ⟶ Z)
:
CategoryStruct.comp (δ F X X') (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (δ F Y Y') h)
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X : C)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X))
(MonoidalCategoryStruct.leftUnitor (F.obj X)).hom) = F.map (MonoidalCategoryStruct.leftUnitor X).hom
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X))
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X : C)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F))
(MonoidalCategoryStruct.rightUnitor (F.obj X)).hom) = F.map (MonoidalCategoryStruct.rightUnitor X).hom
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F))
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.associativity_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶ Z✝)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) h))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.tensorHom (η F) f) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom)
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
(MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) Y ⟶ Z)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (η F) f) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom)
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorUnit D) f) h))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.tensorHom f (η F)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom)
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
(MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (η F)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom)
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f (MonoidalCategoryStruct.tensorUnit D)) h))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶ Z✝)
:
CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h)))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom))
theorem
CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶ Z✝)
:
CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)) h) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h)))
@[implicit_reducible]
instance
CategoryTheory.Functor.OplaxMonoidal.id
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.id_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(x✝ x✝¹ : C)
:
δ (Functor.id C) x✝ x✝¹ = CategoryStruct.id ((Functor.id C).obj (MonoidalCategoryStruct.tensorObj x✝ x✝¹))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.id_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
η (Functor.id C) = CategoryStruct.id ((Functor.id C).obj (MonoidalCategoryStruct.tensorUnit C))
@[implicit_reducible]
instance
CategoryTheory.Functor.OplaxMonoidal.comp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(F.comp G).OplaxMonoidal
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.comp_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.comp_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
(X Y : C)
:
class
CategoryTheory.Functor.Monoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
extends F.LaxMonoidal, F.OplaxMonoidal :
Type (max u₁ v₂)
A functor between monoidal categories is monoidal if it is lax and oplax monoidals, and both data give inverse isomorphisms.
- μ (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (MonoidalCategoryStruct.tensorObj X Y)
- μ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ F Y X') = CategoryStruct.comp (μ F X X') (F.map (MonoidalCategoryStruct.whiskerRight f X'))
- μ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ F X' Y) = CategoryStruct.comp (μ F X' X) (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
- associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z)) (μ F X (MonoidalCategoryStruct.tensorObj Y Z)))
- left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε F) (F.obj X)) (CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorUnit C) X) (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
- right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (ε F)) (CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorUnit C)) (F.map (MonoidalCategoryStruct.rightUnitor X).hom))
- δ (X Y : C) : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)
- δ_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (δ F X X') (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (δ F Y X')
- δ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (δ F X' X) (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (δ F X' Y)
- oplax_associativity (X Y Z : C) : CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (δ F X Y) (F.obj Z)) (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorObj Y Z)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (δ F Y Z)))
- oplax_left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) (CategoryStruct.comp (δ F (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.whiskerRight (η F) (F.obj X)))
- oplax_right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) (CategoryStruct.comp (δ F X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.whiskerLeft (F.obj X) (η F)))
- η_ε : CategoryStruct.comp (OplaxMonoidal.η F) (LaxMonoidal.ε F) = CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorUnit C))
- μ_δ (X Y : C) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (OplaxMonoidal.δ F X Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))
- δ_μ (X Y : C) : CategoryStruct.comp (OplaxMonoidal.δ F X Y) (LaxMonoidal.μ F X Y) = CategoryStruct.id (F.obj (MonoidalCategoryStruct.tensorObj X Y))
Instances
theorem
CategoryTheory.Functor.Monoidal.ext_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.Monoidal}
:
x = y ↔ LaxMonoidal.ε F = LaxMonoidal.ε F ∧ LaxMonoidal.μ F = LaxMonoidal.μ F ∧ OplaxMonoidal.η F = OplaxMonoidal.η F ∧ OplaxMonoidal.δ F = OplaxMonoidal.δ F
theorem
CategoryTheory.Functor.Monoidal.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.Monoidal}
(ε : LaxMonoidal.ε F = LaxMonoidal.ε F)
(μ : LaxMonoidal.μ F = LaxMonoidal.μ F)
(η : OplaxMonoidal.η F = OplaxMonoidal.η F)
(δ : OplaxMonoidal.δ F = OplaxMonoidal.δ F)
:
x = y
@[simp]
theorem
CategoryTheory.Functor.Monoidal.δ_μ_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.Monoidal]
(X Y : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ Z)
:
CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (LaxMonoidal.μ F X Y) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.η_ε_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.Monoidal]
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z)
:
CategoryStruct.comp (OplaxMonoidal.η F) (CategoryStruct.comp (LaxMonoidal.ε F) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.ε_η_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.Monoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (OplaxMonoidal.η F) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.μ_δ_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.Monoidal]
(X Y : C)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ Z)
:
CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (OplaxMonoidal.δ F X Y) h) = h
def
CategoryTheory.Functor.Monoidal.εIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
The isomorphism 𝟙_ D ≅ F.obj (𝟙_ C) when F is a monoidal functor.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.εIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
(εIso F).inv = OplaxMonoidal.η F
@[simp]
theorem
CategoryTheory.Functor.Monoidal.εIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
(εIso F).hom = LaxMonoidal.ε F
def
CategoryTheory.Functor.Monoidal.μIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
The isomorphism F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y) when F is a monoidal functor.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.μIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
(μIso F X Y).inv = OplaxMonoidal.δ F X Y
@[simp]
theorem
CategoryTheory.Functor.Monoidal.μIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
(μIso F X Y).hom = LaxMonoidal.μ F X Y
instance
CategoryTheory.Functor.Monoidal.instIsIsoε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
IsIso (LaxMonoidal.ε F)
instance
CategoryTheory.Functor.Monoidal.instIsIsoη
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
IsIso (OplaxMonoidal.η F)
instance
CategoryTheory.Functor.Monoidal.instIsIsoμ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
IsIso (LaxMonoidal.μ F X Y)
instance
CategoryTheory.Functor.Monoidal.instIsIsoδ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
IsIso (OplaxMonoidal.δ F X Y)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_ε_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
:
CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (G.map (OplaxMonoidal.η F)) = CategoryStruct.id (G.obj (MonoidalCategoryStruct.tensorUnit D))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_ε_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
{Z : C'}
(h : G.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
CategoryStruct.comp (G.map (LaxMonoidal.ε F)) (CategoryStruct.comp (G.map (OplaxMonoidal.η F)) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_η_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
:
CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (G.map (LaxMonoidal.ε F)) = CategoryStruct.id (G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_η_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
{Z : C'}
(h : G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (G.map (OplaxMonoidal.η F)) (CategoryStruct.comp (G.map (LaxMonoidal.ε F)) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_μ_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
(X Y : C)
:
CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (G.map (OplaxMonoidal.δ F X Y)) = CategoryStruct.id (G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_μ_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
(X Y : C)
{Z : C'}
(h : G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z)
:
CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) (CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_δ_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
(X Y : C)
:
CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (G.map (LaxMonoidal.μ F X Y)) = CategoryStruct.id (G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.map_δ_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
[F.Monoidal]
(G : Functor D C')
(X Y : C)
{Z : C'}
(h : G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z)
:
CategoryStruct.comp (G.map (OplaxMonoidal.δ F X Y)) (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_ε_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_ε_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit D) T ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_η_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorUnit C)) T ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T)
(MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T)
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) T ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) T)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) T) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_η_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y))
(MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_μ_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj T (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y)) h) = h
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
(T : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj T (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (OplaxMonoidal.δ F X Y))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft T (LaxMonoidal.μ F X Y)) h) = h
theorem
CategoryTheory.Functor.Monoidal.map_tensor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
:
F.map (MonoidalCategoryStruct.tensorHom f g) = CategoryStruct.comp (OplaxMonoidal.δ F X X')
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (LaxMonoidal.μ F Y Y'))
theorem
CategoryTheory.Functor.Monoidal.map_tensor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y Y') ⟶ Z)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h = CategoryStruct.comp (OplaxMonoidal.δ F X X')
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
(CategoryStruct.comp (LaxMonoidal.μ F Y Y') h))
theorem
CategoryTheory.Functor.Monoidal.map_whiskerLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Y Z : C}
(f : Y ⟶ Z)
:
F.map (MonoidalCategoryStruct.whiskerLeft X f) = CategoryStruct.comp (OplaxMonoidal.δ F X Y)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f)) (LaxMonoidal.μ F X Z))
theorem
CategoryTheory.Functor.Monoidal.map_whiskerLeft_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Y Z : C}
(f : Y ⟶ Z)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X Z) ⟶ Z✝)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X f)) h = CategoryStruct.comp (OplaxMonoidal.δ F X Y)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f))
(CategoryStruct.comp (LaxMonoidal.μ F X Z) h))
theorem
CategoryTheory.Functor.Monoidal.map_whiskerRight
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
{X Y : C}
(f : X ⟶ Y)
(Z : C)
:
F.map (MonoidalCategoryStruct.whiskerRight f Z) = CategoryStruct.comp (OplaxMonoidal.δ F X Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z)) (LaxMonoidal.μ F Y Z))
theorem
CategoryTheory.Functor.Monoidal.map_whiskerRight_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
{X Y : C}
(f : X ⟶ Y)
(Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z✝)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f Z)) h = CategoryStruct.comp (OplaxMonoidal.δ F X Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z))
(CategoryStruct.comp (LaxMonoidal.μ F Y Z) h))
theorem
CategoryTheory.Functor.Monoidal.map_associator
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
:
F.map (MonoidalCategoryStruct.associator X Y Z).hom = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z))
(LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z)))))
theorem
CategoryTheory.Functor.Monoidal.map_associator_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z))
(CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h))))
theorem
CategoryTheory.Functor.Monoidal.map_associator_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
:
F.map (MonoidalCategoryStruct.associator X Y Z).inv = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z))
(LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z))))
theorem
CategoryTheory.Functor.Monoidal.map_associator_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) Z) ⟶ Z✝)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv) h = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z))
(CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z) h))))
theorem
CategoryTheory.Functor.Monoidal.map_associator'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
:
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z))
(CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)))))
theorem
CategoryTheory.Functor.Monoidal.map_associator'_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (F.obj X) (MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z)) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.μ F X Y) (F.obj Z))
(CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.δ F Y Z)) h))))
theorem
CategoryTheory.Functor.Monoidal.map_associator_inv'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
:
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z))
(CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)))))
theorem
CategoryTheory.Functor.Monoidal.map_associator_inv'_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y Z : C)
{Z✝ : D}
(h : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) (F.obj Z) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.μ F Y Z))
(CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorObj Y Z))
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).inv)
(CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.δ F X Y) (F.obj Z)) h))))
theorem
CategoryTheory.Functor.Monoidal.map_leftUnitor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
theorem
CategoryTheory.Functor.Monoidal.map_leftUnitor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorUnit C) X)
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (OplaxMonoidal.η F) (F.obj X))
(CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h))
theorem
CategoryTheory.Functor.Monoidal.map_leftUnitor_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
theorem
CategoryTheory.Functor.Monoidal.map_leftUnitor_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv) h = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (LaxMonoidal.ε F) (F.obj X))
(CategoryStruct.comp (LaxMonoidal.μ F (MonoidalCategoryStruct.tensorUnit C) X) h))
theorem
CategoryTheory.Functor.Monoidal.map_rightUnitor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
theorem
CategoryTheory.Functor.Monoidal.map_rightUnitor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h = CategoryStruct.comp (OplaxMonoidal.δ F X (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (OplaxMonoidal.η F))
(CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h))
theorem
CategoryTheory.Functor.Monoidal.map_rightUnitor_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
theorem
CategoryTheory.Functor.Monoidal.map_rightUnitor_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv) h = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (LaxMonoidal.ε F))
(CategoryStruct.comp (LaxMonoidal.μ F X (MonoidalCategoryStruct.tensorUnit C)) h))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.inv_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.inv_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.inv_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
CategoryTheory.inv (LaxMonoidal.μ F X Y) = OplaxMonoidal.δ F X Y
@[simp]
theorem
CategoryTheory.Functor.Monoidal.inv_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X Y : C)
:
CategoryTheory.inv (OplaxMonoidal.δ F X Y) = LaxMonoidal.μ F X Y
def
CategoryTheory.Functor.Monoidal.μNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
:
The tensorator as a natural isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.μNatIso_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C × C)
:
(μNatIso F).inv.app X = OplaxMonoidal.δ F X.1 X.2
@[simp]
theorem
CategoryTheory.Functor.Monoidal.μNatIso_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C × C)
:
(μNatIso F).hom.app X = LaxMonoidal.μ F X.1 X.2
def
CategoryTheory.Functor.Monoidal.commTensorLeft
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
Monoidal functors commute with left tensoring up to isomorphism
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.commTensorLeft_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X X✝ : C)
:
(commTensorLeft F X).hom.app X✝ = LaxMonoidal.μ F X X✝
@[simp]
theorem
CategoryTheory.Functor.Monoidal.commTensorLeft_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X X✝ : C)
:
(commTensorLeft F X).inv.app X✝ = OplaxMonoidal.δ F X X✝
def
CategoryTheory.Functor.Monoidal.commTensorRight
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X : C)
:
Monoidal functors commute with right tensoring up to isomorphism
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.commTensorRight_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X X✝ : C)
:
(commTensorRight F X).hom.app X✝ = LaxMonoidal.μ F X✝ X
@[simp]
theorem
CategoryTheory.Functor.Monoidal.commTensorRight_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
(X X✝ : C)
:
(commTensorRight F X).inv.app X✝ = OplaxMonoidal.δ F X✝ X
@[implicit_reducible]
instance
CategoryTheory.Functor.Monoidal.instId
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
(Functor.id C).Monoidal
@[implicit_reducible]
instance
CategoryTheory.Functor.Monoidal.instComp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor D E)
[F.Monoidal]
[G.Monoidal]
:
theorem
CategoryTheory.Functor.Monoidal.toLaxMonoidal_injective
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
:
Function.Injective (@toLaxMonoidal C inst✝ inst✝¹ D inst✝² inst✝³ F)
theorem
CategoryTheory.Functor.Monoidal.toOplaxMonoidal_injective
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
:
Function.Injective (@toOplaxMonoidal C inst✝ inst✝¹ D inst✝² inst✝³ F)
structure
CategoryTheory.Functor.CoreMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
:
Type (max u₁ v₂)
Structure which is a helper in order to show that a functor is monoidal. It
consists of isomorphisms εIso and μIso such that the morphisms .hom induced
by these isomorphisms satisfy the axioms of lax monoidal functors.
unit morphism
- μIso (X Y : C) : MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y)
tensorator
- μIso_hom_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (self.μIso Y X').hom = CategoryStruct.comp (self.μIso X X').hom (F.map (MonoidalCategoryStruct.whiskerRight f X'))
- μIso_hom_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (self.μIso X' Y).hom = CategoryStruct.comp (self.μIso X' X).hom (F.map (MonoidalCategoryStruct.whiskerLeft X' f))
- associativity (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom (F.map (MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom) (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom)
associativity of the tensorator
- left_unitality (X : C) : (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X)) (CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorUnit C) X).hom (F.map (MonoidalCategoryStruct.leftUnitor X).hom))
- right_unitality (X : C) : (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom) (CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorUnit C)).hom (F.map (MonoidalCategoryStruct.rightUnitor X).hom))
Instances For
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.associativity_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (self.μIso X Y).hom (F.obj Z))
(CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorObj X Y) Z).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (self.μIso Y Z).hom)
(CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorObj Y Z)).hom h))
associativity of the tensorator
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
{X Y : C}
(X' : C)
(f : X ⟶ Y)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
(CategoryStruct.comp (self.μIso X' Y).hom h) = CategoryStruct.comp (self.μIso X' X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h)
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
{X Y : C}
(f : X ⟶ Y)
(X' : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
(CategoryStruct.comp (self.μIso Y X').hom h) = CategoryStruct.comp (self.μIso X X').hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)
theorem
CategoryTheory.Functor.CoreMonoidal.right_unitality_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom)
(CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorUnit C)).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))
theorem
CategoryTheory.Functor.CoreMonoidal.left_unitality_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X))
(CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorUnit C) X).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))
def
CategoryTheory.Functor.CoreMonoidal.mk'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
:
Alternative constructor for CoreMonoidal, for which the axioms are stated
in terms on the inverses of εIso and μIso.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.mk'_μIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
(X Y : C)
:
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.mk'_εIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
:
@[implicit_reducible]
def
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
The lax monoidal functor structure induced by a Functor.CoreMonoidal structure.
Instances For
theorem
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
(X Y : C)
:
LaxMonoidal.μ F X Y = (h.μIso X Y).hom
theorem
CategoryTheory.Functor.CoreMonoidal.toLaxMonoidal_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
LaxMonoidal.ε F = h.εIso.hom
@[implicit_reducible]
def
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
The oplax monoidal functor structure induced by a Functor.CoreMonoidal structure.
Instances For
theorem
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
(X Y : C)
:
OplaxMonoidal.δ F X Y = (h.μIso X Y).inv
theorem
CategoryTheory.Functor.CoreMonoidal.toOplaxMonoidal_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
OplaxMonoidal.η F = h.εIso.inv
@[implicit_reducible]
def
CategoryTheory.Functor.CoreMonoidal.toMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
F.Monoidal
The monoidal functor structure induced by a Functor.CoreMonoidal structure.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(h : F.CoreMonoidal)
:
noncomputable def
CategoryTheory.Functor.CoreMonoidal.ofLaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
[IsIso (LaxMonoidal.ε F)]
[∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)]
:
The Functor.CoreMonoidal structure given by a lax monoidal functor such
that ε and μ are isomorphisms.
Instances For
noncomputable def
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
[IsIso (OplaxMonoidal.η F)]
[∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)]
:
The Functor.CoreMonoidal structure given by an oplax monoidal functor such
that η and δ are isomorphisms.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_εIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
[IsIso (OplaxMonoidal.η F)]
[∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)]
:
(ofOplaxMonoidal F).εIso = (asIso (OplaxMonoidal.η F)).symm
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_μIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
[IsIso (OplaxMonoidal.η F)]
[∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)]
(X Y : C)
:
(ofOplaxMonoidal F).μIso X Y = (asIso (OplaxMonoidal.δ F X Y)).symm
@[implicit_reducible]
noncomputable def
CategoryTheory.Functor.Monoidal.ofLaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
[IsIso (LaxMonoidal.ε F)]
[∀ (X Y : C), IsIso (LaxMonoidal.μ F X Y)]
:
F.Monoidal
The Functor.Monoidal structure given by a lax monoidal functor such
that ε and μ are isomorphisms.
Instances For
@[implicit_reducible]
noncomputable def
CategoryTheory.Functor.Monoidal.ofOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.OplaxMonoidal]
[IsIso (OplaxMonoidal.η F)]
[∀ (X Y : C), IsIso (OplaxMonoidal.δ F X Y)]
:
F.Monoidal
The Functor.Monoidal structure given by an oplax monoidal functor such
that η and δ are isomorphisms.
Instances For
@[implicit_reducible]
instance
CategoryTheory.Functor.instLaxMonoidalProdProd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(F.prod G).LaxMonoidal
@[simp]
theorem
CategoryTheory.Functor.prod_ε_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(LaxMonoidal.ε (F.prod G)).1 = LaxMonoidal.ε F
@[simp]
theorem
CategoryTheory.Functor.prod_ε_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(LaxMonoidal.ε (F.prod G)).2 = LaxMonoidal.ε G
@[simp]
theorem
CategoryTheory.Functor.prod_μ_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.LaxMonoidal]
[G.LaxMonoidal]
(X Y : C × E)
:
(LaxMonoidal.μ (F.prod G) X Y).1 = LaxMonoidal.μ F X.1 Y.1
@[simp]
theorem
CategoryTheory.Functor.prod_μ_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.LaxMonoidal]
[G.LaxMonoidal]
(X Y : C × E)
:
(LaxMonoidal.μ (F.prod G) X Y).2 = LaxMonoidal.μ G X.2 Y.2
@[implicit_reducible]
instance
CategoryTheory.Functor.instOplaxMonoidalProdProd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(F.prod G).OplaxMonoidal
@[simp]
theorem
CategoryTheory.Functor.prod_η_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(OplaxMonoidal.η (F.prod G)).1 = OplaxMonoidal.η F
@[simp]
theorem
CategoryTheory.Functor.prod_η_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(OplaxMonoidal.η (F.prod G)).2 = OplaxMonoidal.η G
@[simp]
theorem
CategoryTheory.Functor.prod_δ_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.OplaxMonoidal]
[G.OplaxMonoidal]
(X Y : C × E)
:
(OplaxMonoidal.δ (F.prod G) X Y).1 = OplaxMonoidal.δ F X.1 Y.1
@[simp]
theorem
CategoryTheory.Functor.prod_δ_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.OplaxMonoidal]
[G.OplaxMonoidal]
(X Y : C × E)
:
(OplaxMonoidal.δ (F.prod G) X Y).2 = OplaxMonoidal.δ G X.2 Y.2
@[implicit_reducible]
instance
CategoryTheory.Functor.instMonoidalProdProd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{C' : Type u₁'}
[Category.{v₁', u₁'} C']
(F : Functor C D)
(G : Functor E C')
[MonoidalCategory C']
[F.Monoidal]
[G.Monoidal]
:
@[implicit_reducible]
instance
CategoryTheory.Functor.instMonoidalProdDiag
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[simp]
theorem
CategoryTheory.Functor.diag_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
LaxMonoidal.ε (diag C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit (C × C))
@[simp]
theorem
CategoryTheory.Functor.diag_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
OplaxMonoidal.η (diag C) = CategoryStruct.id ((diag C).obj (MonoidalCategoryStruct.tensorUnit C))
@[simp]
theorem
CategoryTheory.Functor.diag_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X Y : C)
:
LaxMonoidal.μ (diag C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((diag C).obj X) ((diag C).obj Y))
@[simp]
theorem
CategoryTheory.Functor.diag_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(X Y : C)
:
OplaxMonoidal.δ (diag C) X Y = CategoryStruct.id ((diag C).obj (MonoidalCategoryStruct.tensorObj X Y))
@[implicit_reducible]
instance
CategoryTheory.Functor.LaxMonoidal.prod'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(F.prod' G).LaxMonoidal
The functor C ⥤ D × E obtained from two lax monoidal functors is lax monoidal.
@[simp]
theorem
CategoryTheory.Functor.prod'_ε_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(LaxMonoidal.ε (F.prod' G)).1 = LaxMonoidal.ε F
@[simp]
theorem
CategoryTheory.Functor.prod'_ε_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.LaxMonoidal]
[G.LaxMonoidal]
:
(LaxMonoidal.ε (F.prod' G)).2 = LaxMonoidal.ε G
@[simp]
theorem
CategoryTheory.Functor.prod'_μ_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.LaxMonoidal]
[G.LaxMonoidal]
(X Y : C)
:
(LaxMonoidal.μ (F.prod' G) X Y).1 = LaxMonoidal.μ F X Y
@[simp]
theorem
CategoryTheory.Functor.prod'_μ_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.LaxMonoidal]
[G.LaxMonoidal]
(X Y : C)
:
(LaxMonoidal.μ (F.prod' G) X Y).2 = LaxMonoidal.μ G X Y
@[implicit_reducible]
instance
CategoryTheory.Functor.OplaxMonoidal.prod'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(F.prod' G).OplaxMonoidal
The functor C ⥤ D × E obtained from two oplax monoidal functors is oplax monoidal.
@[simp]
theorem
CategoryTheory.Functor.prod'_η_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(OplaxMonoidal.η (F.prod' G)).1 = OplaxMonoidal.η F
@[simp]
theorem
CategoryTheory.Functor.prod'_η_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
:
(OplaxMonoidal.η (F.prod' G)).2 = OplaxMonoidal.η G
@[simp]
theorem
CategoryTheory.Functor.prod'_δ_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
(X Y : C)
:
(OplaxMonoidal.δ (F.prod' G) X Y).1 = OplaxMonoidal.δ F X Y
@[simp]
theorem
CategoryTheory.Functor.prod'_δ_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.OplaxMonoidal]
[G.OplaxMonoidal]
(X Y : C)
:
(OplaxMonoidal.δ (F.prod' G) X Y).2 = OplaxMonoidal.δ G X Y
@[implicit_reducible]
instance
CategoryTheory.Functor.Monoidal.prod'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(F : Functor C D)
(G : Functor C E)
[F.Monoidal]
[G.Monoidal]
:
The functor C ⥤ D × E obtained from two monoidal functors is monoidal.
@[implicit_reducible]
def
CategoryTheory.Adjunction.rightAdjointLaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
:
The right adjoint of an oplax monoidal functor is lax monoidal.
Instances For
theorem
CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
(X Y : D)
:
Functor.LaxMonoidal.μ G X Y = (adj.homEquiv (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
(MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)))
theorem
CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
:
class
CategoryTheory.Adjunction.IsMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
:
When adj : F ⊣ G is an adjunction, with F oplax monoidal and G lax-monoidal,
this typeclass expresses compatibilities between the adjunction and the (op)lax
monoidal structures.
- leftAdjoint_ε : Functor.LaxMonoidal.ε G = CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) (G.map (Functor.OplaxMonoidal.η F))
- leftAdjoint_μ (X Y : D) : Functor.LaxMonoidal.μ G X Y = CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y))) (G.map (CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y)) (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))))
Instances
instance
CategoryTheory.Adjunction.instIsMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
:
adj.IsMonoidal
theorem
CategoryTheory.Adjunction.unit_app_unit_comp_map_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
:
CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) (G.map (Functor.OplaxMonoidal.η F)) = Functor.LaxMonoidal.ε G
theorem
CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
{Z : C}
(h : G.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C))
(CategoryStruct.comp (G.map (Functor.OplaxMonoidal.η F)) h) = CategoryStruct.comp (Functor.LaxMonoidal.ε G) h
theorem
CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
(X Y : C)
:
CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y)) (G.map (Functor.OplaxMonoidal.δ F X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
(Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))
theorem
CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
(X Y : C)
{Z : C}
(h : G.obj (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) ⟶ Z)
:
CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (G.map (Functor.OplaxMonoidal.δ F X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
(CategoryStruct.comp (Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)) h)
theorem
CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
:
CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G)) (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) = Functor.OplaxMonoidal.η F
theorem
CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
CategoryStruct.comp (F.map (Functor.LaxMonoidal.ε G))
(CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.η F) h
theorem
CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
(X Y : D)
:
CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y)) (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
(MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y))
theorem
CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
(X Y : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z)
:
CategoryStruct.comp (F.map (Functor.LaxMonoidal.μ G X Y))
(CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ F (G.obj X) (G.obj Y))
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.counit.app X) (adj.counit.app Y)) h)
instance
CategoryTheory.Adjunction.instIsMonoidalId
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
instance
CategoryTheory.Adjunction.isMonoidal_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.OplaxMonoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
{F' : Functor D E}
{G' : Functor E D}
(adj' : F' ⊣ G')
[F'.OplaxMonoidal]
[G'.LaxMonoidal]
[adj'.IsMonoidal]
:
(adj.comp adj').IsMonoidal
@[implicit_reducible]
def
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
The left adjoint of a lax monoidal functor is oplax monoidal.
Instances For
theorem
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
(X Y : C)
:
Functor.OplaxMonoidal.δ F X Y = (adj.homEquiv (MonoidalCategoryStruct.tensorObj X Y) (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))).symm
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
(Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)))
theorem
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
instance
CategoryTheory.Adjunction.instIsMonoidal_1
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
adj.IsMonoidal
def
CategoryTheory.Adjunction.laxMonoidalEquivOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
:
If F ⊣ G is an adjunction, the G is lax monoidal iff F is oplax monoidal.
It is advisable to use Adjunction.leftAdjointOplaxMonoidal and
Adjunction.rightAdjointLaxMonoidal, because compatibilities between
the oplax monoidal left adjoint and the lax monoidal right adjoint
(Adjunction.IsMonoidal) have been stated for these definitions.
Instances For
theorem
CategoryTheory.Adjunction.ε_comp_map_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
:
CategoryStruct.comp (Functor.LaxMonoidal.ε G) (G.map (Functor.LaxMonoidal.ε F)) = adj.unit.app (MonoidalCategoryStruct.tensorUnit C)
theorem
CategoryTheory.Adjunction.ε_comp_map_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
{Z : C}
(h : G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp (G.map (Functor.LaxMonoidal.ε F)) h) = CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) h
theorem
CategoryTheory.Adjunction.map_η_comp_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
:
CategoryStruct.comp (F.map (Functor.OplaxMonoidal.η G)) (Functor.OplaxMonoidal.η F) = adj.counit.app (MonoidalCategoryStruct.tensorUnit D)
theorem
CategoryTheory.Adjunction.map_η_comp_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
CategoryStruct.comp (F.map (Functor.OplaxMonoidal.η G)) (CategoryStruct.comp (Functor.OplaxMonoidal.η F) h) = CategoryStruct.comp (adj.counit.app (MonoidalCategoryStruct.tensorUnit D)) h
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalFunctorSymmOfInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.inverse.Monoidal]
:
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalInverseSymmOfFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
:
@[implicit_reducible]
noncomputable def
CategoryTheory.Equivalence.inverseMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
:
If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Equivalence.IsMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
An equivalence of categories involving monoidal functors is monoidal if the underlying adjunction satisfies certain compatibilities with respect to the monoidal functor data.
Instances For
theorem
CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
theorem
CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : C}
(h : e.inverse.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
theorem
CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
:
CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y))
(e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))
(Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))
theorem
CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
{Z : C}
(h : e.inverse.obj (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z)
:
CategoryStruct.comp (e.unitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))
(CategoryStruct.comp (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)
theorem
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
theorem
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
theorem
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : D)
:
CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y))
(e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
(MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y))
theorem
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counitIso_hom_app_tensor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z)
:
CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y))
(CategoryStruct.comp (e.counitIso.hom.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.counitIso.hom.app X) (e.counitIso.hom.app Y)) h)
theorem
CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
theorem
CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : D}
(h : e.functor.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z)
:
theorem
CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
:
CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
(e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y)
(e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
theorem
CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
{Z : D}
(h :
e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))) ⟶ Z)
:
CategoryStruct.comp (e.counitIso.inv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
(CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y)
(CategoryStruct.comp (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
h)
theorem
CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
theorem
CategoryTheory.Equivalence.unit_app_comp_inverse_map_η_functor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : C}
(h : e.inverse.obj (MonoidalCategoryStruct.tensorUnit D) ⟶ Z)
:
theorem
CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
:
CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorObj X Y))
(e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y))
(Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))
theorem
CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
{Z : C}
(h : e.inverse.obj (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)) ⟶ Z)
:
CategoryStruct.comp (e.unit.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (e.inverse.map (Functor.OplaxMonoidal.δ e.functor X Y)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y))
(CategoryStruct.comp (Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y)) h)
@[simp]
theorem
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
theorem
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : D)
:
CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y))
(e.counit.app (MonoidalCategoryStruct.tensorObj X Y)) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
(MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y))
theorem
CategoryTheory.Equivalence.functor_map_μ_inverse_comp_counit_app_tensor_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : D)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z)
:
CategoryStruct.comp (e.functor.map (Functor.LaxMonoidal.μ e.inverse X Y))
(CategoryStruct.comp (e.counit.app (MonoidalCategoryStruct.tensorObj X Y)) h) = CategoryStruct.comp (Functor.OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y))
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (e.counit.app X) (e.counit.app Y)) h)
theorem
CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
theorem
CategoryTheory.Equivalence.counitInv_app_comp_functor_map_η_inverse_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : D}
(h : e.functor.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z)
:
theorem
CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
:
CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
(e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y)
(e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
theorem
CategoryTheory.Equivalence.counitInv_app_tensor_comp_functor_map_δ_inverse_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(X Y : C)
{Z : D}
(h :
e.functor.obj (MonoidalCategoryStruct.tensorObj (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))) ⟶ Z)
:
CategoryStruct.comp (e.counitInv.app (MonoidalCategoryStruct.tensorObj (e.functor.obj X) (e.functor.obj Y)))
(CategoryStruct.comp (e.functor.map (Functor.OplaxMonoidal.δ e.inverse (e.functor.obj X) (e.functor.obj Y))) h) = CategoryStruct.comp (Functor.LaxMonoidal.μ e.functor X Y)
(CategoryStruct.comp (e.functor.map (MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y)))
h)
@[simp]
theorem
CategoryTheory.Equivalence.ε_comp_map_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.ε_comp_map_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : C}
(h : e.inverse.obj (e.functor.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Equivalence.map_η_comp_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.Equivalence.map_η_comp_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalFunctorRefl
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalInverseRefl
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
instance
CategoryTheory.Equivalence.isMonoidal_refl
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
The obvious auto-equivalence of a monoidal category is monoidal.
instance
CategoryTheory.Equivalence.isMonoidal_symm
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
The inverse of a monoidal category equivalence is also a monoidal category equivalence.
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalFunctorTrans
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
[e.functor.Monoidal]
(e' : D ≌ E)
[e'.functor.Monoidal]
:
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalInverseTrans
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
[e.inverse.Monoidal]
(e' : D ≌ E)
[e'.inverse.Monoidal]
:
instance
CategoryTheory.Equivalence.isMonoidal_trans
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
(e' : D ≌ E)
[e'.functor.Monoidal]
[e'.inverse.Monoidal]
[e'.IsMonoidal]
:
(e.trans e').IsMonoidal
The composition of two monoidal category equivalences is monoidal.
structure
CategoryTheory.LaxMonoidalFunctor
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
extends CategoryTheory.Functor C D :
Type (max (max (max u₁ u₂) v₁) v₂)
Bundled version of lax monoidal functors. This type is equipped with a category
structure in CategoryTheory.Monoidal.NaturalTransformation.
- obj : C → D
- map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
- laxMonoidal : self.LaxMonoidal
Instances For
def
CategoryTheory.LaxMonoidalFunctor.of
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
:
Constructor for LaxMonoidalFunctor C D.
Instances For
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.of_toFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C D)
[F.LaxMonoidal]
:
def
CategoryTheory.Functor.Monoidal.coreMonoidalTransport
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
Auxiliary definition for Functor.Monoidal.transport
Instances For
@[simp]
theorem
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
:
((coreMonoidalTransport i).μIso X Y).inv = CategoryStruct.comp (i.inv.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (OplaxMonoidal.δ F X Y) (MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
(coreMonoidalTransport i).εIso.hom = CategoryStruct.comp (LaxMonoidal.ε F) (i.hom.app (MonoidalCategoryStruct.tensorUnit C))
@[simp]
theorem
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_εIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
:
((coreMonoidalTransport i).μIso X Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
(CategoryStruct.comp (LaxMonoidal.μ F X Y) (i.hom.app (MonoidalCategoryStruct.tensorObj X Y)))
@[implicit_reducible]
def
CategoryTheory.Functor.Monoidal.transport
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
G.Monoidal
Transport the structure of a monoidal functor along a natural isomorphism of functors.
Instances For
theorem
CategoryTheory.Functor.Monoidal.transport_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
LaxMonoidal.ε G = CategoryStruct.comp (LaxMonoidal.ε F) (i.hom.app (MonoidalCategoryStruct.tensorUnit C))
theorem
CategoryTheory.Functor.Monoidal.transport_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
{Z : D}
(h : G.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z)
:
CategoryStruct.comp (LaxMonoidal.ε G) h = CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (i.hom.app (MonoidalCategoryStruct.tensorUnit C)) h)
theorem
CategoryTheory.Functor.Monoidal.transport_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
:
theorem
CategoryTheory.Functor.Monoidal.transport_η_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
{Z : D}
(h : MonoidalCategoryStruct.tensorUnit D ⟶ Z)
:
theorem
CategoryTheory.Functor.Monoidal.transport_μ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
:
LaxMonoidal.μ G X Y = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
(CategoryStruct.comp (LaxMonoidal.μ F X Y) (i.hom.app (MonoidalCategoryStruct.tensorObj X Y)))
theorem
CategoryTheory.Functor.Monoidal.transport_μ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
{Z : D}
(h : G.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ Z)
:
CategoryStruct.comp (LaxMonoidal.μ G X Y) h = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (i.inv.app X) (i.inv.app Y))
(CategoryStruct.comp (LaxMonoidal.μ F X Y)
(CategoryStruct.comp (i.hom.app (MonoidalCategoryStruct.tensorObj X Y)) h))
theorem
CategoryTheory.Functor.Monoidal.transport_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
:
OplaxMonoidal.δ G X Y = CategoryStruct.comp (i.inv.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (OplaxMonoidal.δ F X Y) (MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)))
theorem
CategoryTheory.Functor.Monoidal.transport_δ_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F G : Functor C D}
[F.Monoidal]
(i : F ≅ G)
(X Y : C)
{Z : D}
(h : MonoidalCategoryStruct.tensorObj (G.obj X) (G.obj Y) ⟶ Z)
:
CategoryStruct.comp (OplaxMonoidal.δ G X Y) h = CategoryStruct.comp (i.inv.app (MonoidalCategoryStruct.tensorObj X Y))
(CategoryStruct.comp (OplaxMonoidal.δ F X Y)
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (i.hom.app X) (i.hom.app Y)) h))
@[implicit_reducible]
def
CategoryTheory.Equivalence.monoidalOfPrecompFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
(F : Functor D E)
{F' : Functor C E}
(i : e.functor.comp F ≅ F')
[e.inverse.Monoidal]
[F'.Monoidal]
:
F.Monoidal
Given a functor F and an equivalence of categories e such that e.inverse and e.functor ⋙ F
are monoidal functors, F is monoidal as well.
Instances For
@[implicit_reducible]
def
CategoryTheory.Equivalence.monoidalOfPrecompInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
(F : Functor C E)
{F' : Functor D E}
(i : e.inverse.comp F ≅ F')
[e.functor.Monoidal]
[F'.Monoidal]
:
F.Monoidal
Given a functor F and an equivalence of categories e such that e.functor and e.inverse ⋙ F
are monoidal functors, F is monoidal as well.
Instances For
@[implicit_reducible]
def
CategoryTheory.Equivalence.monoidalOfPostcompInverse
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
(F : Functor E D)
{F' : Functor E C}
(i : F.comp e.inverse ≅ F')
[e.functor.Monoidal]
[F'.Monoidal]
:
F.Monoidal
Given a functor F and an equivalence of categories e such that e.functor and F ⋙ e.inverse
are monoidal functors, F is monoidal as well.
Instances For
@[implicit_reducible]
def
CategoryTheory.Equivalence.monoidalOfPostcompFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{E : Type u₃}
[Category.{v₃, u₃} E]
[MonoidalCategory E]
(e : C ≌ D)
(F : Functor E C)
{F' : Functor E D}
(i : F.comp e.functor ≅ F')
[e.inverse.Monoidal]
[F'.Monoidal]
:
F.Monoidal
Given a functor F and an equivalence of categories e such that e.inverse and F ⋙ e.functor
are monoidal functors, F is monoidal as well.