mathlib3 documentation

category_theory.bicategory.functor

Oplax functors and pseudofunctors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.map_id a : F.map (𝟙 a) ⟶ 𝟙 (F.obj a),
a family of 2-morphisms F.map_comp 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 map_id and map_comp are isomorphisms. We provide several constructors for pseudofunctors:

pseudofunctor.mk : the default constructor, which requires map₂_whisker_left and map₂_whisker_right instead of naturality of map_comp.
pseudofunctor.mk_of_oplax : construct a pseudofunctor from an oplax functor whose map_id and map_comp are isomorphisms. This constructor uses iso to describe isomorphisms.
pseudofunctor.mk_of_oplax' : similar to mk_of_oplax, but uses is_iso 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 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 #

category_theory.oplax_functor B C : an oplax functor between bicategories B and C
category_theory.oplax_functor.comp F G : the composition of oplax functors
category_theory.pseudofunctor B C : a pseudofunctor between bicategories B and C
category_theory.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 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

category_theory.prelax_functor.has_sizeof_inst
category_theory.prelax_functor.has_coe_to_prefunctor
category_theory.prelax_functor.inhabited
category_theory.oplax_functor.has_coe_to_prelax
category_theory.pseudofunctor.has_coe_to_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) :

B ⥤q 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)] :

has_coe (category_theory.prelax_functor B C) (B ⥤q C)

Equations

category_theory.prelax_functor.has_coe_to_prefunctor = {coe := category_theory.prelax_functor.to_prefunctor (λ (a b : C), _inst_4 a b)}

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

F.to_prefunctor = ↑F

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

↑F.obj = F.obj

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

↑F.map = F.map

@[simp]

theorem category_theory.prelax_functor.id_obj (B : Type u₁) [quiver B] [Π (a b : B), quiver (a ⟶ b)] (ᾰ : B) :

(category_theory.prelax_functor.id B).obj ᾰ = (𝟭q B).obj ᾰ

def category_theory.prelax_functor.id (B : Type u₁) [quiver B] [Π (a b : B), quiver (a ⟶ b)] :

category_theory.prelax_functor B B

The identity prelax functor.

Equations

category_theory.prelax_functor.id B = {obj := (𝟭q B).obj, map := (𝟭q B).map, map₂ := λ (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)] (a b : B) (f g : a ⟶ b) (η : f ⟶ g) :

(category_theory.prelax_functor.id B).map₂ η = η

@[simp]

theorem category_theory.prelax_functor.id_map (B : Type u₁) [quiver B] [Π (a b : B), quiver (a ⟶ b)] {X Y : B} (ᾰ : X ⟶ Y) :

(category_theory.prelax_functor.id B).map ᾰ = (𝟭q B).map ᾰ

@[protected, instance]

def category_theory.prelax_functor.inhabited {B : Type u₁} [quiver B] [Π (a b : B), quiver (a ⟶ b)] :

inhabited (category_theory.prelax_functor B B)

Equations

category_theory.prelax_functor.inhabited = {default := category_theory.prelax_functor.id B (λ (a b : B), _inst_2 a b)}

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

category_theory.prelax_functor B D

Composition of prelax functors.

Equations

F.comp G = {obj := (↑F ⋙q ↑G).obj, map := (↑F ⋙q ↑G).map, map₂ := λ (a b : B) (f g : a ⟶ b) (η : f ⟶ g), G.map₂ (F.map₂ η)}

@[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 ⋙q ↑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 ⋙q ↑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

category_theory.oplax_functor.map₂_associator_aux obj map map₂ map_comp f g h = (map₂ (category_theory.bicategory.associator f g h).hom ≫ map_comp f (g ≫ h) ≫ category_theory.bicategory.whisker_left (map f) (map_comp g h) = map_comp (f ≫ g) h ≫ category_theory.bicategory.whisker_right (map_comp f g) (map h) ≫ (category_theory.bicategory.associator (map f) (map g) (map h)).hom)

def category_theory.oplax_functor.to_prelax_functor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.oplax_functor B C) :

