(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.

A monoidal functor is a lax monoidal functor for which ε and μ are isomorphisms.

We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.

See also CategoryTheory.Monoidal.Functorial for a typeclass decorating an object-level function with the additional data of a monoidal functor. This is useful when stating that a pre-existing functor is monoidal.

See CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

We show in CategoryTheory.Monoidal.Mon_ that lax monoidal functors take monoid objects to monoid objects.

Future work #

Oplax monoidal functors.

References #

See .

source

structure CategoryTheory.LaxMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] extends CategoryTheory.Functor :

Type (max (max (max u₁ u₂) v₁) v₂)

A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the appropriate coherences.

obj : C → D
map : {X Y : C} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map_id : ∀ (X : C), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
ε : 𝟙_ D ⟶ self.obj (𝟙_ C)
unit morphism
μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (self.obj X) (self.obj Y) ⟶ self.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
tensorator
μ_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X')) (self.μ Y X') = CategoryTheory.CategoryStruct.comp (self.μ X X') (self.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
μ_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f)) (self.μ X' Y) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z)) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z)) (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
associativity of the tensorator
left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.ε (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.μ (𝟙_ C) X) (self.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.ε) (CategoryTheory.CategoryStruct.comp (self.μ X (𝟙_ C)) (self.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

Instances For

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_left_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (self : CategoryTheory.LaxMonoidalFunctor C D) {X : C} {Y : C} (f : X ⟶ Y) (X' : C) {Z : D} (h : self.obj (CategoryTheory.MonoidalCategory.tensorObj Y X') ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X')) (CategoryTheory.CategoryStruct.comp (self.μ Y X') h) = CategoryTheory.CategoryStruct.comp (self.μ X X') (CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.MonoidalCategory.whiskerRight f X')) h)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (self : CategoryTheory.LaxMonoidalFunctor C D) {X : C} {Y : C} (X' : C) (f : X ⟶ Y) {Z : D} (h : self.obj (CategoryTheory.MonoidalCategory.tensorObj X' Y) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f)) (CategoryTheory.CategoryStruct.comp (self.μ X' Y) h) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f)) h)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.associativity_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (self : CategoryTheory.LaxMonoidalFunctor C D) (X : C) (Y : C) (Z : C) {Z : D} (h : self.obj (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z✝)) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) (CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) h))

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj Y Y') ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (F.μ Y Y') h) = CategoryTheory.CategoryStruct.comp (F.μ X X') (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) h)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.μ_natural {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (F.μ Y Y') = CategoryTheory.CategoryStruct.comp (F.μ X X') (F.map (CategoryTheory.MonoidalCategory.tensorHom f g))

source

@[simp]

∀ {X Y : C} (a : X ⟶ Y), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).map a = F.map a

source

@[simp]

(CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).ε = ε

source

@[simp]

∀ (a : C), (CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).obj a = F.obj a

source

@[simp]

(CategoryTheory.LaxMonoidalFunctor.ofTensorHom F ε μ μ_natural associativity left_unitality right_unitality).μ X Y = μ X Y

source

CategoryTheory.LaxMonoidalFunctor C D

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

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.left_unitality_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.obj X)) (CategoryTheory.CategoryStruct.comp (F.μ (𝟙_ C) X) h)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).inv) h

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.left_unitality_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight F.ε (F.obj X)) (F.μ (𝟙_ C) X)) = F.map (CategoryTheory.MonoidalCategory.leftUnitor X).inv

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.right_unitality_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) F.ε) (CategoryTheory.CategoryStruct.comp (F.μ X (𝟙_ C)) h)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).inv) h

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.right_unitality_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) F.ε) (F.μ X (𝟙_ C))) = F.map (CategoryTheory.MonoidalCategory.rightUnitor X).inv

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.associativity_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) (Y : C) (Z : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.μ Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z✝)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.associator X Y Z✝).inv) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z✝)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.obj Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z✝) h))

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.associativity_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.LaxMonoidalFunctor C D) (X : C) (Y : C) (Z : C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.μ Y Z)) (CategoryTheory.CategoryStruct.comp (F.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.μ X Y) (F.obj Z)) (F.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z))

source

structure CategoryTheory.MonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] extends CategoryTheory.LaxMonoidalFunctor :

Type (max (max (max u₁ u₂) v₁) v₂)

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

See .

