Documentation

Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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.

(Lax) monoidal functors between a fixed pair of monoidal categories themselves form a category.

source
theorem CategoryTheory.MonoidalNatTrans.ext {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F G : CategoryTheory.LaxMonoidalFunctor C D} (x y : CategoryTheory.MonoidalNatTrans F G), x.app = y.app → x = y
source
theorem CategoryTheory.MonoidalNatTrans.ext_iff {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂} {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D} {F G : CategoryTheory.LaxMonoidalFunctor C D} (x y : CategoryTheory.MonoidalNatTrans F G), x = y ↔ x.app = y.app
source
structure CategoryTheory.MonoidalNatTrans {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) (G : CategoryTheory.LaxMonoidalFunctor C D) extends CategoryTheory.NatTrans :
Type (max u₁ v₂)

A monoidal natural transformation is a natural transformation between (lax) monoidal functors additionally satisfying: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y

Instances For
    source
    @[simp]
    theorem CategoryTheory.MonoidalNatTrans.unit {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} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) :
    CategoryTheory.CategoryStruct.comp F.ε (self.app (𝟙_ C)) = G.ε

    The unit condition for a monoidal natural transformation.

    source
    @[simp]
    theorem CategoryTheory.MonoidalNatTrans.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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X : C) (Y : C) :
    CategoryTheory.CategoryStruct.comp (F.μ X Y) (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y)) (G.μ X Y)

    The tensor condition for a monoidal natural transformation.

    source
    @[simp]
    theorem CategoryTheory.MonoidalNatTrans.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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) (X : C) (Y : C) {Z : D} (h : G.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (F.μ X Y) (CategoryTheory.CategoryStruct.comp (self.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (self.app Y)) (CategoryTheory.CategoryStruct.comp (G.μ X Y) h)
    source
    @[simp]
    theorem CategoryTheory.MonoidalNatTrans.unit_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} {G : CategoryTheory.LaxMonoidalFunctor C D} (self : CategoryTheory.MonoidalNatTrans F G) {Z : D} (h : G.obj (𝟙_ C) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.CategoryStruct.comp (self.app (𝟙_ C)) h) = CategoryTheory.CategoryStruct.comp G.ε h
    source
    @[simp]
    theorem CategoryTheory.MonoidalNatTrans.id_toNatTrans_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.LaxMonoidalFunctor C D) (X : C) :
    (CategoryTheory.MonoidalNatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
    source
    def CategoryTheory.MonoidalNatTrans.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.LaxMonoidalFunctor C D) :
    CategoryTheory.MonoidalNatTrans F F

    The identity monoidal natural transformation.

    Equations
    Instances For
      source
      instance CategoryTheory.MonoidalNatTrans.instInhabited {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) :
      Inhabited (CategoryTheory.MonoidalNatTrans F F)
      Equations
      source
      @[simp]
      theorem CategoryTheory.MonoidalNatTrans.vcomp_toNatTrans_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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans G H) (X : C) :
      (α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
      source
      def CategoryTheory.MonoidalNatTrans.vcomp {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} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans G H) :
      CategoryTheory.MonoidalNatTrans F H

      Vertical composition of monoidal natural transformations.

      Equations
      • α.vcomp β = let __src := α.vcomp β.toNatTrans; { toNatTrans := __src, unit := ⋯, tensor := ⋯ }
      Instances For
        source
        instance CategoryTheory.MonoidalNatTrans.categoryLaxMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
        CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.LaxMonoidalFunctor C D)
        Equations
        source
        @[simp]
        theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans_lax {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} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor C D} {α : F ⟶ G} {β : G ⟶ H} :
        (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
        source
        instance CategoryTheory.MonoidalNatTrans.categoryMonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
        CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.MonoidalFunctor C D)
        Equations
        source
        theorem CategoryTheory.MonoidalNatTrans.ext' {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} {G : CategoryTheory.LaxMonoidalFunctor C D} {α : F ⟶ G} {β : F ⟶ G} (w : ∀ (X : C), α.app X = β.app X) :
        α = β
        source
        @[simp]
        theorem CategoryTheory.MonoidalNatTrans.comp_toNatTrans {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.MonoidalFunctor C D} {H : CategoryTheory.MonoidalFunctor C D} {α : F ⟶ G} {β : G ⟶ H} :
        (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
        source
        @[simp]
        theorem CategoryTheory.MonoidalNatTrans.hcomp_toNatTrans {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 D} {H : CategoryTheory.LaxMonoidalFunctor D E} {K : CategoryTheory.LaxMonoidalFunctor D E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) :
        (α.hcomp β).toNatTrans = α.toNatTrans ◫ β.toNatTrans
        source
        def CategoryTheory.MonoidalNatTrans.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 : CategoryTheory.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} {H : CategoryTheory.LaxMonoidalFunctor D E} {K : CategoryTheory.LaxMonoidalFunctor D E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) :
        CategoryTheory.MonoidalNatTrans (F ⊗⋙ H) (G ⊗⋙ K)

        Horizontal composition of monoidal natural transformations.

        Equations
        • α.hcomp β = let __src := α.toNatTrans ◫ β.toNatTrans; { toNatTrans := __src, unit := ⋯, tensor := ⋯ }
        Instances For
          source
          @[simp]
          theorem CategoryTheory.MonoidalNatTrans.prod_toNatTrans_app {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 D} {H : CategoryTheory.LaxMonoidalFunctor C E} {K : CategoryTheory.LaxMonoidalFunctor C E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) (X : C) :
          (α.prod β).app X = (α.app X, β.app X)
          source
          def CategoryTheory.MonoidalNatTrans.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 D} {H : CategoryTheory.LaxMonoidalFunctor C E} {K : CategoryTheory.LaxMonoidalFunctor C E} (α : CategoryTheory.MonoidalNatTrans F G) (β : CategoryTheory.MonoidalNatTrans H K) :
          CategoryTheory.MonoidalNatTrans (F.prod' H) (G.prod' K)

          The cartesian product of two monoidal natural transformations is monoidal.

          Equations
          • α.prod β = { app := fun (X : C) => (α.app X, β.app X), naturality := ⋯, unit := ⋯, tensor := ⋯ }
          Instances For
            source
            def CategoryTheory.MonoidalNatIso.ofComponents {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} {G : CategoryTheory.LaxMonoidalFunctor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality' : autoParam (∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) _auto✝) (unit' : autoParam (CategoryTheory.CategoryStruct.comp F.ε (app (𝟙_ C)).hom = G.ε) _auto✝) (tensor' : autoParam (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G.μ X Y)) _auto✝) :
            F ≅ G

            Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.MonoidalNatIso.ofComponents.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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) (unit : CategoryTheory.CategoryStruct.comp F.ε (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G.μ X Y)) (X : C) :
              (CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).hom.app X = (app X).hom
              source
              @[simp]
              theorem CategoryTheory.MonoidalNatIso.ofComponents.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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (app : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.map f)) (unit : CategoryTheory.CategoryStruct.comp F.ε (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom) (G.μ X Y)) (X : C) :
              (CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).inv.app X = (app X).inv
              source
              instance CategoryTheory.MonoidalNatIso.isIso_of_isIso_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.LaxMonoidalFunctor C D} {G : CategoryTheory.LaxMonoidalFunctor C D} (α : F ⟶ G) [∀ (X : C), CategoryTheory.IsIso (α.app X)] :
              CategoryTheory.IsIso α
              Equations
              • ⋯ = ⋯
              source
              def CategoryTheory.monoidalUnit {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.id C ⟶ F.toLaxMonoidalFunctor ⊗⋙ CategoryTheory.monoidalAdjoint F h

              The unit of a adjunction can be upgraded to a monoidal natural transformation.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.monoidalCounit_toNatTrans {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.monoidalCounit F h).toNatTrans = h.counit
                source
                def CategoryTheory.monoidalCounit {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.monoidalAdjoint F h ⊗⋙ F.toLaxMonoidalFunctor ⟶ CategoryTheory.LaxMonoidalFunctor.id D

                The unit of a adjunction can be upgraded to a monoidal natural transformation.

                Equations
                Instances For
                  source
                  instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalUnitOfIsEquivalence {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) [F.IsEquivalence] :
                  CategoryTheory.IsIso (CategoryTheory.monoidalUnit F h)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.instIsIsoLaxMonoidalFunctorMonoidalCounitOfIsEquivalence {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) [F.IsEquivalence] :
                  CategoryTheory.IsIso (CategoryTheory.monoidalCounit F h)
                  Equations
                  • ⋯ = ⋯