category_theory.prelax_functor B C

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

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), self.map (𝟙 a) ⟶ 𝟙 (self.obj a)
map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), self.map (f ≫ g) ⟶ self.map f ≫ self.map g
map_comp_naturality_left' : (∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), self.map₂ (category_theory.bicategory.whisker_right η g) ≫ self.map_comp f' g = self.map_comp f g ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map g)) . "obviously"
map_comp_naturality_right' : (∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), self.map₂ (category_theory.bicategory.whisker_left f η) ≫ self.map_comp f g' = self.map_comp f g ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η)) . "obviously"
map₂_id' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (𝟙 f) = 𝟙 (self.map f)) . "obviously"
map₂_comp' : (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (η ≫ θ) = self.map₂ η ≫ self.map₂ θ) . "obviously"
map₂_associator' : (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), category_theory.oplax_functor.map₂_associator_aux self.obj (λ (_x _x_1 : B), self.map) (λ (a b : B) (f g : a ⟶ b), self.map₂) (λ (a b c : B), self.map_comp) f g h) . "obviously"
map₂_left_unitor' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (category_theory.bicategory.left_unitor f).hom = self.map_comp (𝟙 a) f ≫ category_theory.bicategory.whisker_right (self.map_id a) (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom) . "obviously"
map₂_right_unitor' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (category_theory.bicategory.right_unitor f).hom = self.map_comp f (𝟙 b) ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b) ≫ (category_theory.bicategory.right_unitor (self.map f)).hom) . "obviously"

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

category_theory.oplax_functor.has_sizeof_inst
category_theory.oplax_functor.has_coe_to_prelax
category_theory.oplax_functor.inhabited
category_theory.pseudofunctor.has_coe_to_oplax
category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct
category_theory.oplax_functor.bicategory

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

self.map₂ (category_theory.bicategory.whisker_right η g) ≫ self.map_comp f' g = self.map_comp f g ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map g)

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

self.map₂ (category_theory.bicategory.whisker_left f η) ≫ self.map_comp f g' = self.map_comp f g ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η)

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

self.map₂ (category_theory.bicategory.associator f g h).hom ≫ self.map_comp f (g ≫ h) ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_comp g h) = self.map_comp (f ≫ g) h ≫ category_theory.bicategory.whisker_right (self.map_comp f g) (self.map h) ≫ (category_theory.bicategory.associator (self.map f) (self.map g) (self.map h)).hom

@[simp]

theorem category_theory.oplax_functor.map₂_left_unitor {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₂ (category_theory.bicategory.left_unitor f).hom = self.map_comp (𝟙 a) f ≫ category_theory.bicategory.whisker_right (self.map_id a) (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom

@[simp]

theorem category_theory.oplax_functor.map₂_right_unitor {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₂ (category_theory.bicategory.right_unitor f).hom = self.map_comp f (𝟙 b) ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b) ≫ (category_theory.bicategory.right_unitor (self.map f)).hom

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

self.map₂ (category_theory.bicategory.whisker_right η g) ≫ self.map_comp f' g ≫ f'_1 = self.map_comp f g ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map g) ≫ f'_1

theorem category_theory.oplax_functor.map₂_right_unitor_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 : a ⟶ b) {X' : self.obj a ⟶ self.obj b} (f' : self.map f ⟶ X') :

self.map₂ (category_theory.bicategory.right_unitor f).hom ≫ f' = self.map_comp f (𝟙 b) ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b) ≫ (category_theory.bicategory.right_unitor (self.map f)).hom ≫ f'

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'

theorem category_theory.oplax_functor.map₂_left_unitor_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 : a ⟶ b) {X' : self.obj a ⟶ self.obj b} (f' : self.map f ⟶ X') :

self.map₂ (category_theory.bicategory.left_unitor f).hom ≫ f' = self.map_comp (𝟙 a) f ≫ category_theory.bicategory.whisker_right (self.map_id a) (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom ≫ 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') :

self.map₂ (category_theory.bicategory.whisker_left f η) ≫ self.map_comp f g' ≫ f' = self.map_comp f g ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η) ≫ f'

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

self.map₂ (category_theory.bicategory.associator f g h).hom ≫ self.map_comp f (g ≫ h) ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_comp g h) ≫ f' = self.map_comp (f ≫ g) h ≫ category_theory.bicategory.whisker_right (self.map_comp f g) (self.map h) ≫ (category_theory.bicategory.associator (self.map f) (self.map g) (self.map h)).hom ≫ f'

@[protected, instance]

def category_theory.oplax_functor.has_coe_to_prelax {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] :

has_coe (category_theory.oplax_functor B C) (category_theory.prelax_functor B C)

Equations

category_theory.oplax_functor.has_coe_to_prelax = {coe := category_theory.oplax_functor.to_prelax_functor _inst_2}

