Lax functors #

A lax functor F between bicategories B and C consists of

a function between objects F.obj : B ⟶ C,
a family of functions between 1-morphisms F.map : (a ⟶ b) → (F.obj a ⟶ F.obj b),
a family of functions between 2-morphisms F.map₂ : (f ⟶ g) → (F.map f ⟶ F.map g),
a family of 2-morphisms F.mapId a : 𝟙 (F.obj a) ⟶ F.map (𝟙 a),
a family of 2-morphisms F.mapComp f g : F.map f ≫ F.map g ⟶ F.map (f ≫ g), and
certain consistency conditions on them.

Main definitions #

CategoryTheory.LaxFunctor B C : an lax functor between bicategories B and C
CategoryTheory.LaxFunctor.comp F G : the composition of lax functors
CategoryTheory.LaxFunctor.Pseudocore : a structure on an Lax functor that promotes a Lax functor to a pseudofunctor

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.

source

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.

obj : B → C
map : {X Y : B} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (self.map f ⟶ self.map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
mapId : (a : B) → CategoryTheory.CategoryStruct.id (self.obj a) ⟶ self.map (CategoryTheory.CategoryStruct.id a)
The 2-morphism underlying the lax unity constraint.
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → CategoryTheory.CategoryStruct.comp (self.map f) (self.map g) ⟶ self.map (CategoryTheory.CategoryStruct.comp f g)
The 2-morphism underlying the lax functoriality constraint.
mapComp_naturality_left : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)
Naturality of the lax functoriality constraint, on the left.
mapComp_naturality_right : ∀ {a b c : B} (f : a ⟶ b) {g 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.
map₂_associator : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h)) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)))
Lax associativity.
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (self.mapComp (CategoryTheory.CategoryStruct.id a) f))
Lax left unity.
map₂_rightUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (self.mapComp f (CategoryTheory.CategoryStruct.id b)))
Lax right unity.

Instances For

source

@[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) :

CategoryTheory.CategoryStruct.comp (self.mapComp f g) (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)

Naturality of the lax functoriality constraint, on the left.

source

@[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.

source

@[simp]

theorem CategoryTheory.LaxFunctor.map₂_associator {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h)) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)))

Lax associativity.

source

@[simp]

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) :

self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (self.mapComp (CategoryTheory.CategoryStruct.id a) f))

Lax left unity.

source

@[simp]

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) :

self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (self.mapComp f (CategoryTheory.CategoryStruct.id b)))

Lax right unity.

source

@[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) :

CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (CategoryTheory.CategoryStruct.comp (self.mapComp f g') h)

source

@[simp]

theorem CategoryTheory.LaxFunctor.map₂_associator_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : self.obj a ⟶ self.obj d} (h : self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h✝)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h✝)) (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h✝).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h✝)) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) h))

source

@[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) :

CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) (CategoryTheory.CategoryStruct.comp (self.mapComp f' g) h)

source

@[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)

source

@[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)

source

@[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))

source

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) h))

source

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) h))

source

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))

source

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))

source

theorem CategoryTheory.LaxFunctor.mapComp_assoc_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h : F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h✝) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h✝)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h✝)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h✝)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h✝).inv) h)))

source

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)))

source

theorem CategoryTheory.LaxFunctor.mapComp_assoc_left {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)))

source

theorem CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h : F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h✝)) ⟶ Z) :

source

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)))

source

theorem CategoryTheory.LaxFunctor.mapComp_assoc_right {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)))

source

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h))

source

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} (f : a ⟶ b) (X : ↑(F.obj a)) :

(CategoryTheory.Bicategory.leftUnitor (F.map f)).hom.app X = CategoryTheory.CategoryStruct.comp ((F.map f).map ((F.mapId a).app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).app X) ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).app X))

source

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) :

(CategoryTheory.Bicategory.leftUnitor (F.map f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f) (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom))

source

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h))

source

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a : B} {b : B} (f : a ⟶ b) (X : ↑(F.obj a)) :

(CategoryTheory.Bicategory.rightUnitor (F.map f)).hom.app X = CategoryTheory.CategoryStruct.comp ((F.mapId b).app ((F.map f).obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).app X) ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).app X))

source

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) :

(CategoryTheory.Bicategory.rightUnitor (F.map f)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b)) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)) (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom))

source

@[simp]

theorem CategoryTheory.LaxFunctor.id_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) :

(CategoryTheory.LaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)

source

@[simp]

theorem CategoryTheory.LaxFunctor.id_mapComp (B : Type u₁) [CategoryTheory.Bicategory B] :

∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.LaxFunctor.id B).mapComp f g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

source

@[simp]

theorem CategoryTheory.LaxFunctor.id_toPrelaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] :

(CategoryTheory.LaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B

source

def CategoryTheory.LaxFunctor.id (B : Type u₁) [CategoryTheory.Bicategory B] :

CategoryTheory.LaxFunctor B B

The identity lax functor.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance CategoryTheory.LaxFunctor.instInhabited {B : Type u₁} [CategoryTheory.Bicategory B] :

Inhabited (CategoryTheory.LaxFunctor B B)

Equations

CategoryTheory.LaxFunctor.instInhabited = { default := CategoryTheory.LaxFunctor.id B }

source

@[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

source

@[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))

source

@[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))

source

def CategoryTheory.LaxFunctor.comp {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) :

CategoryTheory.LaxFunctor B D

Composition of lax functors.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)
The isomorphism giving rise to the lax unity constraint
mapCompIso : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)
The isomorphism giving rise to the lax functoriality constraint
mapIdIso_inv : ∀ {a : B}, (self.mapIdIso a).inv = F.mapId a
mapIdIso gives rise to the lax unity constraint
mapCompIso_inv : ∀ {a 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

Instances For

source

@[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

source

@[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

Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Lax

Lax functors #

Main definitions #

Future work #