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

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.

source

structure CategoryTheory.PrelaxFunctor (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] (C : Type u₂) [Quiver C] [(a b : C) → Quiver (a ⟶ b)] extends Prefunctor :

Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

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

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)
The action of a prelax functor on 2-morphisms.

Instances For

source

instance CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] :

Coe (CategoryTheory.PrelaxFunctor B C) (B ⥤q C)

Equations

CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor = { coe := CategoryTheory.PrelaxFunctor.toPrefunctor }

source

@[simp]

theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :

↑(CategoryTheory.PrelaxFunctor.id B) = 𝟭q B

source

@[simp]

theorem CategoryTheory.PrelaxFunctor.id_map₂ (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :

∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (CategoryTheory.PrelaxFunctor.id B).map₂ η = η

source

def CategoryTheory.PrelaxFunctor.id (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :

CategoryTheory.PrelaxFunctor B B

The identity prelax functor.

Equations

CategoryTheory.PrelaxFunctor.id B = let __src := 𝟭q B; { toPrefunctor := __src, map₂ := fun {a b : B} {f g : a ⟶ b} (η : f ⟶ g) => η }

Instances For

source

instance CategoryTheory.PrelaxFunctor.instInhabited {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] :

Inhabited (CategoryTheory.PrelaxFunctor B B)

Equations

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

source

@[simp]

theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor {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 : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :

↑(F.comp G) = ↑F ⋙q ↑G

source

@[simp]

theorem CategoryTheory.PrelaxFunctor.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 : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :

∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (F.comp G).map₂ η = G.map₂ (F.map₂ η)

source

def CategoryTheory.PrelaxFunctor.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 : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :

CategoryTheory.PrelaxFunctor B D

Composition of prelax functors.

Equations

F.comp G = let __src := ↑F ⋙q ↑G; { toPrefunctor := __src, map₂ := fun {a b : B} {f g : a ⟶ b} (η : f ⟶ g) => G.map₂ (F.map₂ η) }

Instances For

source

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.toPrelaxFunctor).obj X ⟶ (↑self.toPrelaxFunctor).obj Y)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → ((↑self.toPrelaxFunctor).map f ⟶ (↑self.toPrelaxFunctor).map g)
mapId : (a : B) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).obj a)
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).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.toPrelaxFunctor).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.toPrelaxFunctor).map f) (self.map₂ η))
map₂_id : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).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₂ θ)
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.toPrelaxFunctor).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.toPrelaxFunctor).map h)) (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).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.toPrelaxFunctor).map f)) (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).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.toPrelaxFunctor).map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom)

Instances For

source

@[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.toPrelaxFunctor).map g))

source

@[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.toPrelaxFunctor).map f) (self.map₂ η))

source

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_id {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.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).map f)

source

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :

self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)

source

@[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.toPrelaxFunctor).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.toPrelaxFunctor).map h)) (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom)

source

@[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.toPrelaxFunctor).map f)) (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom)

source

@[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.toPrelaxFunctor).map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom)

source

@[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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).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.toPrelaxFunctor).map f) (self.map₂ η)) h)

source

@[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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj c} (h : CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f') ((↑self.toPrelaxFunctor).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.toPrelaxFunctor).map g)) h)

source

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

source

theorem CategoryTheory.OplaxFunctor.map₂_comp_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} {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) :

CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (self.map₂ η) (CategoryTheory.CategoryStruct.comp (self.map₂ θ) h)

source

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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).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.toPrelaxFunctor).map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom h))

source

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.toPrelaxFunctor).obj a ⟶ (↑self.toPrelaxFunctor).obj b} (h : (↑self.toPrelaxFunctor).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.toPrelaxFunctor).map f) (self.mapId b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom h))

source

instance CategoryTheory.OplaxFunctor.hasCoeToPrelax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] :

Coe (CategoryTheory.OplaxFunctor B C) (CategoryTheory.PrelaxFunctor B C)

Equations

CategoryTheory.OplaxFunctor.hasCoeToPrelax = { coe := CategoryTheory.OplaxFunctor.toPrelaxFunctor }

source

@[simp]

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

(F.mapFunctor a b).obj f = (↑F.toPrelaxFunctor).map f

source

@[simp]

theorem CategoryTheory.OplaxFunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) :

∀ {X Y : a ⟶ b} (η : X ⟶ Y), (F.mapFunctor a b).map η = F.map₂ η

source

def CategoryTheory.OplaxFunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) :

CategoryTheory.Functor (a ⟶ b) ((↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b)

Function between 1-morphisms as a functor.

Equations

F.mapFunctor a b = { obj := fun (f : a ⟶ b) => (↑F.toPrelaxFunctor).map f, map := fun {X Y : a ⟶ b} (η : X ⟶ Y) => F.map₂ η, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂Iso_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) :

(F.map₂Iso η).hom = F.map₂ η.hom

source

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂Iso_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) :

(F.map₂Iso η).inv = F.map₂ η.inv

source

@[reducible, inline]

abbrev CategoryTheory.OplaxFunctor.map₂Iso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) :

(↑F.toPrelaxFunctor).map f ≅ (↑F.toPrelaxFunctor).map g

An oplax functor F : B ⥤ C sends 2-isomorphisms η : f ≅ f to 2-isomorphisms F.map f ≅ F.map g

Equations

F.map₂Iso η = (F.mapFunctor a b).mapIso η

Instances For

source

instance CategoryTheory.OplaxFunctor.map₂_isIso {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] :

CategoryTheory.IsIso (F.map₂ η)

Equations

⋯ = ⋯

source

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] :

F.map₂ (CategoryTheory.inv η) = CategoryTheory.inv (F.map₂ η)

source

theorem CategoryTheory.OplaxFunctor.map₂_hom_inv_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] {Z : (↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b} (h : (↑F.toPrelaxFunctor).map f ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map₂ η) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) h) = h

source

theorem CategoryTheory.OplaxFunctor.map₂_hom_inv {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] :

CategoryTheory.CategoryStruct.comp (F.map₂ η) (F.map₂ (CategoryTheory.inv η)) = CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).map f)

source

theorem CategoryTheory.OplaxFunctor.map₂_inv_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] {Z : (↑F.toPrelaxFunctor).obj a ⟶ (↑F.toPrelaxFunctor).obj b} (h : (↑F.toPrelaxFunctor).map g ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (CategoryTheory.CategoryStruct.comp (F.map₂ η) h) = h

source

theorem CategoryTheory.OplaxFunctor.map₂_inv_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [CategoryTheory.IsIso η] :

CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (F.map₂ η) = CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).map g)

source

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

source

@[simp]

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

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

source

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

source

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.

Instances For

source

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

Inhabited (CategoryTheory.OplaxFunctor B B)

Equations

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

source

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.

Instances For

source

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.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).obj a)
mapCompIso : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → (↑F.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).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

Instances For

source

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

source

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

Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Oplax functors #

Main definitions #

Future work #