# Documentation

Mathlib.CategoryTheory.Bicategory.Functor

# Oplax functors and pseudofunctors #

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.

A pseudofunctor is an oplax functor whose mapId and mapComp are isomorphisms. We provide several constructors for pseudofunctors:

• Pseudofunctor.mk : the default constructor, which requires map₂_whiskerLeft and map₂_whiskerRight instead of naturality of mapComp.
• Pseudofunctor.mkOfOplax : construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms. This constructor uses Iso to describe isomorphisms.
• pseudofunctor.mkOfOplax' : similar to mkOfOplax, but uses IsIso to describe isomorphisms.

The additional constructors are useful when constructing a pseudofunctor where the construction of the oplax functor associated with it is already done. For example, the composition of pseudofunctors can be defined by using the composition of oplax functors as follows:

def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D :=
mkOfOplax ((F : OplaxFunctor B C).comp G)
{ mapIdIso := λ a => (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
mapCompIso := λ f g =>
(G.mapFunctor _ _).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g) }


although the composition of pseudofunctors in this file is defined by using the default constructor because obviously wasn't smart enough in mathlib3 and the porter of this file was too lazy to investigate this issue further in mathlib4. Similarly, the composition is also defined by using mkOfOplax' after giving appropriate instances for IsIso. The former constructor mkOfOplax requires isomorphisms as data type Iso, and so it is useful if you don't want to forget the definitions of the inverses. On the other hand, the latter constructor mkOfOplax' is useful if you want to use propositional type class IsIso.

## Main definitions #

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

## Future work #

There are two types of functors between bicategories, called lax and oplax functors, depending on the directions of mapId and mapComp. We may need both in mathlib in the future, but for now we only define oplax functors.

structure CategoryTheory.PrelaxFunctor (B : Type u₁) [] [(a b : B) → Quiver (a b)] (C : Type u₂) [] [(a b : C) → Quiver (a b)] extends :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
• obj : BC
• map : {X Y : B} → (X Y) → ((s).obj X (s).obj Y)
• map₂ : {a b : B} → {f g : a b} → (f g) → ((s).map f (s).map g)

The action of a prelax functor on 2-morphisms.

A prelax functor between bicategories consists of functions between objects, 1-morphisms, and 2-morphisms. This structure will be extended to define OplaxFunctor.

Instances For
instance CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor {B : Type u₁} [] [(a b : B) → Quiver (a b)] {C : Type u₂} [] [(a b : C) → Quiver (a b)] :
Coe () (B ⥤q C)
@[simp]
theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor_map (B : Type u₁) [] [(a b : B) → Quiver (a b)] :
∀ {X Y : B} (a : X Y), ().map a = (𝟭q B).map a
@[simp]
theorem CategoryTheory.PrelaxFunctor.id_map₂ (B : Type u₁) [] [(a b : B) → Quiver (a b)] :
∀ {a b : B} {f g : a b} (η : f g),
@[simp]
theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor_obj (B : Type u₁) [] [(a b : B) → Quiver (a b)] :
∀ (a : B), ().obj a = (𝟭q B).obj a
def CategoryTheory.PrelaxFunctor.id (B : Type u₁) [] [(a b : B) → Quiver (a b)] :

The identity prelax functor.

Instances For
instance CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctor {B : Type u₁} [] [(a b : B) → Quiver (a b)] :
@[simp]
theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor_map {B : Type u₁} [] [(a b : B) → Quiver (a b)] {C : Type u₂} [] [(a b : C) → Quiver (a b)] {D : Type u₃} [] [(a b : D) → Quiver (a b)] (F : ) (G : ) :
∀ {X Y : B} (a : X Y), ().map a = (F ⋙q G).map a
@[simp]
theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor_obj {B : Type u₁} [] [(a b : B) → Quiver (a b)] {C : Type u₂} [] [(a b : C) → Quiver (a b)] {D : Type u₃} [] [(a b : D) → Quiver (a b)] (F : ) (G : ) :
∀ (a : B), ().obj a = (F ⋙q G).obj a
@[simp]
theorem CategoryTheory.PrelaxFunctor.comp_map₂ {B : Type u₁} [] [(a b : B) → Quiver (a b)] {C : Type u₂} [] [(a b : C) → Quiver (a b)] {D : Type u₃} [] [(a b : D) → Quiver (a b)] (F : ) (G : ) :
∀ {a b : B} {f g : a b} (η : f g),
def CategoryTheory.PrelaxFunctor.comp {B : Type u₁} [] [(a b : B) → Quiver (a b)] {C : Type u₂} [] [(a b : C) → Quiver (a b)] {D : Type u₃} [] [(a b : D) → Quiver (a b)] (F : ) (G : ) :

