mathlib documentation

category_theory.bicategory.functor

Oplax functors and pseudofunctors #

An oplax functor F between bicategories B and C consists of

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

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 pseudofunctor.comp (F : pseudofunctor B C) (G : pseudofunctor C D) : pseudofunctor B D :=
mk_of_oplax ((F : oplax_functor B C).comp G)
{ map_id_iso := λ a, (G.map_functor _ _).map_iso (F.map_id a) ≪≫ G.map_id (F.obj a),
  map_comp_iso := λ a b c f g,
    (G.map_functor _ _).map_iso (F.map_comp f g) ≪≫ G.map_comp (F.map f) (F.map g) }

although the composition of pseudofunctors in this file is defined by using the default constructor because obviously is smart enough. Similarly, the composition is also defined by using mk_of_oplax' after giving appropriate instances for is_iso. The former constructor mk_of_oplax 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 mk_of_oplax' is useful if you want to use propositional type class is_iso.

Main definitions #

Future work #

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

structure category_theory.prelax_functor (B : Type u₁) [quiver B] [Π (a b : B), quiver (a b)] (C : Type u₂) [quiver C] [Π (a b : C), quiver (a b)] :
Type (max u₁ u₂ v₁ v₂ w₁ w₂)
  • 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)

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

Instances for category_theory.prelax_functor
def category_theory.prelax_functor.to_prefunctor {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] (self : category_theory.prelax_functor B C) :

The prefunctor between the underlying quivers.

@[protected, instance]
def category_theory.prelax_functor.has_coe_to_prefunctor {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] :
Equations
@[simp]
theorem category_theory.prelax_functor.to_prefunctor_eq_coe {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] (F : category_theory.prelax_functor B C) :
@[simp]
theorem category_theory.prelax_functor.to_prefunctor_obj {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] (F : category_theory.prelax_functor B C) :
@[simp]
theorem category_theory.prelax_functor.to_prefunctor_map {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] (F : category_theory.prelax_functor B C) :
@[simp]
theorem category_theory.prelax_functor.id_obj (B : Type u₁) [quiver B] [Π (a b : B), quiver (a b)] (ᾰ : B) :
def category_theory.prelax_functor.id (B : Type u₁) [quiver B] [Π (a b : B), quiver (a b)] :

The identity prelax functor.

Equations
@[simp]
theorem category_theory.prelax_functor.id_map₂ (B : Type u₁) [quiver B] [Π (a b : B), quiver (a b)] (a b : B) (f g : a b) (η : f g) :
@[simp]
theorem category_theory.prelax_functor.id_map (B : Type u₁) [quiver B] [Π (a b : B), quiver (a b)] {X Y : B} (ᾰ : X Y) :
@[protected, instance]
Equations
@[simp]
theorem category_theory.prelax_functor.comp_map₂ {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] {D : Type u₃} [quiver D] [Π (a b : D), quiver (a b)] (F : category_theory.prelax_functor B C) (G : category_theory.prelax_functor C D) (a b : B) (f g : a b) (η : f g) :
(F.comp G).map₂ η = G.map₂ (F.map₂ η)
def category_theory.prelax_functor.comp {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] {D : Type u₃} [quiver D] [Π (a b : D), quiver (a b)] (F : category_theory.prelax_functor B C) (G : category_theory.prelax_functor C D) :

Composition of prelax functors.

