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 Prefunctor : 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.

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 }

@[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 : B} : ∀ {f g : a ⟶ b} (a_1 : f ⟶ g), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map₂ a_1 = (F' a b).map a_1

@[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 : B} : ∀ (a_1 : a ⟶ b), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map a_1 = (F' a b).obj a_1

@[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) => η }

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

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

@[simp]

theorem CategoryTheory.PrelaxFunctor.map₂_id {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} (f : a ⟶ b) : self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)

Prelax functors preserves identity 2-morphisms.

@[simp]

theorem CategoryTheory.PrelaxFunctor.map₂_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.PrelaxFunctor 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₂ θ)

Prelax functors preserves compositions of 2-morphisms.

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 : B} {f : a ⟶ b} {g : a ⟶ b} {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.

@[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 := ⋯ }

@[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 := ⋯ }

@[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 : 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 := ⋯ }

@[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 : 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 : 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 : 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 : B} {f : a ⟶ b} {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 η

@[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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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 : B} {f : a ⟶ b} {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