Composition of prelax functors.

Instances For
structure CategoryTheory.OplaxFunctor (B : Type u₁) (C : Type u₂) extends :
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.

Instances For
@[simp]
theorem CategoryTheory.OplaxFunctor.map₂_associator_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj d} (h : CategoryTheory.CategoryStruct.comp ((self.toPrelaxFunctor).map f) (CategoryTheory.CategoryStruct.comp ((self.toPrelaxFunctor).map g) ((self.toPrelaxFunctor).map h)) Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor ().hom) (CategoryTheory.CategoryStruct.comp () (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((self.toPrelaxFunctor).map f) ()) h)) = CategoryTheory.CategoryStruct.comp () (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight () ((self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((self.toPrelaxFunctor).map f) ((self.toPrelaxFunctor).map g) ((self.toPrelaxFunctor).map h)).hom h))
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {f : a b} {f' : a b} (η : f f') (g : b c) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((self.toPrelaxFunctor).map f') ((self.toPrelaxFunctor).map g) Z) :
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} (f : a b) {g : b c} {g' : b c} (η : g g') {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((self.toPrelaxFunctor).map f) ((self.toPrelaxFunctor).map g') Z) :
theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map f Z) :
theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map f Z) :
theorem CategoryTheory.OplaxFunctor.map₂_comp_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {f : a b} {g : a b} {h : a b} (η : f g) (θ : g h) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map h Z) :
@[simp]
theorem CategoryTheory.OplaxFunctor.mapFunctor_obj {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) (f : a b) :
().obj f = (F.toPrelaxFunctor).map f
@[simp]
theorem CategoryTheory.OplaxFunctor.mapFunctor_map {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) :
∀ {X Y : a b} (η : X Y), ().map η = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor η
def CategoryTheory.OplaxFunctor.mapFunctor {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) :
CategoryTheory.Functor (a b) ((F.toPrelaxFunctor).obj a (F.toPrelaxFunctor).obj b)

Function between 1-morphisms as a functor.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor_toPrefunctor (B : Type u₁) :
().toPrelaxFunctor =
@[simp]
theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor_map₂ (B : Type u₁) :
∀ {a b : B} {f g : a b} (a_1 : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor a_1 =
@[simp]
theorem CategoryTheory.OplaxFunctor.id_mapComp (B : Type u₁) :
∀ {a b c : B} (f : a b) (g : b c),

The identity oplax functor.

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

Composition of oplax functors.

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

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

Instances For
structure CategoryTheory.Pseudofunctor (B : Type u₁) (C : Type u₂) extends :
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A pseudofunctor 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 compositions, and do not need to strictly preserve the identity. Instead, there are specified 2-isomorphisms 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.

Instances For
theorem CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map f Z) :
theorem CategoryTheory.Pseudofunctor.map₂_comp_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {f : a b} {g : a b} {h : a b} (η : f g) (θ : g h) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map h Z) :
theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f g) (h : b c) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj c} (h : (self.toPrelaxFunctor).map () Z) :
theorem CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj b} (h : (self.toPrelaxFunctor).map f Z) :
theorem CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g h) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj c} (h : (self.toPrelaxFunctor).map () Z) :
theorem CategoryTheory.Pseudofunctor.map₂_associator_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) {Z : (self.toPrelaxFunctor).obj a (self.toPrelaxFunctor).obj d} (h : (self.toPrelaxFunctor).map () Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.PrelaxFunctor.map₂ self.toPrelaxFunctor ().hom) h = CategoryTheory.CategoryStruct.comp ().hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight ().hom ((self.toPrelaxFunctor).map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator ((self.toPrelaxFunctor).map f) ((self.toPrelaxFunctor).map g) ((self.toPrelaxFunctor).map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((self.toPrelaxFunctor).map f) ().inv) ())))
def CategoryTheory.Pseudofunctor.toOplax {B : Type u₁} {C : Type u₂} (F : ) :

The oplax functor associated with a pseudofunctor.

