Documentation

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong

Strong natural transformations #

A strong natural transformation is an oplax natural transformation such that each component 2-cell is an isomorphism.

Main definitions #

TODO #

After having defined lax functors, we should define 3 different types of strong natural transformations:

References #

structure CategoryTheory.StrongOplaxNatTrans {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) :
Type (max (max (max u₁ v₁) v₂) w₂)

A strong natural transformation between oplax functors F and G is a natural transformation that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:

  • a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B.
  • a 2-isomorphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
  • These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.
Instances For
    @[simp]
    theorem CategoryTheory.StrongOplaxNatTrans.naturality_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.StrongOplaxNatTrans F G) {a : B} {b : B} {f : a b} {g : a b} (η : f g) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g).hom = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
    @[simp]
    theorem CategoryTheory.StrongOplaxNatTrans.toOplax_naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.StrongOplaxNatTrans F G) :
    ∀ {a b : B} (f : a b), η.toOplax.naturality f = (η.naturality f).hom

    The underlying oplax natural transformation of a strong natural transformation.

    Equations
    • η.toOplax = { app := η.app, naturality := fun {a b : B} (f : a b) => (η.naturality f).hom, naturality_naturality := , naturality_id := , naturality_comp := }
    Instances For

      Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.

      Equations
      Instances For

        Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The identity strong natural transformation.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {G : CategoryTheory.OplaxFunctor B C} {H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.StrongOplaxNatTrans G H) {a : B} {b : B} {c : B} {a' : C} (f : a' G.obj a) (g : a b) (h : b c) {Z : a' H.obj c} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.comp (H.map g) (H.map h✝))) Z) :
            @[simp]
            theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.StrongOplaxNatTrans F G) {a : B} {b : B} {c : B} {a' : C} (f : a b) (g : b c) (h : G.obj c a') {Z : F.obj a a'} (h : CategoryTheory.CategoryStruct.comp (η.app a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h✝) Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h✝)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c)) h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g)) h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h✝).hom h))))))))
            @[simp]
            theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.StrongOplaxNatTrans F G) {a : B} {b : B} {c : B} {a' : C} (f : a b) (g : b c) (h : G.obj c a') :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))

            Vertical composition of strong natural transformations.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For