Equations
@[simp]
theorem category_theory.prelax_functor.comp_obj {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] {D : Type u₃} [quiver D] [Π (a b : D), quiver (a b)] (F : category_theory.prelax_functor B C) (G : category_theory.prelax_functor C D) (ᾰ : B) :
(F.comp G).obj = (F.comp G).obj
@[simp]
theorem category_theory.prelax_functor.comp_map {B : Type u₁} [quiver B] [Π (a b : B), quiver (a b)] {C : Type u₂} [quiver C] [Π (a b : C), quiver (a b)] {D : Type u₃} [quiver D] [Π (a b : D), quiver (a b)] (F : category_theory.prelax_functor B C) (G : category_theory.prelax_functor C D) {X Y : B} (ᾰ : X Y) :
(F.comp G).map = (F.comp G).map
@[simp]
def category_theory.oplax_functor.map₂_associator_aux {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (obj : B → C) (map : Π {X Y : B}, (X Y)(obj X obj Y)) (map₂ : Π {a b : B} {f g : a b}, (f g)(map f map g)) (map_comp : Π {a b c : B} (f : a b) (g : b c), map (f g) map f map g) {a b c d : B} (f : a b) (g : b c) (h : c d) :
Prop

This auxiliary definition states that oplax functors preserve the associators modulo some adjustments of domains and codomains of 2-morphisms.

Equations

The prelax functor between the underlying quivers.

structure category_theory.oplax_functor (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] :
Type (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 category_theory.oplax_functor
@[simp]
theorem category_theory.oplax_functor.map_comp_naturality_left {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c : B} {f f' : a b} (η : f f') (g : b c) :
@[simp]
theorem category_theory.oplax_functor.map_comp_naturality_right {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c : B} (f : a b) {g g' : b c} (η : g g') :
@[simp]
theorem category_theory.oplax_functor.map₂_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b : B} (f : a b) :
self.map₂ (𝟙 f) = 𝟙 (self.map f)
@[simp]
theorem category_theory.oplax_functor.map₂_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b : B} {f g h : a b} (η : f g) (θ : g h) :
self.map₂ θ) = self.map₂ η self.map₂ θ
@[simp]
theorem category_theory.oplax_functor.map₂_associator {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c d : B} (f : a b) (g : b c) (h : c d) :
@[simp]
theorem category_theory.oplax_functor.map_comp_naturality_left_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c : B} {f f' : a b} (η : f f') (g : b c) {X' : self.obj a self.obj c} (f'_1 : self.map f' self.map g X') :
theorem category_theory.oplax_functor.map₂_comp_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b : B} {f g h : a b} (η : f g) (θ : g h) {X' : self.obj a self.obj b} (f' : self.map h X') :
self.map₂ θ) f' = self.map₂ η self.map₂ θ f'
@[simp]
theorem category_theory.oplax_functor.map_comp_naturality_right_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c : B} (f : a b) {g g' : b c} (η : g g') {X' : self.obj a self.obj c} (f' : self.map f self.map g' X') :
@[simp]
theorem category_theory.oplax_functor.map₂_associator_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) {a b c d : B} (f : a b) (g : b c) (h : c d) {X' : self.obj a self.obj d} (f' : self.map f self.map g self.map h X') :
@[simp]
theorem category_theory.oplax_functor.map_functor_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (a b : B) (f g : a b) (η : f g) :
(F.map_functor a b).map η = F.map₂ η
@[simp]
theorem category_theory.oplax_functor.map_functor_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (a b : B) (f : a b) :
(F.map_functor a b).obj f = F.map f
def category_theory.oplax_functor.map_functor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (a b : B) :
(a b) (F.obj a F.obj b)

Function between 1-morphisms as a functor.

Equations
@[simp]
theorem category_theory.oplax_functor.id_map_comp (B : Type u₁) [category_theory.bicategory B] (a b c : B) (f : a b) (g : b c) :
@[simp]
theorem category_theory.oplax_functor.comp_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.oplax_functor B C) (G : category_theory.oplax_functor C D) (ᾰ : B) :
(F.comp G).obj = (F.comp G).obj
@[simp]

Composition of oplax functors.

Equations
@[simp]
theorem category_theory.oplax_functor.comp_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.oplax_functor B C) (G : category_theory.oplax_functor C D) {a b : B} {f g : a b} (ᾰ : f g) :
(F.comp G).map₂ = (F.comp G).map₂
@[simp]
theorem category_theory.oplax_functor.comp_map_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.oplax_functor B C) (G : category_theory.oplax_functor C D) (a b c : B) (f : a b) (g : b c) :
(F.comp G).map_comp f g = (G.map_functor (F.obj a) (F.obj c)).map (F.map_comp f g) G.map_comp (F.map f) (F.map g)
@[simp]
theorem category_theory.oplax_functor.comp_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.oplax_functor B C) (G : category_theory.oplax_functor C D) {X Y : B} (ᾰ : X Y) :
(F.comp G).map = (F.comp G).map
@[nolint]
structure category_theory.oplax_functor.pseudo_core {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :
Type (max u₁ v₁ w₂)

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

Instances for category_theory.oplax_functor.pseudo_core
  • category_theory.oplax_functor.pseudo_core.has_sizeof_inst
@[simp]
theorem category_theory.oplax_functor.pseudo_core.map_comp_iso_hom {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F : category_theory.oplax_functor B C} (self : F.pseudo_core) {a b c : B} (f : a b) (g : b c) :
(self.map_comp_iso f g).hom = F.map_comp f g
@[simp]
def category_theory.pseudofunctor.map₂_associator_aux {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (obj : B → C) (map : Π {X Y : B}, (X Y)(obj X obj Y)) (map₂ : Π {a b : B} {f g : a b}, (f g)(map f map g)) (map_comp : Π {a b c : B} (f : a b) (g : b c), map (f g) map f map g) {a b c d : B} (f : a b) (g : b c) (h : c d) :
Prop

This auxiliary definition states that pseudofunctors preserve the associators modulo some adjustments of domains and codomains of 2-morphisms.

Equations
structure category_theory.pseudofunctor (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] :
Type (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 category_theory.pseudofunctor

The prelax functor between the underlying quivers.

@[simp]
theorem category_theory.pseudofunctor.map₂_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b : B} (f : a b) :
self.map₂ (𝟙 f) = 𝟙 (self.map f)
@[simp]
theorem category_theory.pseudofunctor.map₂_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b : B} {f g h : a b} (η : f g) (θ : g h) :
self.map₂ θ) = self.map₂ η self.map₂ θ
@[simp]
theorem category_theory.pseudofunctor.map₂_whisker_left {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c : B} (f : a b) {g h : b c} (η : g h) :
@[simp]
theorem category_theory.pseudofunctor.map₂_whisker_right {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c : B} {f g : a b} (η : f g) (h : b c) :
@[simp]
theorem category_theory.pseudofunctor.map₂_associator {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c d : B} (f : a b) (g : b c) (h : c d) :
theorem category_theory.pseudofunctor.map₂_whisker_right_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c : B} {f g : a b} (η : f g) (h : b c) {X' : self.obj a self.obj c} (f' : self.map (g h) X') :
theorem category_theory.pseudofunctor.map₂_comp_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b : B} {f g h : a b} (η : f g) (θ : g h) {X' : self.obj a self.obj b} (f' : self.map h X') :
self.map₂ θ) f' = self.map₂ η self.map₂ θ f'
theorem category_theory.pseudofunctor.map₂_associator_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c d : B} (f : a b) (g : b c) (h : c d) {X' : self.obj a self.obj d} (f' : self.map (f g h) X') :
theorem category_theory.pseudofunctor.map₂_whisker_left_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) {a b c : B} (f : a b) {g h : b c} (η : g h) {X' : self.obj a self.obj c} (f' : self.map (f h) X') :

The oplax functor associated with a pseudofunctor.

Equations
@[simp]
theorem category_theory.pseudofunctor.to_oplax_map_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) {a b c : B} (f : a b) (g : b c) :
F.map_comp f g = (F.map_comp f g).hom
@[simp]
theorem category_theory.pseudofunctor.map_functor_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) (a b : B) (f g : a b) (η : f g) :
(F.map_functor a b).map η = F.map₂ η
@[simp]
theorem category_theory.pseudofunctor.map_functor_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) (a b : B) (f : a b) :
(F.map_functor a b).obj f = F.map f
def category_theory.pseudofunctor.map_functor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) (a b : B) :
(a b) (F.obj a F.obj b)