Instances For
@[simp]
theorem CategoryTheory.Pseudofunctor.to_oplax_obj {B : Type u₁} {C : Type u₂} (F : ) :
(().toPrelaxFunctor).obj = F.obj
@[simp]
theorem CategoryTheory.Pseudofunctor.to_oplax_mapId {B : Type u₁} {C : Type u₂} (F : ) (a : B) :
@[simp]
theorem CategoryTheory.Pseudofunctor.to_oplax_mapComp {B : Type u₁} {C : Type u₂} (F : ) {a : B} {b : B} {c : B} (f : a b) (g : b c) :
@[simp]
theorem CategoryTheory.Pseudofunctor.mapFunctor_map {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) :
∀ {X Y : a b} (η : X Y), ().map η = CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor η
@[simp]
theorem CategoryTheory.Pseudofunctor.mapFunctor_obj {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) (f : a b) :
().obj f = (().toPrelaxFunctor).map f
def CategoryTheory.Pseudofunctor.mapFunctor {B : Type u₁} {C : Type u₂} (F : ) (a : B) (b : B) :
CategoryTheory.Functor (a b) ((F.toPrelaxFunctor).obj a (F.toPrelaxFunctor).obj b)

Function on 1-morphisms as a functor.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.Pseudofunctor.id_mapComp (B : Type u₁) :
∀ {a b c : B} (f : a b) (g : b c),
@[simp]
theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor_toPrefunctor (B : Type u₁) :
().toPrelaxFunctor =
@[simp]
theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor_map₂ (B : Type u₁) :
∀ {a b : B} {f g : a b} (a_1 : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor a_1 =

The identity pseudofunctor.

Instances For
@[simp]
theorem CategoryTheory.Pseudofunctor.comp_mapComp {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) :
∀ {a b c : B} (f : a b) (g : b c), = (CategoryTheory.Pseudofunctor.mapFunctor G ((F.toPrelaxFunctor).obj a) ((F.toPrelaxFunctor).obj c)).mapIso () ≪≫ CategoryTheory.Pseudofunctor.mapComp G ((F.toPrelaxFunctor).map f) ((F.toPrelaxFunctor).map g)
@[simp]
theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor_toPrefunctor {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) :
().toPrelaxFunctor = ↑(CategoryTheory.PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor)
@[simp]
theorem CategoryTheory.Pseudofunctor.comp_mapId {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) (a : B) :
= (CategoryTheory.Pseudofunctor.mapFunctor G ((F.toPrelaxFunctor).obj a) ((F.toPrelaxFunctor).obj a)).mapIso () ≪≫ CategoryTheory.Pseudofunctor.mapId G ((F.toPrelaxFunctor).obj a)
@[simp]
theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor_map₂ {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) :
∀ {a b : B} {f g : a b} (a_1 : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ (CategoryTheory.PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor) a_1
def CategoryTheory.Pseudofunctor.comp {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) :

Composition of pseudofunctors.

Instances For
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor_toPrefunctor {B : Type u₁} {C : Type u₂} (F : ) :
().toPrelaxFunctor = F.toPrelaxFunctor
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapId {B : Type u₁} {C : Type u₂} (F : ) (a : B) :
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapComp {B : Type u₁} {C : Type u₂} (F : ) :
∀ {a b c : B} (f : a b) (g : b c),
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor_map₂ {B : Type u₁} {C : Type u₂} (F : ) :
∀ {a b : B} {f g : a b} (a_1 : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor a_1
def CategoryTheory.Pseudofunctor.mkOfOplax {B : Type u₁} {C : Type u₂} (F : ) :

Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

Instances For
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor_toPrefunctor {B : Type u₁} {C : Type u₂} (F : ) [∀ (a : B), ] [∀ {a b c : B} (f : a b) (g : b c), ] :
().toPrelaxFunctor = F.toPrelaxFunctor
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId {B : Type u₁} {C : Type u₂} (F : ) [∀ (a : B), ] [∀ {a b c : B} (f : a b) (g : b c), ] (a : B) :
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp {B : Type u₁} {C : Type u₂} (F : ) [∀ (a : B), ] [∀ {a b c : B} (f : a b) (g : b c), ] :
∀ {a b c : B} (f : a b) (g : b c),
@[simp]
theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor_map₂ {B : Type u₁} {C : Type u₂} (F : ) [∀ (a : B), ] [∀ {a b c : B} (f : a b) (g : b c), ] :
∀ {a b : B} {f g : a b} (a_1 : f g), CategoryTheory.PrelaxFunctor.map₂ ().toPrelaxFunctor a_1 = CategoryTheory.PrelaxFunctor.map₂ F.toPrelaxFunctor a_1
noncomputable def CategoryTheory.Pseudofunctor.mkOfOplax' {B : Type u₁} {C : Type u₂} (F : ) [∀ (a : B), ] [∀ {a b c : B} (f : a b) (g : b c), ] :

Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

Instances For