obj : C → D
map : {X Y : C} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map_id : ∀ (X : C), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
ε : 𝟙_ D ⟶ self.obj (𝟙_ C)
μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (self.obj X) (self.obj Y) ⟶ self.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
μ_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X')) (self.μ Y X') = CategoryTheory.CategoryStruct.comp (self.μ X X') (self.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
μ_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f)) (self.μ X' Y) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z)) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z)) (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.ε (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.μ (𝟙_ C) X) (self.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.ε) (CategoryTheory.CategoryStruct.comp (self.μ X (𝟙_ C)) (self.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
ε_isIso : CategoryTheory.IsIso self.ε
μ_isIso : ∀ (X Y : C), CategoryTheory.IsIso (self.μ X Y)

Instances For

source

noncomputable def CategoryTheory.MonoidalFunctor.εIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) :

𝟙_ D ≅ F.obj (𝟙_ C)

The unit morphism of a (strong) monoidal functor as an isomorphism.

Equations

CategoryTheory.MonoidalFunctor.εIso F = CategoryTheory.asIso F.ε

Instances For

source

noncomputable def CategoryTheory.MonoidalFunctor.μIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) :

CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ≅ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)

The tensorator of a (strong) monoidal functor as an isomorphism.

Equations

CategoryTheory.MonoidalFunctor.μIso F X Y = CategoryTheory.asIso (F.μ X Y)

Instances For

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) :

(CategoryTheory.LaxMonoidalFunctor.id C).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.id C).obj X) ((CategoryTheory.Functor.id C).obj Y))

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.LaxMonoidalFunctor.id C).toFunctor = CategoryTheory.Functor.id C

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.id_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.LaxMonoidalFunctor.id C).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

source

def CategoryTheory.LaxMonoidalFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

CategoryTheory.LaxMonoidalFunctor C C

The identity lax monoidal functor.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance CategoryTheory.LaxMonoidalFunctor.instInhabitedLaxMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

Inhabited (CategoryTheory.LaxMonoidalFunctor C C)

Equations

CategoryTheory.LaxMonoidalFunctor.instInhabitedLaxMonoidalFunctor C = { default := CategoryTheory.LaxMonoidalFunctor.id C }

source

theorem CategoryTheory.MonoidalFunctor.map_tensor_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj Y Y') ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.tensorHom f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X X')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (F.μ Y Y') h))

source

theorem CategoryTheory.MonoidalFunctor.map_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {X : C} {Y : C} {X' : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

F.map (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X X')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map f) (F.map g)) (F.μ Y Y'))

source

theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) {Y : C} {Z : C} (f : Y ⟶ Z✝) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj X Z✝) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft X f)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.map f)) (CategoryTheory.CategoryStruct.comp (F.μ X Z✝) h))

source

theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) {Y : C} {Z : C} (f : Y ⟶ Z) :

F.map (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (F.map f)) (F.μ X Z))

source

theorem CategoryTheory.MonoidalFunctor.map_whiskerRight_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {X : C} {Y : C} (f : X ⟶ Y) (Z : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj Y Z✝) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f Z✝)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X Z✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj Z✝)) (CategoryTheory.CategoryStruct.comp (F.μ Y Z✝) h))

source

theorem CategoryTheory.MonoidalFunctor.map_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {X : C} {Y : C} (f : X ⟶ Y) (Z : C) :

F.map (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj Z)) (F.μ Y Z))

source

theorem CategoryTheory.MonoidalFunctor.map_leftUnitor_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) {Z : D} (h : F.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ (𝟙_ C) X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv F.ε) (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom h))

source

theorem CategoryTheory.MonoidalFunctor.map_leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) :

F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ (𝟙_ C) X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv F.ε) (F.obj X)) (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom)

source

theorem CategoryTheory.MonoidalFunctor.map_rightUnitor_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) {Z : D} (h : F.obj X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X (𝟙_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.inv F.ε)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom h))

source

theorem CategoryTheory.MonoidalFunctor.map_rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) :

F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.μ X (𝟙_ C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.inv F.ε)) (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom)

source

noncomputable def CategoryTheory.MonoidalFunctor.μNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) :

CategoryTheory.Functor.comp (CategoryTheory.Functor.prod F.toFunctor F.toFunctor) (CategoryTheory.MonoidalCategory.tensor D) ≅ CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensor C) F.toFunctor

The tensorator as a natural isomorphism.

Equations

CategoryTheory.MonoidalFunctor.μNatIso F = CategoryTheory.NatIso.ofComponents (fun (X : C × C) => CategoryTheory.MonoidalFunctor.μIso F X.1 X.2) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.μIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) :

(CategoryTheory.MonoidalFunctor.μIso F X Y).hom = F.μ X Y

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_inv_hom_id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.μIso F X Y).inv (CategoryTheory.CategoryStruct.comp (F.μ X Y) h) = h

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.μIso F X Y).inv (F.μ X Y) = CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.μ_hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (Y : C) :

CategoryTheory.CategoryStruct.comp (F.μ X Y) (CategoryTheory.MonoidalFunctor.μIso F X Y).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.εIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) :