@[simp]

theorem category_theory.oplax_functor.to_prelax_eq_coe {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :

F.to_prelax_functor = ↑F

@[simp]

theorem category_theory.oplax_functor.to_prelax_functor_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :

↑F.obj = F.obj

@[simp]

theorem category_theory.oplax_functor.to_prelax_functor_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :

↑F.map = F.map

@[simp]

theorem category_theory.oplax_functor.to_prelax_functor_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :

↑F.map₂ = F.map₂

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

F.map_functor a b = {obj := λ (f : a ⟶ b), F.map f, map := λ (f g : a ⟶ b) (η : f ⟶ g), F.map₂ η, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.oplax_functor.id_map_id (B : Type u₁) [category_theory.bicategory B] (a : B) :

(category_theory.oplax_functor.id B).map_id a = 𝟙 (𝟙 a)

@[simp]

theorem category_theory.oplax_functor.id_map (B : Type u₁) [category_theory.bicategory B] {X Y : B} (ᾰ : X ⟶ Y) :

(category_theory.oplax_functor.id B).map ᾰ = (category_theory.prelax_functor.id B).map ᾰ

@[simp]

theorem category_theory.oplax_functor.id_obj (B : Type u₁) [category_theory.bicategory B] (ᾰ : B) :

(category_theory.oplax_functor.id B).obj ᾰ = (category_theory.prelax_functor.id B).obj ᾰ

def category_theory.oplax_functor.id (B : Type u₁) [category_theory.bicategory B] :

category_theory.oplax_functor B B

The identity oplax functor.

Equations

category_theory.oplax_functor.id B = {obj := (category_theory.prelax_functor.id B).obj, map := (category_theory.prelax_functor.id B).map, map₂ := (category_theory.prelax_functor.id B).map₂, map_id := λ (a : B), 𝟙 (𝟙 a), map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), 𝟙 (f ≫ g), map_comp_naturality_left' := _, map_comp_naturality_right' := _, map₂_id' := _, map₂_comp' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

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

(category_theory.oplax_functor.id B).map_comp f g = 𝟙 (f ≫ g)

@[simp]

theorem category_theory.oplax_functor.id_map₂ (B : Type u₁) [category_theory.bicategory B] {a b : B} {f g : a ⟶ b} (ᾰ : f ⟶ g) :

(category_theory.oplax_functor.id B).map₂ ᾰ = (category_theory.prelax_functor.id B).map₂ ᾰ

@[protected, instance]

def category_theory.oplax_functor.inhabited {B : Type u₁} [category_theory.bicategory B] :

inhabited (category_theory.oplax_functor B B)

Equations

category_theory.oplax_functor.inhabited = {default := category_theory.oplax_functor.id B _inst_1}

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

theorem category_theory.oplax_functor.comp_map_id {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) :

(F.comp G).map_id a = (G.map_functor (↑↑F.obj a) (↑↑F.obj a)).map (F.map_id a) ≫ G.map_id (F.obj a)

def category_theory.oplax_functor.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) :

category_theory.oplax_functor B D

Composition of oplax functors.

Equations

F.comp G = {obj := (↑F.comp ↑G).obj, map := (↑F.comp ↑G).map, map₂ := (↑F.comp ↑G).map₂, map_id := λ (a : B), (G.map_functor (↑↑F.obj a) (↑↑F.obj a)).map (F.map_id a) ≫ G.map_id (F.obj a), map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), (G.map_functor (↑↑F.obj a) (↑↑F.obj c)).map (F.map_comp f g) ≫ G.map_comp (F.map f) (F.map g), map_comp_naturality_left' := _, map_comp_naturality_right' := _, map₂_id' := _, map₂_comp' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

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

map_id_iso : Π (a : B), F.map (𝟙 a) ≅ 𝟙 (F.obj a)
map_comp_iso : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), F.map (f ≫ g) ≅ F.map f ≫ F.map g
map_id_iso_hom' : (∀ {a : B}, (self.map_id_iso a).hom = F.map_id a) . "obviously"
map_comp_iso_hom' : (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (self.map_comp_iso f g).hom = F.map_comp f g) . "obviously"

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_id_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} :

(self.map_id_iso a).hom = F.map_id a

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

