Monoidal natural transformations #
Natural transformations between (lax) monoidal functors must satisfy
an additional compatibility relation with the tensorators:
F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y.
class
CategoryTheory.NatTrans.IsMonoidal
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F₁ F₂ : CategoryTheory.Functor C D}
(τ : F₁ ⟶ F₂)
[F₁.LaxMonoidal]
[F₂.LaxMonoidal]
:
A natural transformation between (lax) monoidal functors is monoidal if it satisfies
ε F ≫ τ.app (𝟙_ C) = ε G and μ F X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ μ G X Y.
- unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₁) (τ.app (𝟙_ C)) = CategoryTheory.Functor.LaxMonoidal.ε F₂
- tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y) (τ.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (τ.app X) (τ.app Y)) (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y)
Instances
@[simp]
theorem
CategoryTheory.NatTrans.IsMonoidal.tensor_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{D : Type u₂}
{inst✝² : CategoryTheory.Category.{v₂, u₂} D}
{inst✝³ : CategoryTheory.MonoidalCategory D}
{F₁ F₂ : CategoryTheory.Functor C D}
{τ : F₁ ⟶ F₂}
{inst✝⁴ : F₁.LaxMonoidal}
{inst✝⁵ : F₂.LaxMonoidal}
[self : CategoryTheory.NatTrans.IsMonoidal τ]
(X Y : C)
{Z : D}
(h : F₂.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y)
(CategoryTheory.CategoryStruct.comp (τ.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (τ.app X) (τ.app Y))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y) h)
@[simp]
theorem
CategoryTheory.NatTrans.IsMonoidal.unit_assoc
{C : Type u₁}
{inst✝ : CategoryTheory.Category.{v₁, u₁} C}
{inst✝¹ : CategoryTheory.MonoidalCategory C}
{D : Type u₂}
{inst✝² : CategoryTheory.Category.{v₂, u₂} D}
{inst✝³ : CategoryTheory.MonoidalCategory D}
{F₁ F₂ : CategoryTheory.Functor C D}
{τ : F₁ ⟶ F₂}
{inst✝⁴ : F₁.LaxMonoidal}
{inst✝⁵ : F₂.LaxMonoidal}
[self : CategoryTheory.NatTrans.IsMonoidal τ]
{Z : D}
(h : F₂.obj (𝟙_ C) ⟶ Z)
:
instance
CategoryTheory.NatTrans.IsMonoidal.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.Functor C D}
[F₁.LaxMonoidal]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.IsMonoidal.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F₁ F₂ F₃ : CategoryTheory.Functor C D}
(τ : F₁ ⟶ F₂)
[F₁.LaxMonoidal]
[F₂.LaxMonoidal]
[F₃.LaxMonoidal]
(τ' : F₂ ⟶ F₃)
[CategoryTheory.NatTrans.IsMonoidal τ]
[CategoryTheory.NatTrans.IsMonoidal τ']
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.IsMonoidal.hcomp
{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₁ F₂ : CategoryTheory.Functor C D}
(τ : F₁ ⟶ F₂)
[F₁.LaxMonoidal]
[F₂.LaxMonoidal]
{G₁ G₂ : CategoryTheory.Functor D E}
[G₁.LaxMonoidal]
[G₂.LaxMonoidal]
(τ' : G₁ ⟶ G₂)
[CategoryTheory.NatTrans.IsMonoidal τ]
[CategoryTheory.NatTrans.IsMonoidal τ']
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
[F.LaxMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal F.leftUnitor.hom
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorRightUnitor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
[F.LaxMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal F.rightUnitor.hom
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorAssociator
{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]
{E' : Type u₄}
[CategoryTheory.Category.{v₄, u₄} E']
[CategoryTheory.MonoidalCategory E']
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
(H : CategoryTheory.Functor E E')
[F.LaxMonoidal]
[G.LaxMonoidal]
[H.LaxMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal (F.associator G H).hom
Equations
- ⋯ = ⋯
instance
CategoryTheory.NatTrans.instIsMonoidalProdProd'
{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 G : CategoryTheory.Functor C D}
{H K : CategoryTheory.Functor C E}
(α : F ⟶ G)
(β : H ⟶ K)
[F.LaxMonoidal]
[G.LaxMonoidal]
[CategoryTheory.NatTrans.IsMonoidal α]
[H.LaxMonoidal]
[K.LaxMonoidal]
[CategoryTheory.NatTrans.IsMonoidal β]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Iso.instIsMonoidalInvFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F₁ F₂ : CategoryTheory.Functor C D}
[F₁.LaxMonoidal]
[F₂.LaxMonoidal]
(e : F₁ ≅ F₂)
[CategoryTheory.NatTrans.IsMonoidal e.hom]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal adj.unit
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.Monoidal]
[G.LaxMonoidal]
[adj.IsMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal adj.counit
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(e : C ≌ D)
[e.functor.Monoidal]
[e.inverse.Monoidal]
[e.IsMonoidal]
:
CategoryTheory.NatTrans.IsMonoidal e.counit
Equations
- ⋯ = ⋯
structure
CategoryTheory.LaxMonoidalFunctor.Hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F G : CategoryTheory.LaxMonoidalFunctor C D)
:
Type (max u₁ v₂)
The type of monoidal natural transformations between (bundled) lax monoidal functors.
- hom : F.toFunctor ⟶ G.toFunctor
the natural transformation between the underlying functors
- isMonoidal : CategoryTheory.NatTrans.IsMonoidal self.hom
Instances For
instance
CategoryTheory.LaxMonoidalFunctor.instCategory
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
:
Equations
- CategoryTheory.LaxMonoidalFunctor.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.id_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.LaxMonoidalFunctor C D)
:
(CategoryTheory.CategoryStruct.id F).hom = CategoryTheory.CategoryStruct.id F.toFunctor
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.comp_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G H : CategoryTheory.LaxMonoidalFunctor C D}
(α : F ⟶ G)
(β : G ⟶ H)
:
(CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
theorem
CategoryTheory.LaxMonoidalFunctor.comp_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G H : CategoryTheory.LaxMonoidalFunctor C D}
(α : F ⟶ G)
(β : G ⟶ H)
{Z : CategoryTheory.Functor C D}
(h : H.toFunctor ⟶ Z)
:
theorem
CategoryTheory.LaxMonoidalFunctor.hom_ext
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
{α β : F ⟶ G}
(h : α.hom = β.hom)
:
α = β
def
CategoryTheory.LaxMonoidalFunctor.homMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(f : F.toFunctor ⟶ G.toFunctor)
[CategoryTheory.NatTrans.IsMonoidal f]
:
F ⟶ G
Constructor for morphisms in the category LaxMonoidalFunctor C D.
Equations
- CategoryTheory.LaxMonoidalFunctor.homMk f = { hom := f, isMonoidal := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.homMk_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(f : F.toFunctor ⟶ G.toFunctor)
[CategoryTheory.NatTrans.IsMonoidal f]
:
(CategoryTheory.LaxMonoidalFunctor.homMk f).hom = f
def
CategoryTheory.LaxMonoidalFunctor.isoMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(e : F.toFunctor ≅ G.toFunctor)
[CategoryTheory.NatTrans.IsMonoidal e.hom]
:
F ≅ G
Constructor for isomorphisms in the category LaxMonoidalFunctor C D.
Equations
- CategoryTheory.LaxMonoidalFunctor.isoMk e = { hom := CategoryTheory.LaxMonoidalFunctor.homMk e.hom, inv := CategoryTheory.LaxMonoidalFunctor.homMk e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.isoMk_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(e : F.toFunctor ≅ G.toFunctor)
[CategoryTheory.NatTrans.IsMonoidal e.hom]
:
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.isoMk_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(e : F.toFunctor ≅ G.toFunctor)
[CategoryTheory.NatTrans.IsMonoidal e.hom]
:
def
CategoryTheory.LaxMonoidalFunctor.isoOfComponents
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F G : CategoryTheory.LaxMonoidalFunctor C D}
(e : (X : C) → F.obj X ≅ G.obj X)
(naturality :
∀ {X Y : C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by
aesop_cat)
(unit :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by
aesop_cat)
(tensor :
∀ (X Y : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
(e (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (e X).hom (e Y).hom)
(CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by
aesop_cat)
:
F ≅ G
Constructor for isomorphisms between lax monoidal functors.
Equations
- CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor = CategoryTheory.LaxMonoidalFunctor.isoMk (CategoryTheory.NatIso.ofComponents e ⋯)
Instances For
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.isoOfComponents_inv_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 G : CategoryTheory.LaxMonoidalFunctor C D}
(e : (X : C) → F.obj X ≅ G.obj X)
(naturality :
∀ {X Y : C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by
aesop_cat)
(unit :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by
aesop_cat)
(tensor :
∀ (X Y : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
(e (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (e X).hom (e Y).hom)
(CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by
aesop_cat)
(X : C)
:
(CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor).inv.hom.app X = (e X).inv
@[simp]
theorem
CategoryTheory.LaxMonoidalFunctor.isoOfComponents_hom_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 G : CategoryTheory.LaxMonoidalFunctor C D}
(e : (X : C) → F.obj X ≅ G.obj X)
(naturality :
∀ {X Y : C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by
aesop_cat)
(unit :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by
aesop_cat)
(tensor :
∀ (X Y : C),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y)
(e (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (e X).hom (e Y).hom)
(CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by
aesop_cat)
(X : C)
:
(CategoryTheory.LaxMonoidalFunctor.isoOfComponents e naturality unit tensor).hom.hom.app X = (e X).hom