(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)
:
@[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
@[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)
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
instance
CategoryTheory.Functor.LaxMonoidal.id
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
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✝¹))
@[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
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
@[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]
:
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)
:
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_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.δ_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.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]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
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✝¹))
@[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
Equations
- One or more equations did not get rendered due to their size.
@[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
{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)
:
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
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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.
Equations
- CategoryTheory.Functor.Monoidal.εIso F = { hom := CategoryTheory.Functor.LaxMonoidal.ε F, inv := CategoryTheory.Functor.OplaxMonoidal.η F, hom_inv_id := ⋯, inv_hom_id := ⋯ }
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]
:
@[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]
:
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.
Equations
- CategoryTheory.Functor.Monoidal.μIso F X Y = { hom := CategoryTheory.Functor.LaxMonoidal.μ F X Y, inv := CategoryTheory.Functor.OplaxMonoidal.δ F X Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[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)
:
@[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)
:
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)
:
@[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)
:
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.
Equations
- CategoryTheory.Functor.Monoidal.μNatIso F = CategoryTheory.NatIso.ofComponents (fun (x : C × C) => CategoryTheory.Functor.Monoidal.μIso F x.1 x.2) ⋯
Instances For
@[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)
:
@[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)
:
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
Equations
- CategoryTheory.Functor.Monoidal.commTensorLeft F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.Functor.Monoidal.μIso F X Y) ⋯
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)
:
@[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)
:
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
Equations
- CategoryTheory.Functor.Monoidal.commTensorRight F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.Functor.Monoidal.μIso F Y X) ⋯
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)
:
@[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)
:
@[implicit_reducible]
instance
CategoryTheory.Functor.Monoidal.instId
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
(Functor.id C).Monoidal
Equations
- One or more equations did not get rendered due to their size.
@[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]
:
Equations
- One or more equations did not get rendered due to their size.
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.μ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)
@[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)
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))
@[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.
Equations
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)
:
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)
:
@[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.
Equations
- One or more equations did not get rendered due to their size.
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)
:
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)
:
@[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.
Equations
- h.toMonoidal = { toLaxMonoidal := h.toLaxMonoidal, toOplaxMonoidal := h.toOplaxMonoidal, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }
Instances For
@[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)
:
@[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)
:
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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)]
(X Y : C)
:
@[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)]
:
@[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.
Equations
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.
Equations
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
Equations
- One or more equations did not get rendered due to their size.
@[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]
:
@[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]
:
@[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)
:
@[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)
:
@[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
Equations
- One or more equations did not get rendered due to their size.
@[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]
:
@[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]
:
@[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)
:
@[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)
:
@[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]
:
Equations
- F.instMonoidalProdProd G = { toLaxMonoidal := F.instLaxMonoidalProdProd G, toOplaxMonoidal := F.instOplaxMonoidalProdProd G, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }
@[implicit_reducible]
instance
CategoryTheory.Functor.instMonoidalProdDiag
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[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.
Equations
@[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]
:
@[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]
:
@[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)
:
@[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)
:
@[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.
Equations
@[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]
:
@[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]
:
@[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)
:
@[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)
:
@[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.
Equations
- One or more equations did not get rendered due to their size.
@[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
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]
:
@[simp]
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)))
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]
:
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
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]
:
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)
:
@[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]
:
Equations
@[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]
:
Equations
@[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.
Equations
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]
:
Equations
- e.instMonoidalFunctorTrans e' = inferInstanceAs (e.functor.comp 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]
:
Equations
- e.instMonoidalInverseTrans e' = inferInstanceAs (e'.inverse.comp 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.
Equations
- CategoryTheory.LaxMonoidalFunctor.of F = { toFunctor := F, laxMonoidal := inferInstance }
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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_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.
Equations
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)
:
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)
:
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.
Equations
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.
Equations
- e.monoidalOfPrecompInverse F i = e.symm.monoidalOfPrecompFunctor F i
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- e.monoidalOfPostcompFunctor F i = e.symm.monoidalOfPostcompInverse F i