category_theory.pseudofunctor.map₂_associator_aux obj map map₂ map_comp f g h = (map₂ (category_theory.bicategory.associator f g h).hom = (map_comp (f ≫ g) h).hom ≫ category_theory.bicategory.whisker_right (map_comp f g).hom (map h) ≫ (category_theory.bicategory.associator (map f) (map g) (map h)).hom ≫ category_theory.bicategory.whisker_left (map f) (map_comp g h).inv ≫ (map_comp f (g ≫ h)).inv)

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

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), self.map (𝟙 a) ≅ 𝟙 (self.obj a)
map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), self.map (f ≫ g) ≅ self.map f ≫ self.map g
map₂_id' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (𝟙 f) = 𝟙 (self.map f)) . "obviously"
map₂_comp' : (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (η ≫ θ) = self.map₂ η ≫ self.map₂ θ) . "obviously"
map₂_whisker_left' : (∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h), self.map₂ (category_theory.bicategory.whisker_left f η) = (self.map_comp f g).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η) ≫ (self.map_comp f h).inv) . "obviously"
map₂_whisker_right' : (∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c), self.map₂ (category_theory.bicategory.whisker_right η h) = (self.map_comp f h).hom ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map h) ≫ (self.map_comp g h).inv) . "obviously"
map₂_associator' : (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), category_theory.pseudofunctor.map₂_associator_aux self.obj (λ (a b : B), self.map) (λ (a b : B) (f g : a ⟶ b), self.map₂) (λ (a b c : B), self.map_comp) f g h) . "obviously"
map₂_left_unitor' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (category_theory.bicategory.left_unitor f).hom = (self.map_comp (𝟙 a) f).hom ≫ category_theory.bicategory.whisker_right (self.map_id a).hom (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom) . "obviously"
map₂_right_unitor' : (∀ {a b : B} (f : a ⟶ b), self.map₂ (category_theory.bicategory.right_unitor f).hom = (self.map_comp f (𝟙 b)).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b).hom ≫ (category_theory.bicategory.right_unitor (self.map f)).hom) . "obviously"

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

category_theory.pseudofunctor.has_sizeof_inst
category_theory.pseudofunctor.has_coe_to_prelax_functor
category_theory.pseudofunctor.has_coe_to_oplax
category_theory.pseudofunctor.inhabited

def category_theory.pseudofunctor.to_prelax_functor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (self : category_theory.pseudofunctor B C) :

category_theory.prelax_functor B C

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

self.map₂ (category_theory.bicategory.whisker_left f η) = (self.map_comp f g).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η) ≫ (self.map_comp f h).inv

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

self.map₂ (category_theory.bicategory.whisker_right η h) = (self.map_comp f h).hom ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map h) ≫ (self.map_comp g h).inv

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

self.map₂ (category_theory.bicategory.associator f g h).hom = (self.map_comp (f ≫ g) h).hom ≫ category_theory.bicategory.whisker_right (self.map_comp f g).hom (self.map h) ≫ (category_theory.bicategory.associator (self.map f) (self.map g) (self.map h)).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_comp g h).inv ≫ (self.map_comp f (g ≫ h)).inv

@[simp]

