Strictly unitary lax functors and pseudofunctors

In this file, we define strictly unitary Lax functors and strictly unitary pseudofunctors between bicategories.

A lax functor F is said to be strictly unitary (sometimes, they are also called normal) if there is an equality F.obj (𝟙 _) = 𝟙 (F.obj x) and if the unit 2-morphism F.obj (𝟙 _) → 𝟙 (F.obj _) is the identity 2-morphism induced by this equality.

A pseudofunctor is called strictly unitary (or a normal homomorphism) if it satisfies the same condition (i.e its "underlying" lax functor is strictly unitary).

References

• Kerodon, section 2.2.2.4

TODOs

• Define lax-composable (resp. pseudo-composable) arrows as strictly unitary lax (resp. pseudo-) functors out of LocallyDiscrete Fin n.
• Define identity-component oplax natural transformations ("icons") between strictly unitary pseudofunctors and construct a bicategory structure on bicategories, strictly unitary pseudofunctors and icons.
• Construct the Duskin of a bicategory using lax-composable arrows
• Construct the 2-nerve of a bicategory using pseudo-composable arrows

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

A strictly unitary lax functor F between bicategories B and C is a lax functor F from B to C such that the structure 1-cell 𝟙 (obj X) ⟶ map (𝟙 X) is in fact an identity 1-cell for every X : B.

• 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) : CategoryStruct.id (self.obj a) ⟶ self.map (CategoryStruct.id a)
• mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.map f) (self.map g) ⟶ self.map (CategoryStruct.comp f g)
• mapComp_naturality_left {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerRight η g)) = CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)
• mapComp_naturality_right {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerLeft f η)) = CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f g')
• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h) (self.map₂ (Bicategory.associator f g h).hom)) = 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)) (self.mapComp f (CategoryStruct.comp g h)))
• map₂_leftUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).inv = CategoryStruct.comp (Bicategory.leftUnitor (self.map f)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.mapId a) (self.map f)) (self.mapComp (CategoryStruct.id a) f))
• map₂_rightUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).inv = CategoryStruct.comp (Bicategory.rightUnitor (self.map f)).inv (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapId b)) (self.mapComp f (CategoryStruct.id b)))
• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• mapId_eq_eqToHom (X : B) : self.mapId X = eqToHom ⋯

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

A helper structure that bundles the necessary data to construct a StrictlyUnitaryLaxFunctor without specifying the redundant field mapId.

• obj : B → C

  action on objects

• map {X Y : B} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)

  action on 1-morhisms

• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (self.map f ⟶ self.map g)

  action on 2-morphisms

• 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₂ θ)
• mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.map f) (self.map g) ⟶ self.map (CategoryStruct.comp f g)

  structure 2-morphism for composition of 1-morphism

• mapComp_naturality_left {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerRight η g)) = CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)
• mapComp_naturality_right {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerLeft f η)) = CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f g')
• map₂_leftUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).inv = CategoryStruct.comp (Bicategory.leftUnitor (self.map f)).inv (CategoryStruct.comp (eqToHom ⋯) (self.mapComp (CategoryStruct.id a) f))
• map₂_rightUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).inv = CategoryStruct.comp (Bicategory.rightUnitor (self.map f)).inv (CategoryStruct.comp (eqToHom ⋯) (self.mapComp f (CategoryStruct.id b)))
• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h) (self.map₂ (Bicategory.associator f g h).hom)) = 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)) (self.mapComp f (CategoryStruct.comp g h)))

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

An alternate constructor for strictly unitary lax functors that does not require the mapId fields, and that adapts the map₂_leftUnitor and map₂_rightUnitor to the fact that the functor is strictly unitary.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_isIso {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) (x : B) : IsIso (F.mapId x)

def CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) (x : B) : CategoryStruct.id (F.obj x) ≅ F.map (CategoryStruct.id x)

Promote the morphism F.mapId x : 𝟙 (F.obj x) ⟶ F.map (𝟙 x) to an isomorphism when F is strictly unitary.

Equations

• F.mapIdIso x = { hom := F.mapId x, inv := CategoryTheory.eqToHom ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) (x : B) : (F.mapIdIso x).hom = F.mapId x

@[simp]

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) (x : B) : (F.mapIdIso x).inv = eqToHom ⋯

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

The identity StrictlyUnitaryLaxFunctor.

Equations

