Documentation

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Oplax natural transformations #

Just as there are natural transformations between functors, there are oplax natural transformations between oplax functors. The equality in the naturality of natural transformations is replaced by a specified 2-morphism F.map f ≫ app b ⟶ app a ≫ G.map f in the case of oplax natural transformations.

Main definitions #

structure CategoryTheory.OplaxNatTrans {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₂)

If η is an oplax natural transformation between F and G, we have a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. We also have a 2-morphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b. These 2-morphisms satisfies 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.OplaxNatTrans.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.OplaxNatTrans 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) = CategoryTheory.CategoryStruct.comp (self.naturality f) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))

    The identity oplax natural transformation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.OplaxNatTrans.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.OplaxNatTrans 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.OplaxNatTrans.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.OplaxNatTrans 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)) 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) 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) (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.OplaxNatTrans.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.OplaxNatTrans 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)) 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) 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) (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 oplax natural transformations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.OplaxNatTrans.Modification.ext {B : Type u₁} :
        ∀ {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C} {F G : CategoryTheory.OplaxFunctor B C} {η θ : F G} {x y : CategoryTheory.OplaxNatTrans.Modification η θ}, x.app = y.appx = y
        theorem CategoryTheory.OplaxNatTrans.Modification.ext_iff {B : Type u₁} :
        ∀ {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C} {F G : CategoryTheory.OplaxFunctor B C} {η θ : F G} {x y : CategoryTheory.OplaxNatTrans.Modification η θ}, x = y x.app = y.app

        A modification Γ between oplax natural transformations η and θ consists of a family of 2-morphisms Γ.app a : η.app a ⟶ θ.app a, which satisfies the equation (F.map f ◁ app b) ≫ θ.naturality f = η.naturality f ≫ (app a ▷ G.map f) for each 1-morphism f : a ⟶ b.

        Instances For

          The identity modification.

          Equations
          Instances For

            Vertical composition of modifications.

            Equations
            Instances For
              theorem CategoryTheory.OplaxNatTrans.ext_iff {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F G} {β : F G} {m : α β} {n : α β} :
              m = n ∀ (b : B), m.app b = n.app b
              theorem CategoryTheory.OplaxNatTrans.ext {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F G} {β : F G} {m : α β} {n : α β} (w : ∀ (b : B), m.app b = n.app b) :
              m = n
              @[simp]
              theorem CategoryTheory.OplaxNatTrans.Modification.comp_app' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {X : B} {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F G} {β : F G} {γ : F G} (m : α β) (n : β γ) :
              @[simp]
              theorem CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F G} {θ : F G} (app : (a : B) → η.app a θ.app a) (naturality : ∀ {a b : B} (f : a b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))) (a : B) :
              (CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).hom.app a = (app a).hom
              @[simp]
              theorem CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F G} {θ : F G} (app : (a : B) → η.app a θ.app a) (naturality : ∀ {a b : B} (f : a b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))) (a : B) :
              (CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).inv.app a = (app a).inv
              def CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F G} {θ : F G} (app : (a : B) → η.app a θ.app a) (naturality : ∀ {a b : B} (f : a b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))) :
              η θ

              Construct a modification isomorphism between oplax natural transformations by giving object level isomorphisms, and checking naturality only in the forward direction.

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

                A structure on an Oplax natural transformation that promotes it to a strong natural transformation.

                See StrongNatTrans.mkOfOplax.

                Instances For
                  @[simp]
                  theorem CategoryTheory.OplaxNatTrans.StrongCore.naturality_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : CategoryTheory.OplaxNatTrans F G} (self : η.StrongCore) {a : B} {b : B} (f : a b) :
                  (self.naturality f).hom = η.naturality f