Function on 1-morphisms as a functor.

Equations
@[simp]
theorem category_theory.pseudofunctor.comp_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.pseudofunctor B C) (G : category_theory.pseudofunctor C D) {X Y : B} (ᾰ : X Y) :
(F.comp G).map = (F.comp G).map
@[simp]
theorem category_theory.pseudofunctor.comp_map_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.pseudofunctor B C) (G : category_theory.pseudofunctor C D) (a b c : B) (f : a b) (g : b c) :
(F.comp G).map_comp f g = (G.map_functor (F.obj a) (F.obj c)).map_iso (F.map_comp f g) ≪≫ G.map_comp (F.map f) (F.map g)

Composition of pseudofunctors.

Equations
@[simp]
theorem category_theory.pseudofunctor.comp_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.pseudofunctor B C) (G : category_theory.pseudofunctor C D) {a b : B} {f g : a b} (ᾰ : f g) :
(F.comp G).map₂ = (F.comp G).map₂
@[simp]
theorem category_theory.pseudofunctor.comp_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {D : Type u₃} [category_theory.bicategory D] (F : category_theory.pseudofunctor B C) (G : category_theory.pseudofunctor C D) (ᾰ : B) :
(F.comp G).obj = (F.comp G).obj
@[simp]

Construct a pseudofunctor from an oplax functor whose map_id and map_comp are isomorphisms.

Equations
@[simp]
theorem category_theory.pseudofunctor.mk_of_oplax_map_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (F' : F.pseudo_core) (_x _x_1 _x_2 : B) (f : _x _x_1) (g : _x_1 _x_2) :
@[simp]
theorem category_theory.pseudofunctor.mk_of_oplax'_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) [∀ (a : B), category_theory.is_iso (F.map_id a)] [∀ {a b c : B} (f : a b) (g : b c), category_theory.is_iso (F.map_comp f g)] {a b : B} {f g : a b} (ᾰ : f g) :
@[simp]
theorem category_theory.pseudofunctor.mk_of_oplax'_map_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) [∀ (a : B), category_theory.is_iso (F.map_id a)] [∀ {a b c : B} (f : a b) (g : b c), category_theory.is_iso (F.map_comp f g)] (a b c : B) (f : a b) (g : b c) :
@[simp]
theorem category_theory.pseudofunctor.mk_of_oplax'_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) [∀ (a : B), category_theory.is_iso (F.map_id a)] [∀ {a b c : B} (f : a b) (g : b c), category_theory.is_iso (F.map_comp f g)] {X Y : B} (ᾰ : X Y) :
@[simp]
theorem category_theory.pseudofunctor.mk_of_oplax'_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) [∀ (a : B), category_theory.is_iso (F.map_id a)] [∀ {a b c : B} (f : a b) (g : b c), category_theory.is_iso (F.map_comp f g)] (ᾰ : B) :
noncomputable def category_theory.pseudofunctor.mk_of_oplax' {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) [∀ (a : B), category_theory.is_iso (F.map_id a)] [∀ {a b c : B} (f : a b) (g : b c), category_theory.is_iso (F.map_comp f g)] :

Construct a pseudofunctor from an oplax functor whose map_id and map_comp are isomorphisms.

Equations