Strict pseudofunctors

In this file we introduce the notion of strict pseudofunctors, which are pseudofunctors such that mapId and mapComp are given by eqToIso _.

To a strict pseudofunctor between strict bicategories we can associate a functor between the underlying categories, see StrictPseudofunctor.toFunctor.

TODO

Once the deprecated Functor/Strict.lean is removed we should rename this file to Functor/Strict.lean.

structure CategoryTheory.StrictPseudofunctor (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] extends CategoryTheory.StrictlyUnitaryPseudofunctor B C : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A strict pseudofunctor F between bicategories B and C is a pseudofunctor F from B to C such that mapId and mapComp are given by eqToIso _.

• 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₂ (CategoryStruct.id f) = CategoryStruct.id (self.map f)
• map₂_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryStruct.comp η θ) = CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• mapId (a : B) : self.map (CategoryStruct.id a) ≅ CategoryStruct.id (self.obj a)
• mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (self.map f) (self.map g)
• map₂_whisker_left {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : self.map₂ (Bicategory.whiskerLeft f η) = CategoryStruct.comp (self.mapComp f g).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f h).inv)
• map₂_whisker_right {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) : self.map₂ (Bicategory.whiskerRight η h) = CategoryStruct.comp (self.mapComp f h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map h)) (self.mapComp g h).inv)
• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : self.map₂ (Bicategory.associator f g h).hom = CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g).hom (self.map h)) (CategoryStruct.comp (Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv) (self.mapComp f (CategoryStruct.comp g h)).inv)))
• map₂_left_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).hom = CategoryStruct.comp (self.mapComp (CategoryStruct.id a) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapId a).hom (self.map f)) (Bicategory.leftUnitor (self.map f)).hom)
• map₂_right_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).hom = CategoryStruct.comp (self.mapComp f (CategoryStruct.id b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapId b).hom) (Bicategory.rightUnitor (self.map f)).hom)
• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• mapId_eq_eqToIso (X : B) : self.mapId X = eqToIso ⋯
• map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
• mapComp_eq_eqToIso {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.mapComp f g = eqToIso ⋯

structure CategoryTheory.StrictPseudofunctorPreCore (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] extends CategoryTheory.PrelaxFunctor B C : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A helper structure that bundles the necessary data to construct a StrictPseudofunctor.

StrictPseudofunctorPreCore does not construct a Pseudofunctor in general, since it does not include the compatibility conditoins on the associator and unitors. However, when the underlying bicategories are strict, a StrictPseudofunctorPreCore does induce a StrictPseudofunctor.

• 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₂ (CategoryStruct.id f) = CategoryStruct.id (self.map f)
• map₂_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryStruct.comp η θ) = CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
• map₂_whisker_left {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') : self.map₂ (Bicategory.whiskerLeft f η) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (eqToHom ⋯))
• map₂_whisker_right {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : self.map₂ (Bicategory.whiskerRight η g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map g)) (eqToHom ⋯))

structure CategoryTheory.StrictPseudofunctorCore (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] extends CategoryTheory.StrictPseudofunctorPreCore B C : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A helper structure that bundles the necessary data to construct a StrictPseudofunctor without specifying the redundant fields mapId and mapComp.

• 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₂ (CategoryStruct.id f) = CategoryStruct.id (self.map f)
• map₂_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryStruct.comp η θ) = CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
• map₂_whisker_left {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') : self.map₂ (Bicategory.whiskerLeft f η) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (eqToHom ⋯))
• map₂_whisker_right {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : self.map₂ (Bicategory.whiskerRight η g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map g)) (eqToHom ⋯))
• map₂_left_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).hom = CategoryStruct.comp (eqToHom ⋯) (Bicategory.leftUnitor (self.map f)).hom
• map₂_right_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).hom = CategoryStruct.comp (eqToHom ⋯) (Bicategory.rightUnitor (self.map f)).hom
• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : self.map₂ (Bicategory.associator f g h).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (eqToHom ⋯))

def CategoryTheory.StrictPseudofunctor.mk' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) : StrictPseudofunctor B C

An alternate constructor for strictly unitary lax functors that does not require the mapId or mapComp fields, and that adapts the compatability conditions to the fact that the pseudofunctor is strict

