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.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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (F.μ X Y) (CategoryTheory.CategoryStruct.comp (self.toNatTrans.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.toNatTrans.app X) (self.toNatTrans.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.toPrefunctor.obj (𝟙_ C) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp F.ε (CategoryTheory.CategoryStruct.comp (self.toNatTrans.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).toNatTrans.app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.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.instInhabitedMonoidalNatTrans {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) :
      (CategoryTheory.MonoidalNatTrans.vcomp α β).toNatTrans.app X = CategoryTheory.CategoryStruct.comp (α.toNatTrans.app X) (β.toNatTrans.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
      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
        • CategoryTheory.MonoidalNatTrans.categoryLaxMonoidalFunctor = CategoryTheory.Category.mk
        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), α.toNatTrans.app X = β.toNatTrans.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) :
        (CategoryTheory.MonoidalNatTrans.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
        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) :
          (CategoryTheory.MonoidalNatTrans.prod α β).toNatTrans.app X = (α.toNatTrans.app X, β.toNatTrans.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 (CategoryTheory.LaxMonoidalFunctor.prod' F H) (CategoryTheory.LaxMonoidalFunctor.prod' G K)

          The cartesian product of two monoidal natural transformations is monoidal.

          Equations
          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.toPrefunctor.obj X ≅ G.toPrefunctor.obj X) (naturality' : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.toPrefunctor.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)) :
            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.toPrefunctor.obj X ≅ G.toPrefunctor.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.toPrefunctor.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.toNatTrans.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.toPrefunctor.obj X ≅ G.toPrefunctor.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (app Y).hom = CategoryTheory.CategoryStruct.comp (app X).hom (G.toPrefunctor.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.toNatTrans.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 (α.toNatTrans.app X)] :
              CategoryTheory.IsIso α
              Equations
              source
              @[simp]
              theorem CategoryTheory.monoidalUnit_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) [CategoryTheory.IsEquivalence F.toFunctor] :
              (CategoryTheory.monoidalUnit F).toNatTrans = (CategoryTheory.Functor.asEquivalence F.toFunctor).unit
              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) [CategoryTheory.IsEquivalence F.toFunctor] :
              CategoryTheory.LaxMonoidalFunctor.id C ⟶ F.toLaxMonoidalFunctor ⊗⋙ (CategoryTheory.monoidalInverse F).toLaxMonoidalFunctor

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

              Equations
              Instances For
                source
                instance CategoryTheory.instIsIsoLaxMonoidalFunctorCategoryLaxMonoidalFunctorIdCompToLaxMonoidalFunctorToLaxMonoidalFunctorMonoidalInverseMonoidalUnit {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.IsEquivalence F.toFunctor] :
                CategoryTheory.IsIso (CategoryTheory.monoidalUnit F)
                Equations
                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) [CategoryTheory.IsEquivalence F.toFunctor] :
                (CategoryTheory.monoidalCounit F).toNatTrans = (CategoryTheory.Functor.asEquivalence F.toFunctor).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) [CategoryTheory.IsEquivalence F.toFunctor] :
                (CategoryTheory.monoidalInverse F).toLaxMonoidalFunctor ⊗⋙ F.toLaxMonoidalFunctor ⟶ CategoryTheory.LaxMonoidalFunctor.id D

                The counit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

                Equations
                Instances For
                  source
                  instance CategoryTheory.instIsIsoLaxMonoidalFunctorCategoryLaxMonoidalFunctorCompToLaxMonoidalFunctorMonoidalInverseToLaxMonoidalFunctorIdMonoidalCounit {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.IsEquivalence F.toFunctor] :
                  CategoryTheory.IsIso (CategoryTheory.monoidalCounit F)
                  Equations