(CategoryTheory.MonoidalFunctor.εIso F).hom = F.ε

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_inv_hom_id_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {Z : D} (h : F.obj (𝟙_ C) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.εIso F).inv (CategoryTheory.CategoryStruct.comp F.ε h) = h

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalFunctor.εIso F).inv F.ε = CategoryTheory.CategoryStruct.id (F.obj (𝟙_ C))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.ε_hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) :

CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.MonoidalFunctor.εIso F).inv = CategoryTheory.CategoryStruct.id (𝟙_ D)

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorLeft_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) :

(CategoryTheory.MonoidalFunctor.commTensorLeft F X✝).inv.app X = (CategoryTheory.MonoidalFunctor.μIso F X✝ X).inv

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorLeft_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) :

(CategoryTheory.MonoidalFunctor.commTensorLeft F X✝).hom.app X = F.μ X✝ X

source

noncomputable def CategoryTheory.MonoidalFunctor.commTensorLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) :

CategoryTheory.Functor.comp F.toFunctor (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X)) ≅ CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorLeft X) F.toFunctor

Monoidal functors commute with left tensoring up to isomorphism

Equations

CategoryTheory.MonoidalFunctor.commTensorLeft F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.MonoidalFunctor.μIso F X Y) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) :

(CategoryTheory.MonoidalFunctor.commTensorRight F X✝).inv.app X = (CategoryTheory.MonoidalFunctor.μIso F X X✝).inv

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.commTensorRight_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) (X : C) :

(CategoryTheory.MonoidalFunctor.commTensorRight F X✝).hom.app X = F.μ X X✝

source

noncomputable def CategoryTheory.MonoidalFunctor.commTensorRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) (X : C) :

CategoryTheory.Functor.comp F.toFunctor (CategoryTheory.MonoidalCategory.tensorRight (F.obj X)) ≅ CategoryTheory.Functor.comp (CategoryTheory.MonoidalCategory.tensorRight X) F.toFunctor

Monoidal functors commute with right tensoring up to isomorphism

Equations

CategoryTheory.MonoidalFunctor.commTensorRight F X = CategoryTheory.NatIso.ofComponents (fun (Y : C) => CategoryTheory.MonoidalFunctor.μIso F Y X) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) :

(CategoryTheory.MonoidalFunctor.id C).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.id C).obj X) ((CategoryTheory.Functor.id C).obj Y))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.MonoidalFunctor.id C).toFunctor = CategoryTheory.Functor.id C

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.id_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.MonoidalFunctor.id C).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

source

def CategoryTheory.MonoidalFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

CategoryTheory.MonoidalFunctor C C

The identity monoidal functor.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance CategoryTheory.MonoidalFunctor.instInhabitedMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

Inhabited (CategoryTheory.MonoidalFunctor C C)

Equations

CategoryTheory.MonoidalFunctor.instInhabitedMonoidalFunctor C = { default := CategoryTheory.MonoidalFunctor.id C }

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.comp_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor D E) :

(F ⊗⋙ G).ε = CategoryTheory.CategoryStruct.comp G.ε (G.map F.ε)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.comp_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor D E) (X : C) (Y : C) :

(F ⊗⋙ G).μ X Y = CategoryTheory.CategoryStruct.comp (G.μ (F.obj X) (F.obj Y)) (G.map (F.μ X Y))

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.comp_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor D E) :

(F ⊗⋙ G).toFunctor = CategoryTheory.Functor.comp F.toFunctor G.toFunctor

source

def CategoryTheory.LaxMonoidalFunctor.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor D E) :

CategoryTheory.LaxMonoidalFunctor C E

The composition of two lax monoidal functors is again lax monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CategoryTheory.LaxMonoidalFunctor.«term_⊗⋙_» :

Lean.TrailingParserDescr

The composition of two lax monoidal functors is again lax monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) (X : B × D) (Y : B × D) :

(CategoryTheory.LaxMonoidalFunctor.prod F G).μ X Y = (F.μ X.1 Y.1, G.μ X.2 Y.2)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) :

(CategoryTheory.LaxMonoidalFunctor.prod F G).toFunctor = CategoryTheory.Functor.prod F.toFunctor G.toFunctor

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) :

(CategoryTheory.LaxMonoidalFunctor.prod F G).ε = (F.ε, G.ε)

source

def CategoryTheory.LaxMonoidalFunctor.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.LaxMonoidalFunctor B C) (G : CategoryTheory.LaxMonoidalFunctor D E) :

CategoryTheory.LaxMonoidalFunctor (B × D) (C × E)

The cartesian product of two lax monoidal functors is lax monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.MonoidalFunctor.diag C).ε = CategoryTheory.CategoryStruct.id (𝟙_ (C × C))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) :