Equations

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

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk'_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (mk' S).map a✝ = S.map a✝

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk'_obj {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) (a✝ : B) : (mk' S).obj a✝ = S.obj a✝

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk'_map₂ {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (mk' S).map₂ a✝¹ = S.map₂ a✝¹

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk'_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (mk' S).mapComp f g = eqToIso ⋯

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk'_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (S : StrictPseudofunctorCore B C) (x : B) : (mk' S).mapId x = eqToIso ⋯

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

The identity StrictPseudofunctor.

Equations

• CategoryTheory.StrictPseudofunctor.id B = { toStrictlyUnitaryPseudofunctor := CategoryTheory.StrictlyUnitaryPseudofunctor.id B, map_comp := ⋯, mapComp_eq_eqToIso := ⋯ }

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_mapComp_hom (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((id B).mapComp f g).hom = CategoryStruct.id (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_map (B : Type u₁) [Bicategory B] {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : (id B).map f = f

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_mapComp_inv (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((id B).mapComp f g).inv = CategoryStruct.id (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_mapId_hom (B : Type u₁) [Bicategory B] (a : B) : ((id B).mapId a).hom = CategoryStruct.id (CategoryStruct.id a)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_map₂ (B : Type u₁) [Bicategory B] {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : (id B).map₂ η = η

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_mapId_inv (B : Type u₁) [Bicategory B] (a : B) : ((id B).mapId a).inv = CategoryStruct.id (CategoryStruct.id a)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.id_obj (B : Type u₁) [Bicategory B] (X : B) : (id B).obj X = X

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

Composition of StrictPseudofunctor.

Equations

• F.comp G = { toStrictlyUnitaryPseudofunctor := F.comp G.toStrictlyUnitaryPseudofunctor, map_comp := ⋯, mapComp_eq_eqToIso := ⋯ }

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_map₂ {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : (F.comp G).map₂ η = G.map₂ (F.map₂ η)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_mapComp_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((F.comp G).mapComp f g).inv = CategoryStruct.comp (G.mapComp (F.map f) (F.map g)).inv (G.map₂ (F.mapComp f g).inv)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_mapComp_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((F.comp G).mapComp f g).hom = CategoryStruct.comp (G.map₂ (F.mapComp f g).hom) (G.mapComp (F.map f) (F.map g)).hom

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : (F.comp G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) (a : B) : ((F.comp G).mapId a).hom = CategoryStruct.comp (G.map₂ (F.mapId a).hom) (G.mapId (F.obj a)).hom

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) (a : B) : ((F.comp G).mapId a).inv = CategoryStruct.comp (G.mapId (F.obj a)).inv (G.map₂ (F.mapId a).inv)

@[simp]

theorem CategoryTheory.StrictPseudofunctor.comp_obj {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictPseudofunctor B C) (G : StrictPseudofunctor C D) (X : B) : (F.comp G).obj X = G.obj (F.obj X)

def CategoryTheory.StrictPseudofunctor.mk'' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) : StrictPseudofunctor B C

An alternate constructor for strict pseudofunctors between strict bicategories, that only requires the data bundled in StrictPseudofunctorPreCore.

Equations

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

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk''_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (mk'' S).map a✝ = S.map a✝

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk''_obj {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) (a✝ : B) : (mk'' S).obj a✝ = S.obj a✝

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk''_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) (x : B) : (mk'' S).mapId x = eqToIso ⋯

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk''_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (mk'' S).mapComp f g = eqToIso ⋯

@[simp]

theorem CategoryTheory.StrictPseudofunctor.mk''_map₂ {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (S : StrictPseudofunctorPreCore B C) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (mk'' S).map₂ a✝¹ = S.map₂ a✝¹

def CategoryTheory.StrictPseudofunctor.toFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (F : StrictPseudofunctor B C) : Functor B C

A strict pseudofunctor between strict bicategories induces a functor on the underlying categories.

Equations

• F.toFunctor = { obj := F.obj, map := fun {X Y : B} => F.map, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.StrictPseudofunctor.toFunctor_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (F : StrictPseudofunctor B C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : F.toFunctor.map a✝ = F.map a✝

@[simp]

theorem CategoryTheory.StrictPseudofunctor.toFunctor_obj {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] [Bicategory.Strict B] [Bicategory.Strict C] (F : StrictPseudofunctor B C) (a✝ : B) : F.toFunctor.obj a✝ = F.obj a✝