theorem category_theory.pseudofunctor.map₂_left_unitor {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₂ (category_theory.bicategory.left_unitor f).hom = (self.map_comp (𝟙 a) f).hom ≫ category_theory.bicategory.whisker_right (self.map_id a).hom (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom

@[simp]

theorem category_theory.pseudofunctor.map₂_right_unitor {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₂ (category_theory.bicategory.right_unitor f).hom = (self.map_comp f (𝟙 b)).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b).hom ≫ (category_theory.bicategory.right_unitor (self.map f)).hom

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

self.map₂ (category_theory.bicategory.whisker_right η h) ≫ f' = (self.map_comp f h).hom ≫ category_theory.bicategory.whisker_right (self.map₂ η) (self.map h) ≫ (self.map_comp g h).inv ≫ f'

theorem category_theory.pseudofunctor.map₂_left_unitor_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 : a ⟶ b) {X' : self.obj a ⟶ self.obj b} (f' : self.map f ⟶ X') :

self.map₂ (category_theory.bicategory.left_unitor f).hom ≫ f' = (self.map_comp (𝟙 a) f).hom ≫ category_theory.bicategory.whisker_right (self.map_id a).hom (self.map f) ≫ (category_theory.bicategory.left_unitor (self.map f)).hom ≫ f'

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

self.map₂ (category_theory.bicategory.associator f g h).hom ≫ f' = (self.map_comp (f ≫ g) h).hom ≫ category_theory.bicategory.whisker_right (self.map_comp f g).hom (self.map h) ≫ (category_theory.bicategory.associator (self.map f) (self.map g) (self.map h)).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_comp g h).inv ≫ (self.map_comp f (g ≫ h)).inv ≫ f'

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

self.map₂ (category_theory.bicategory.whisker_left f η) ≫ f' = (self.map_comp f g).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map₂ η) ≫ (self.map_comp f h).inv ≫ f'

theorem category_theory.pseudofunctor.map₂_right_unitor_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 : a ⟶ b) {X' : self.obj a ⟶ self.obj b} (f' : self.map f ⟶ X') :

self.map₂ (category_theory.bicategory.right_unitor f).hom ≫ f' = (self.map_comp f (𝟙 b)).hom ≫ category_theory.bicategory.whisker_left (self.map f) (self.map_id b).hom ≫ (category_theory.bicategory.right_unitor (self.map f)).hom ≫ f'

@[protected, instance]

def category_theory.pseudofunctor.has_coe_to_prelax_functor {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] :

has_coe (category_theory.pseudofunctor B C) (category_theory.prelax_functor B C)

Equations

category_theory.pseudofunctor.has_coe_to_prelax_functor = {coe := category_theory.pseudofunctor.to_prelax_functor _inst_2}

@[simp]

theorem category_theory.pseudofunctor.to_prelax_functor_eq_coe {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

F.to_prelax_functor = ↑F

@[simp]

theorem category_theory.pseudofunctor.to_prelax_functor_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.obj = F.obj

@[simp]

theorem category_theory.pseudofunctor.to_prelax_functor_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.map = F.map

@[simp]

theorem category_theory.pseudofunctor.to_prelax_functor_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.map₂ = F.map₂

def category_theory.pseudofunctor.to_oplax {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

category_theory.oplax_functor B C

The oplax functor associated with a pseudofunctor.

Equations

F.to_oplax = {obj := ↑F.obj, map := ↑F.map, map₂ := ↑F.map₂, map_id := λ (a : B), (F.map_id a).hom, map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), (F.map_comp f g).hom, map_comp_naturality_left' := _, map_comp_naturality_right' := _, map₂_id' := _, map₂_comp' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

@[protected, instance]

def category_theory.pseudofunctor.has_coe_to_oplax {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] :

has_coe (category_theory.pseudofunctor B C) (category_theory.oplax_functor B C)

Equations

category_theory.pseudofunctor.has_coe_to_oplax = {coe := category_theory.pseudofunctor.to_oplax _inst_2}

@[simp]

theorem category_theory.pseudofunctor.to_oplax_eq_coe {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

F.to_oplax = ↑F

@[simp]

theorem category_theory.pseudofunctor.to_oplax_obj {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.obj = F.obj

@[simp]

theorem category_theory.pseudofunctor.to_oplax_map {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.map = F.map

@[simp]

theorem category_theory.pseudofunctor.to_oplax_map₂ {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) :

↑F.map₂ = F.map₂

@[simp]

theorem category_theory.pseudofunctor.to_oplax_map_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.pseudofunctor B C) (a : B) :

↑F.map_id a = (F.map_id a).hom

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

F.map_functor a b = ↑F.map_functor a b

def category_theory.pseudofunctor.id (B : Type u₁) [category_theory.bicategory B] :

category_theory.pseudofunctor B B

The identity pseudofunctor.

Equations

category_theory.pseudofunctor.id B = {obj := (category_theory.prelax_functor.id B).obj, map := (category_theory.prelax_functor.id B).map, map₂ := (category_theory.prelax_functor.id B).map₂, map_id := λ (a : B), category_theory.iso.refl (𝟙 a), map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), category_theory.iso.refl (f ≫ g), map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

@[simp]

theorem category_theory.pseudofunctor.id_map₂ (B : Type u₁) [category_theory.bicategory B] {a b : B} {f g : a ⟶ b} (ᾰ : f ⟶ g) :

(category_theory.pseudofunctor.id B).map₂ ᾰ = (category_theory.prelax_functor.id B).map₂ ᾰ

@[simp]

theorem category_theory.pseudofunctor.id_map_comp (B : Type u₁) [category_theory.bicategory B] (a b c : B) (f : a ⟶ b) (g : b ⟶ c) :

(category_theory.pseudofunctor.id B).map_comp f g = category_theory.iso.refl (f ≫ g)

@[simp]

theorem category_theory.pseudofunctor.id_obj (B : Type u₁) [category_theory.bicategory B] (ᾰ : B) :

(category_theory.pseudofunctor.id B).obj ᾰ = (category_theory.prelax_functor.id B).obj ᾰ

@[simp]

theorem category_theory.pseudofunctor.id_map (B : Type u₁) [category_theory.bicategory B] {X Y : B} (ᾰ : X ⟶ Y) :

(category_theory.pseudofunctor.id B).map ᾰ = (category_theory.prelax_functor.id B).map ᾰ

@[simp]

theorem category_theory.pseudofunctor.id_map_id (B : Type u₁) [category_theory.bicategory B] (a : B) :

(category_theory.pseudofunctor.id B).map_id a = category_theory.iso.refl (𝟙 a)

@[protected, instance]

def category_theory.pseudofunctor.inhabited {B : Type u₁} [category_theory.bicategory B] :

inhabited (category_theory.pseudofunctor B B)

Equations

category_theory.pseudofunctor.inhabited = {default := category_theory.pseudofunctor.id B _inst_1}

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

def category_theory.pseudofunctor.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) :

category_theory.pseudofunctor B D

Composition of pseudofunctors.

Equations

F.comp G = {obj := (↑F.comp ↑G).obj, map := (↑F.comp ↑G).map, map₂ := (↑F.comp ↑G).map₂, map_id := λ (a : B), (G.map_functor (↑↑F.obj a) (↑↑F.obj a)).map_iso (F.map_id a) ≪≫ G.map_id (F.obj a), map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), (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), map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

@[simp]

theorem category_theory.pseudofunctor.comp_map_id {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) :

(F.comp G).map_id a = (G.map_functor (↑↑F.obj a) (↑↑F.obj a)).map_iso (F.map_id a) ≪≫ G.map_id (F.obj a)

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

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) (F' : F.pseudo_core) (ᾰ : B) :

(category_theory.pseudofunctor.mk_of_oplax F F').obj ᾰ = ↑F.obj ᾰ

@[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) (F' : F.pseudo_core) {a b : B} {f g : a ⟶ b} (ᾰ : f ⟶ g) :

(category_theory.pseudofunctor.mk_of_oplax F F').map₂ ᾰ = ↑F.map₂ ᾰ

@[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) (F' : F.pseudo_core) {X Y : B} (ᾰ : X ⟶ Y) :

(category_theory.pseudofunctor.mk_of_oplax F F').map ᾰ = ↑F.map ᾰ

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) (F' : F.pseudo_core) :

category_theory.pseudofunctor B C

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

Equations

category_theory.pseudofunctor.mk_of_oplax F F' = {obj := ↑F.obj, map := ↑F.map, map₂ := ↑F.map₂, map_id := F'.map_id_iso, map_comp := λ (_x _x_1 _x_2 : B), F'.map_comp_iso, map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

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

(category_theory.pseudofunctor.mk_of_oplax F F').map_comp f g = F'.map_comp_iso f g

@[simp]

theorem category_theory.pseudofunctor.mk_of_oplax_map_id {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) (a : B) :

(category_theory.pseudofunctor.mk_of_oplax F F').map_id a = F'.map_id_iso a

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

(category_theory.pseudofunctor.mk_of_oplax' F).map₂ ᾰ = ↑F.map₂ ᾰ

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

(category_theory.pseudofunctor.mk_of_oplax' F).map_comp f g = category_theory.as_iso (F.map_comp f g)

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

(category_theory.pseudofunctor.mk_of_oplax' F).map ᾰ = ↑F.map ᾰ

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

(category_theory.pseudofunctor.mk_of_oplax' F).obj ᾰ = ↑F.obj ᾰ

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

category_theory.pseudofunctor B C

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

Equations

category_theory.pseudofunctor.mk_of_oplax' F = {obj := ↑F.obj, map := ↑F.map, map₂ := ↑F.map₂, map_id := λ (a : B), category_theory.as_iso (F.map_id a), map_comp := λ (a b c : B) (f : a ⟶ b) (g : b ⟶ c), category_theory.as_iso (F.map_comp f g), map₂_id' := _, map₂_comp' := _, map₂_whisker_left' := _, map₂_whisker_right' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

@[simp]

theorem category_theory.pseudofunctor.mk_of_oplax'_map_id {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) :

(category_theory.pseudofunctor.mk_of_oplax' F).map_id a = category_theory.as_iso (F.map_id a)