(CategoryTheory.MonoidalFunctor.diag C).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.diag C).obj X) ((CategoryTheory.Functor.diag C).obj Y))

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.diag_toLaxMonoidalFunctor_toFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

(CategoryTheory.MonoidalFunctor.diag C).toFunctor = CategoryTheory.Functor.diag C

source

def CategoryTheory.MonoidalFunctor.diag (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :

CategoryTheory.MonoidalFunctor C (C × C)

The diagonal functor as a monoidal functor.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CategoryTheory.LaxMonoidalFunctor.prod' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C E) :

CategoryTheory.LaxMonoidalFunctor C (D × E)

The cartesian product of two lax monoidal functors starting from the same monoidal category C is lax monoidal.

Equations

CategoryTheory.LaxMonoidalFunctor.prod' F G = (CategoryTheory.MonoidalFunctor.diag C).toLaxMonoidalFunctor ⊗⋙ CategoryTheory.LaxMonoidalFunctor.prod F G

Instances For

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod'_toFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C E) :

(CategoryTheory.LaxMonoidalFunctor.prod' F G).toFunctor = CategoryTheory.Functor.prod' F.toFunctor G.toFunctor

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod'_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C E) :

(CategoryTheory.LaxMonoidalFunctor.prod' F G).ε = (F.ε, G.ε)

source

@[simp]

theorem CategoryTheory.LaxMonoidalFunctor.prod'_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.LaxMonoidalFunctor C D) (G : CategoryTheory.LaxMonoidalFunctor C E) (X : C) (Y : C) :

(CategoryTheory.LaxMonoidalFunctor.prod' F G).μ X Y = (F.μ X Y, G.μ X Y)

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.comp_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor D E) :

(F ⊗⋙ G).toLaxMonoidalFunctor = F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor

source

def CategoryTheory.MonoidalFunctor.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor D E) :

CategoryTheory.MonoidalFunctor C E

The composition of two monoidal functors is again monoidal.

Equations

F ⊗⋙ G = let __src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; { toLaxMonoidalFunctor := __src, ε_isIso := ⋯, μ_isIso := ⋯ }

Instances For

source

def CategoryTheory.MonoidalFunctor.«term_⊗⋙_» :

Lean.TrailingParserDescr

The composition of two monoidal functors is again monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.prod_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.MonoidalFunctor B C) (G : CategoryTheory.MonoidalFunctor D E) :

(CategoryTheory.MonoidalFunctor.prod F G).toLaxMonoidalFunctor = CategoryTheory.LaxMonoidalFunctor.prod F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor

source

def CategoryTheory.MonoidalFunctor.prod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] {B : Type u₀} [CategoryTheory.Category.{v₀, u₀} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.MonoidalFunctor B C) (G : CategoryTheory.MonoidalFunctor D E) :

CategoryTheory.MonoidalFunctor (B × D) (C × E)

The cartesian product of two monoidal functors is monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def CategoryTheory.MonoidalFunctor.prod' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor C E) :

CategoryTheory.MonoidalFunctor C (D × E)

The cartesian product of two monoidal functors starting from the same monoidal category C is monoidal.

Equations

CategoryTheory.MonoidalFunctor.prod' F G = CategoryTheory.MonoidalFunctor.diag C ⊗⋙ CategoryTheory.MonoidalFunctor.prod F G

Instances For

source

@[simp]

theorem CategoryTheory.MonoidalFunctor.prod'_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] (F : CategoryTheory.MonoidalFunctor C D) (G : CategoryTheory.MonoidalFunctor C E) :

(CategoryTheory.MonoidalFunctor.prod' F G).toLaxMonoidalFunctor = CategoryTheory.LaxMonoidalFunctor.prod' F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor

source

noncomputable def CategoryTheory.monoidalAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) {G : CategoryTheory.Functor D C} (h : F.toFunctor ⊣ G) :

CategoryTheory.LaxMonoidalFunctor D C

If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.monoidalInverse_toLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.Functor.IsEquivalence F.toFunctor] :

(CategoryTheory.monoidalInverse F).toLaxMonoidalFunctor = CategoryTheory.monoidalAdjoint F (CategoryTheory.Functor.asEquivalence F.toLaxMonoidalFunctor.1).toAdjunction

source

noncomputable def CategoryTheory.monoidalInverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.Functor.IsEquivalence F.toFunctor] :

CategoryTheory.MonoidalFunctor D C

If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

Equations

One or more equations did not get rendered due to their size.

Instances For

Documentation

Mathlib.CategoryTheory.Monoidal.Functor

(Lax) monoidal functors #

Future work #

References #