Documentation

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Prelax functors #

This file defines lax prefunctors and prelax functors between bicategories. The point of these definitions is to provide some common API that will be helpful in the development of both lax and oplax functors.

Main definitions #

PrelaxFunctorStruct B C:

A PrelaxFunctorStruct F between quivers B and C, such that both have been equipped with quiver structures on the hom-types, 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),

PrelaxFunctor B C:

A prelax functor F between bicategories B and C is a PrelaxFunctorStruct such that the associated prefunctors between the hom types are all functors. In other words, it is a PrelaxFunctorStruct that satisfies

F.map₂ (𝟙 f) = 𝟙 (F.map f),
F.map₂ (η ≫ θ) = F.map₂ η ≫ F.map₂ θ.

mkOfHomFunctor: constructs a PrelaxFunctor from a map on objects and functors between the corresponding hom types.

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

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

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

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 lax prefunctor on 2-morphisms.

Instances For

def CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) :

CategoryTheory.PrelaxFunctorStruct B C

Construct a lax prefunctor from a map on objects, and prefunctors between the corresponding hom types.

Equations

CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F' = { obj := F, map := fun {a b : B} => (F' a b).obj, map₂ := fun {a b : B} {f g : a ⟶ b} => (F' a b).map }

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_map₂ {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) {a b : B} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) :

(CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map₂ a✝ = (F' a b).map a✝

@[simp]

theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_map {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) {a b : B} (a✝ : a ⟶ b) :

(CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map a✝ = (F' a b).obj a✝

@[simp]

theorem CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_obj {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) (a✝ : B) :

(CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').obj a✝ = F a✝

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

CategoryTheory.PrelaxFunctorStruct B B

The identity lax prefunctor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctorStruct.id_map₂ (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) :

(CategoryTheory.PrelaxFunctorStruct.id B).map₂ η = η

@[simp]

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

(CategoryTheory.PrelaxFunctorStruct.id B).toPrefunctor = 𝟭q B

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

Inhabited (CategoryTheory.PrelaxFunctorStruct B B)

Equations

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

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

CategoryTheory.PrelaxFunctorStruct B D

Composition of lax prefunctors.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctorStruct.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.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) :

(F.comp G).map₂ η = G.map₂ (F.map₂ η)

@[simp]

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

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

structure CategoryTheory.PrelaxFunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctorStruct B C :

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

A prelax functor between bicategories is a lax prefunctor such that map₂ is a functor. This structure will be extended to define LaxFunctor and 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)
map₂_id : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
Prelax functors preserves identity 2-morphisms.
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₂ θ)
Prelax functors preserves compositions of 2-morphisms.

Instances For

theorem CategoryTheory.PrelaxFunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) {Z : self.obj a ⟶ self.obj b} (h✝ : self.map h ⟶ Z) :

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

def CategoryTheory.PrelaxFunctor.mkOfHomFunctors {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B → C) (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)) :

CategoryTheory.PrelaxFunctor B C

Construct a prelax functor from a map on objects, and functors between the corresponding hom types.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B → C) (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)) :

(CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F fun (a b : B) => (F' a b).toPrefunctor

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

CategoryTheory.PrelaxFunctor B B

The identity prelax functor.

Equations

CategoryTheory.PrelaxFunctor.id B = { toPrelaxFunctorStruct := CategoryTheory.PrelaxFunctorStruct.id B, map₂_id := ⋯, map₂_comp := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctor.id_toPrelaxFunctorStruct (B : Type u₁) [CategoryTheory.Bicategory B] :

(CategoryTheory.PrelaxFunctor.id B).toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.id B

instance CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctorStruct {B : Type u₁} [CategoryTheory.Bicategory B] :

Inhabited (CategoryTheory.PrelaxFunctorStruct B B)

Equations

CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctorStruct = { default := CategoryTheory.PrelaxFunctorStruct.id B }

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

CategoryTheory.PrelaxFunctor B D

Composition of prelax functors.

Equations

F.comp G = { toPrelaxFunctorStruct := F.comp G.toPrelaxFunctorStruct, map₂_id := ⋯, map₂_comp := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.PrelaxFunctor.comp_toPrelaxFunctorStruct {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) :

(F.comp G).toPrelaxFunctorStruct = F.comp G.toPrelaxFunctorStruct

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

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

Function between 1-morphisms as a functor.

Equations

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

Instances For

@[simp]

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

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

@[simp]

theorem CategoryTheory.PrelaxFunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) (a b : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) :

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

@[simp]

theorem CategoryTheory.PrelaxFunctor.mkOfHomFunctors_mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B → C) (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)) (a b : B) :

(CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').mapFunctor a b = F' a b

@[reducible, inline]

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

F.map f ≅ F.map g

A prelaxfunctor F 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

@[simp]

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

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

@[simp]

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

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

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

CategoryTheory.IsIso (F.map₂ η)

Equations

⋯ = ⋯

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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