(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
{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)
:
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}
:
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
{X Y : C}
(f : X ⟶ Y)
(X' : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryStruct.comp (μ F Y X') h) = CategoryStruct.comp (μ F X X') (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)
@[simp]
theorem
CategoryTheory.Functor.LaxMonoidal.associativity_assoc
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
(F : Functor C D)
[self : F.LaxMonoidal]
(X Y Z : C)
{Z✝ : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X (MonoidalCategoryStruct.tensorObj Y Z)) ⟶ Z✝)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μ F X Y) (F.obj Z))
(CategoryStruct.comp (μ F (MonoidalCategoryStruct.tensorObj X Y) Z)
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ F Y Z))
(CategoryStruct.comp (μ F X (MonoidalCategoryStruct.tensorObj Y Z)) h))
associativity of the tensorator
@[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)
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_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}
:
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)
:
@[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]
(x✝ x✝¹ : C)
:
δ (Functor.id C) x✝ x✝¹ = CategoryStruct.id ((Functor.id C).obj (MonoidalCategoryStruct.tensorObj x✝ x✝¹))
@[simp]
theorem
CategoryTheory.Functor.OplaxMonoidal.id_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
@[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_iff
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.Monoidal}
:
x = y ↔ LaxMonoidal.ε F = LaxMonoidal.ε F ∧ LaxMonoidal.μ F = LaxMonoidal.μ F ∧ OplaxMonoidal.η F = OplaxMonoidal.η F ∧ OplaxMonoidal.δ F = OplaxMonoidal.δ F
theorem
CategoryTheory.Functor.Monoidal.ext
{C : Type u₁}
{inst✝ : Category.{v₁, u₁} C}
{inst✝¹ : MonoidalCategory C}
{D : Type u₂}
{inst✝² : Category.{v₂, u₂} D}
{inst✝³ : MonoidalCategory D}
{F : Functor C D}
{x y : F.Monoidal}
(ε : LaxMonoidal.ε F = LaxMonoidal.ε F)
(μ : LaxMonoidal.μ F = LaxMonoidal.μ F)
(η : OplaxMonoidal.η F = OplaxMonoidal.η F)
(δ : OplaxMonoidal.δ F = OplaxMonoidal.δ F)
:
@[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]
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ 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]
(X Y : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X Y) ⟶ 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_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)
:
@[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)
:
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_right_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
{X Y : C}
(X' : C)
(f : X ⟶ Y)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj X' Y) ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
(CategoryStruct.comp (self.μIso X' Y).hom h) = CategoryStruct.comp (self.μIso X' X).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) h)
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
{X Y : C}
(f : X ⟶ Y)
(X' : C)
{Z : D}
(h : F.obj (MonoidalCategoryStruct.tensorObj Y X') ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
(CategoryStruct.comp (self.μIso Y X').hom h) = CategoryStruct.comp (self.μIso X X').hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) h)
@[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
theorem
CategoryTheory.Functor.CoreMonoidal.right_unitality_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj X) self.εIso.hom)
(CategoryStruct.comp (self.μIso X (MonoidalCategoryStruct.tensorUnit C)).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).hom) h))
theorem
CategoryTheory.Functor.CoreMonoidal.left_unitality_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(self : F.CoreMonoidal)
(X : C)
{Z : D}
(h : F.obj X ⟶ Z)
:
CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight self.εIso.hom (F.obj X))
(CategoryStruct.comp (self.μIso (MonoidalCategoryStruct.tensorUnit C) X).hom
(CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).hom) h))
def
CategoryTheory.Functor.CoreMonoidal.mk'
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
:
Alternative constructor for CoreMonoidal, for which the axioms are stated
in terms on the inverses of εIso and μIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.mk'_εIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
:
@[simp]
theorem
CategoryTheory.Functor.CoreMonoidal.mk'_μIso
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
(εIso : MonoidalCategoryStruct.tensorUnit D ≅ F.obj (MonoidalCategoryStruct.tensorUnit C))
(μIso : (X Y : C) → MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (MonoidalCategoryStruct.tensorObj X Y))
(μIso_inv_natural_left :
∀ {X Y : C} (f : X ⟶ Y) (X' : C),
CategoryStruct.comp (μIso X X').inv (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f X')) (μIso Y X').inv := by
cat_disch)
(μIso_inv_natural_right :
∀ {X Y : C} (X' : C) (f : X ⟶ Y),
CategoryStruct.comp (μIso X' X).inv (MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft X' f)) (μIso X' Y).inv := by
cat_disch)
(oplax_associativity :
∀ (X Y Z : C),
CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorObj X Y) Z).inv
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (μIso X Y).inv (F.obj Z))
(MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryStruct.comp (F.map (MonoidalCategoryStruct.associator X Y Z).hom)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorObj Y Z)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) (μIso Y Z).inv)) := by
cat_disch)
(oplax_left_unitality :
∀ (X : C),
(MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor X).inv)
(CategoryStruct.comp (μIso (MonoidalCategoryStruct.tensorUnit C) X).inv
(MonoidalCategoryStruct.whiskerRight εIso.inv (F.obj X))) := by
cat_disch)
(oplax_right_unitality :
∀ (X : C),
(MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor X).inv)
(CategoryStruct.comp (μIso X (MonoidalCategoryStruct.tensorUnit C)).inv
(MonoidalCategoryStruct.whiskerLeft (F.obj X) εIso.inv)) := by
cat_disch)
(X Y : C)
:
@[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)
:
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)
:
@[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)]
:
@[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)
:
@[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
- 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]
(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
- 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]
(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
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]
:
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
@[implicit_reducible]
def
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
The left adjoint of a lax monoidal functor is oplax monoidal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
theorem
CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_δ
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
(X Y : C)
:
Functor.OplaxMonoidal.δ F X Y = (adj.homEquiv (MonoidalCategoryStruct.tensorObj X Y) (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))).symm
(CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (adj.unit.app X) (adj.unit.app Y))
(Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y)))
instance
CategoryTheory.Adjunction.instIsMonoidal_1
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[G.LaxMonoidal]
:
adj.IsMonoidal
def
CategoryTheory.Adjunction.laxMonoidalEquivOplaxMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
:
If F ⊣ G is an adjunction, the G is lax monoidal iff F is oplax monoidal.
It is advisable to use Adjunction.leftAdjointOplaxMonoidal and
Adjunction.rightAdjointLaxMonoidal, because compatibilities between
the oplax monoidal left adjoint and the lax monoidal right adjoint
(Adjunction.IsMonoidal) have been stated for these definitions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Adjunction.ε_comp_map_ε
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
:
CategoryStruct.comp (Functor.LaxMonoidal.ε G) (G.map (Functor.LaxMonoidal.ε F)) = adj.unit.app (MonoidalCategoryStruct.tensorUnit C)
theorem
CategoryTheory.Adjunction.ε_comp_map_ε_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
{Z : C}
(h : G.obj (F.obj (MonoidalCategoryStruct.tensorUnit C)) ⟶ Z)
:
CategoryStruct.comp (Functor.LaxMonoidal.ε G) (CategoryStruct.comp (G.map (Functor.LaxMonoidal.ε F)) h) = CategoryStruct.comp (adj.unit.app (MonoidalCategoryStruct.tensorUnit C)) h
theorem
CategoryTheory.Adjunction.map_η_comp_η
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.Monoidal]
[adj.IsMonoidal]
:
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]
:
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalInverseSymmOfFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
:
@[implicit_reducible]
noncomputable def
CategoryTheory.Equivalence.inverseMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
:
If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Equivalence.IsMonoidal
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
:
An equivalence of categories involving monoidal functors is monoidal if the underlying adjunction satisfies certain compatibilities with respect to the monoidal functor data.
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]
:
Equations
- One or more equations did not get rendered due to their size.
@[implicit_reducible]
instance
CategoryTheory.Equivalence.instMonoidalInverseRefl
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
@[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
- One or more equations did not get rendered due to their size.
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_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)))
@[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)
:
@[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