Oplax functors

An oplax 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.map (𝟙 a) ⟶ 𝟙 (F.obj a),
• a family of 2-morphisms F.mapComp f g : F.map (f ≫ g) ⟶ F.map f ≫ F.map g, and
• certain consistency conditions on them.

Main definitions

• CategoryTheory.OplaxFunctor B C : an oplax functor between bicategories B and C
• CategoryTheory.OplaxFunctor.comp F G : the composition of oplax functors

structure CategoryTheory.OplaxFunctor (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₂)

An oplax 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.map (𝟙 a) ⟶ 𝟙 (F.obj a) and F.map (f ≫ g) ⟶ F.map f ≫ F.map 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) → self.map (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.id (self.obj a)
• mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → self.map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
• mapComp_naturality_left : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
• mapComp_naturality_right : ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (self.mapComp f g') = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
• map₂_associator : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom)
• map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
• map₂_rightUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)

@[simp]

theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))

@[simp]

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

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_associator {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom)

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)

@[simp]

theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (self.map f') (self.map g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (CategoryTheory.CategoryStruct.comp (self.mapComp f' g) h) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g)) h)

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_associator_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp (self.map g) (self.map h✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h✝).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h✝)) h)) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h✝)).hom h))

@[simp]

theorem CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (self.map f) (self.map g') ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (CategoryTheory.CategoryStruct.comp (self.mapComp f g') h) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) h)

theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom h))

theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom h))

theorem CategoryTheory.OplaxFunctor.mapComp_assoc_right_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (F.map h✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h✝)) h) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h✝).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h✝)).hom h)))

theorem CategoryTheory.OplaxFunctor.mapComp_assoc_right {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))

theorem CategoryTheory.OplaxFunctor.mapComp_assoc_left_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)) (F.map h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h✝)) h) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h✝).hom) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h✝)).inv h)))

theorem CategoryTheory.OplaxFunctor.mapComp_assoc_left {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h)) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h)) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))

@[simp]

theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] : (CategoryTheory.OplaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B

@[simp]

theorem CategoryTheory.OplaxFunctor.id_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) : (CategoryTheory.OplaxFunctor.id B).mapId a = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)

@[simp]

theorem CategoryTheory.OplaxFunctor.id_mapComp (B : Type u₁) [CategoryTheory.Bicategory B] : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.OplaxFunctor.id B).mapComp f g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

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

The identity oplax functor.

Equations

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

instance CategoryTheory.OplaxFunctor.instInhabited {B : Type u₁} [CategoryTheory.Bicategory B] : Inhabited (CategoryTheory.OplaxFunctor B B)

Equations

• CategoryTheory.OplaxFunctor.instInhabited = { default := CategoryTheory.OplaxFunctor.id B }

def CategoryTheory.OplaxFunctor.comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor C D) : CategoryTheory.OplaxFunctor B D

Composition of oplax functors.

Equations

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

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

A structure on an oplax functor that promotes an oplax functor to a pseudofunctor. See Pseudofunctor.mkOfOplax.

• mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)
• 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)
• mapIdIso_hom : ∀ {a : B}, (self.mapIdIso a).hom = F.mapId a
• mapCompIso_hom : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (self.mapCompIso f g).hom = F.mapComp f g

@[simp]

theorem CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} (self : F.PseudoCore) {a : B} : (self.mapIdIso a).hom = F.mapId a

@[simp]

theorem CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} (self : F.PseudoCore) {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : (self.mapCompIso f g).hom = F.mapComp f g