• CategoryTheory.StrictlyUnitaryLaxFunctor.id B = { toLaxFunctor := CategoryTheory.LaxFunctor.id B, map_id := ⋯, mapId_eq_eqToHom := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapId (B : Type u₁) [Bicategory B] (a : B) : (id B).mapId a = CategoryStruct.id (CategoryStruct.id a)

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

Composition of StrictlyUnitaryLaxFunctor.

Equations

• F.comp G = { toLaxFunctor := F.comp G.toLaxFunctor, map_id := ⋯, mapId_eq_eqToHom := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.ext {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {x y : StrictlyUnitaryLaxFunctor B C} (obj : x.obj = y.obj) (map : @Prefunctor.map B inst✝.toQuiver C inst✝¹.toQuiver x.toPrefunctor ≍ @Prefunctor.map B inst✝.toQuiver C inst✝¹.toQuiver y.toPrefunctor) (map₂ : @PrelaxFunctorStruct.map₂ B inst✝.toQuiver (fun (a b : B) => (Bicategory.homCategory a b).toQuiver) C inst✝¹.toQuiver (fun (a b : C) => (Bicategory.homCategory a b).toQuiver) x.toPrelaxFunctorStruct ≍ @PrelaxFunctorStruct.map₂ B inst✝.toQuiver (fun (a b : B) => (Bicategory.homCategory a b).toQuiver) C inst✝¹.toQuiver (fun (a b : C) => (Bicategory.homCategory a b).toQuiver) y.toPrelaxFunctorStruct) (mapId : x.mapId ≍ y.mapId) (mapComp : @LaxFunctor.mapComp B inst✝ C inst✝¹ x.toLaxFunctor ≍ @LaxFunctor.mapComp B inst✝ C inst✝¹ y.toLaxFunctor) : x = y

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {x y : StrictlyUnitaryLaxFunctor B C} : x = y ↔ x.obj = y.obj ∧ @Prefunctor.map B inst✝.toQuiver C inst✝¹.toQuiver x.toPrefunctor ≍ @Prefunctor.map B inst✝.toQuiver C inst✝¹.toQuiver y.toPrefunctor ∧ @PrelaxFunctorStruct.map₂ B inst✝.toQuiver (fun (a b : B) => (Bicategory.homCategory a b).toQuiver) C inst✝¹.toQuiver (fun (a b : C) => (Bicategory.homCategory a b).toQuiver) x.toPrelaxFunctorStruct ≍ @PrelaxFunctorStruct.map₂ B inst✝.toQuiver (fun (a b : B) => (Bicategory.homCategory a b).toQuiver) C inst✝¹.toQuiver (fun (a b : C) => (Bicategory.homCategory a b).toQuiver) y.toPrelaxFunctorStruct ∧ x.mapId ≍ y.mapId ∧ @LaxFunctor.mapComp B inst✝ C inst✝¹ x.toLaxFunctor ≍ @LaxFunctor.mapComp B inst✝ C inst✝¹ y.toLaxFunctor

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.comp_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) : F.comp (id C) = F

Composition of StrictlyUnitaryLaxFunctor is strictly right unitary

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.id_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryLaxFunctor B C) : (id B).comp F = F

Composition of StrictlyUnitaryLaxFunctor is strictly left unitary

theorem CategoryTheory.StrictlyUnitaryLaxFunctor.comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] {E : Type u₄} [Bicategory E] (F : StrictlyUnitaryLaxFunctor B C) (G : StrictlyUnitaryLaxFunctor C D) (H : StrictlyUnitaryLaxFunctor D E) : (F.comp G).comp H = F.comp (G.comp H)

Composition of StrictlyUnitaryLaxFunctor is strictly associative

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

A strictly unitary pseudofunctor (sometimes called a "normal homomorphism) F between bicategories B and C is a lax functor F from B to C such that the structure isomorphism map (𝟙 X) ≅ 𝟙 (F.obj X) is in fact an identity 1-cell for every X : B (in particular, there is an equality F.map (𝟙 X) = 𝟙 (F.obj x)).

• 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 ⋯

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

A helper structure that bundles the necessary data to construct a StrictlyUnitaryPseudofunctor without specifying the redundant field mapId

• obj : B → C

  action on objects

• map {X Y : B} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)

  action on 1-morphisms

• map_id (X : B) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (self.map f ⟶ self.map g)

  action on 2-morphisms

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

  structure 2-isomorphism for composition of 1-morphisms

• 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₂_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 (eqToHom ⋯) (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 (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 (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)))

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

An alternate constructor for strictly unitary lax functors that does not require the mapId fields, and that adapts the map₂_leftUnitor and map₂_rightUnitor to the fact that the functor is strictly unitary.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) : StrictlyUnitaryLaxFunctor B C

By forgetting the inverse to mapComp, a StrictlyUnitaryPseudofunctor is a StrictlyUnitaryLaxFunctor.

Equations

• F.toStrictlyUnitaryLaxFunctor = { toLaxFunctor := F.toLax, map_id := ⋯, mapId_eq_eqToHom := ⋯ }

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) (x : B) : F.toStrictlyUnitaryLaxFunctor.obj x = F.obj x

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) {x y : B} (f : x ⟶ y) : F.toStrictlyUnitaryLaxFunctor.map f = F.map f

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map₂ {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) {x y : B} {f g : x ⟶ y} (η : f ⟶ g) : F.toStrictlyUnitaryLaxFunctor.map₂ η = F.map₂ η

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) {x y z : B} (f : x ⟶ y) (g : y ⟶ z) : F.toStrictlyUnitaryLaxFunctor.mapComp f g = (F.mapComp f g).inv

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : StrictlyUnitaryPseudofunctor B C) {x : B} : F.toStrictlyUnitaryLaxFunctor.mapId x = (F.mapId x).inv

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

The identity StrictlyUnitaryPseudofunctor.

Equations

• CategoryTheory.StrictlyUnitaryPseudofunctor.id B = { toPseudofunctor := CategoryTheory.Pseudofunctor.id B, map_id := ⋯, mapId_eq_eqToIso := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.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.StrictlyUnitaryPseudofunctor.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)

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

Composition of StrictlyUnitaryPseudofunctor.

Equations

• F.comp G = { toPseudofunctor := F.comp G.toPseudofunctor, map_id := ⋯, mapId_eq_eqToIso := ⋯ }

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor 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.StrictlyUnitaryPseudofunctor.comp_map {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor C D) {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : (F.comp G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapComp_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor 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.StrictlyUnitaryPseudofunctor.comp_map₂ {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor C D) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : (F.comp G).map₂ η = G.map₂ (F.map₂ η)

@[simp]

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

@[simp]

theorem CategoryTheory.StrictlyUnitaryPseudofunctor.comp_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor 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.StrictlyUnitaryPseudofunctor.comp_mapComp_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : StrictlyUnitaryPseudofunctor B C) (G : StrictlyUnitaryPseudofunctor 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