Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Lax

Lax functors #

A lax functor F between bicategories B and C consists of

Main definitions #

Future work #

Some constructions in the bicategory library have only been done in terms of oplax functors, since lax functors had not yet been added (e.g FunctorBicategory.lean). A possible project would be to mirror these constructions for lax functors.

structure CategoryTheory.LaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A lax functor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂.

Unlike functors between categories, F.map do not need to strictly commute with the composition, and do not need to strictly preserve the identity. Instead, there are specified 2-morphisms 𝟙 (F.obj a) ⟶ F.map (𝟙 a) and F.map f ≫ F.map g ⟶ F.map (f ≫ g).

F.map₂ strictly commute with compositions and preserve the identity. They also preserve the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

Instances For
    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_left {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {f : a b} {f' : a b} (η : f f') (g : b c) :

    Naturality of the lax functoriality constraint, on the left.

    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_right {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} (f : a b) {g : b c} {g' : b c} (η : g g') :
    CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f g')

    Naturality of the lax functoriality constraint, on the right.

    @[simp]

    Lax associativity.

    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} (f : a b) {g : b c} {g' : b c} (η : g g') {Z : self.obj a self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp f g') Z) :
    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {f : a b} {f' : a b} (η : f f') (g : b c) {Z : self.obj a self.obj c} (h : self.map (CategoryTheory.CategoryStruct.comp f' g) Z) :
    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_left_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {f : a b} {f' : a b} (η : f f') (g : b c) (X : (self.obj a)) :
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).app X) ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).app X) = CategoryTheory.CategoryStruct.comp ((self.map g).map ((self.map₂ η).app X)) ((self.mapComp f' g).app X)
    @[simp]
    theorem CategoryTheory.LaxFunctor.mapComp_naturality_right_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} (f : a b) {g : b c} {g' : b c} (η : g g') (X : (self.obj a)) :
    CategoryTheory.CategoryStruct.comp ((self.mapComp f g).app X) ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).app X) = CategoryTheory.CategoryStruct.comp ((self.map₂ η).app ((self.map f).obj X)) ((self.mapComp f g').app X)
    @[simp]
    theorem CategoryTheory.LaxFunctor.map₂_associator_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) (X : (self.obj a)) :
    CategoryTheory.CategoryStruct.comp ((self.map h).map ((self.mapComp f g).app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).app X) ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).app ((self.map f).obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).app X))
    theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} (f : a b) (X : (self.obj a)) :
    (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.rightUnitor (self.map f)).inv.app X) (CategoryTheory.CategoryStruct.comp ((self.mapId b).app ((self.map f).obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).app X))
    theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} (f : a b) (X : (self.obj a)) :
    (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.leftUnitor (self.map f)).inv.app X) (CategoryTheory.CategoryStruct.comp ((self.map f).map ((self.mapId a).app X)) ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).app X))
    theorem CategoryTheory.LaxFunctor.mapComp_assoc_left_app {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) (X : (F.obj a)) :
    CategoryTheory.CategoryStruct.comp ((F.map h).map ((F.mapComp f g).app X)) ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).app ((F.map f).obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).app X)))
    theorem CategoryTheory.LaxFunctor.mapComp_assoc_right_app {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) (X : (F.obj a)) :
    CategoryTheory.CategoryStruct.comp ((F.mapComp g h).app ((F.map f).obj X)) ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.map h).map ((F.mapComp f g).app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).app X)))

    The identity lax functor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      @[simp]
      theorem CategoryTheory.LaxFunctor.comp_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D) :
      (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
      @[simp]
      theorem CategoryTheory.LaxFunctor.comp_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D) (a : B) :
      (F.comp G).mapId a = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)) (G.map₂ (F.mapId a))
      @[simp]
      theorem CategoryTheory.LaxFunctor.comp_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D) :
      ∀ {a b c : B} (f : a b) (g : b c), (F.comp G).mapComp f g = CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)) (G.map₂ (F.mapComp f g))

      Composition of lax functors.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        structure CategoryTheory.LaxFunctor.PseudoCore {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) :
        Type (max (max u₁ v₁) w₂)

        A structure on an Lax functor that promotes an Lax functor to a pseudofunctor.

        See Pseudofunctor.mkOfLax.

        Instances For
          @[simp]
          theorem CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.LaxFunctor B C} (self : F.PseudoCore) {a : B} :
          (self.mapIdIso a).inv = F.mapId a

          mapIdIso gives rise to the lax unity constraint

          @[simp]
          theorem CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.LaxFunctor B C} (self : F.PseudoCore) {a : B} {b : B} {c : B} (f : a b) (g : b c) :
          (self.mapCompIso f g).inv = F.mapComp f g

          mapCompIso gives rise to the lax functoriality constraint