Modifications between transformations of pseudofunctors

In this file we define modifications of strong transformations of pseudofunctors. They are defined similarly to modifications of transformations of oplax functors.

Main definitions

Given two pseudofunctors F and G, we define:

• Pseudofunctor.StrongTrans.Modification η θ : modifications between strong transformations η and θ (between F and G).
• Pseudofunctor.StrongTrans.homCategory F G : the category structure on strong transformations between F and G, where the morphisms are modifications, and composition is given by vertical composition of modifications. Note that this a scoped instance in the Pseudofunctor.StrongTrans namespace, so you need to run open scoped Pseudofunctor.StrongTrans to access it.

structure CategoryTheory.Pseudofunctor.StrongTrans.Modification {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η θ : F ⟶ G) : Type (max u₁ w₂)

A modification Γ between strong transformations (of pseudofunctors) η and θ consists of a family of 2-morphisms Γ.app a : η.app a ⟶ θ.app a, which satisfies the equation (F.map f ◁ app b) ≫ (θ.naturality f).hom = (η.naturality f).hom ≫ (app a ▷ G.map f) for each 1-morphism f : a ⟶ b.

• app (a : B) : η.app a ⟶ θ.app a

  The underlying family of 2-morphism.

• naturality {a b : B} (f : a ⟶ b) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.app b)) (θ.naturality f).hom = CategoryStruct.comp (η.naturality f).hom (Bicategory.whiskerRight (self.app a) (G.map f))

  The naturality condition.

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext_iff {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : Pseudofunctor B C} {η θ : F ⟶ G} {x y : Modification η θ} : x = y ↔ x.app = y.app

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : Pseudofunctor B C} {η θ : F ⟶ G} {x y : Modification η θ} (app : x.app = y.app) : x = y

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (self : Modification η θ) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ G.obj b} (h : CategoryStruct.comp (θ.app a) (G.map f) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.app b)) (CategoryStruct.comp (θ.naturality f).hom h) = CategoryStruct.comp (η.naturality f).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.app a) (G.map f)) h)

The naturality condition.

def CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) : Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ)

The modification between the corresponding strong transformation of the underlying oplax functors.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) (a : B) : Γ.toOplax.app a = Γ.app a

instance CategoryTheory.Pseudofunctor.StrongTrans.Modification.hasCoeToOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} : Coe (Modification η θ) (Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ))

def CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ)) : Modification η θ

The modification between strong transformations of pseudofunctors associated to a modification between the underlying strong transformations of oplax functors.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.mkOfOplax_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ)) (a : B) : (mkOfOplax Γ).app a = Γ.app a

def CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} : Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ) ≃ Modification η θ

Modifications between strong transformations of pseudofunctors are equivalent to modifications between the underlying strong transformations of oplax functors.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_apply {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Oplax.StrongTrans.Modification (StrongTrans.toOplax η) (StrongTrans.toOplax θ)) : equivOplax Γ = mkOfOplax Γ

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax_symm_apply {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) : equivOplax.symm Γ = Γ.toOplax

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (F.map g) (Γ.app c))) (Bicategory.whiskerLeft f (θ.naturality g).hom) = CategoryStruct.comp (Bicategory.whiskerLeft f (η.naturality g).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerRight (Γ.app b) (G.map g)))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) {Z : a' ⟶ G.obj c} (h : CategoryStruct.comp f (CategoryStruct.comp (θ.app b) (G.map g)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (F.map g) (Γ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g).hom) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (η.naturality g).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (Γ.app b) (G.map g))) h)

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (Γ.app b) g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (θ.app b) g).inv (Bicategory.whiskerRight (θ.naturality f).hom g)) = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b) g).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom g) (Bicategory.whiskerRight (Bicategory.whiskerRight (Γ.app a) (G.map f)) g))

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (Γ : Modification η θ) {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {Z : F.obj a ⟶ a'} (h : CategoryStruct.comp (CategoryStruct.comp (θ.app a) (G.map f)) g ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (Bicategory.whiskerRight (Γ.app b) g)) (CategoryStruct.comp (Bicategory.associator (F.map f) (θ.app b) g).inv (CategoryStruct.comp (Bicategory.whiskerRight (θ.naturality f).hom g) h)) = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b) g).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom g) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (Γ.app a) (G.map f)) g) h))

def CategoryTheory.Pseudofunctor.StrongTrans.Modification.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) : Modification η η

The identity modification.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η : F ⟶ G) (a : B) : (id η).app a = CategoryStruct.id (η.app a)

instance CategoryTheory.Pseudofunctor.StrongTrans.Modification.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η : F ⟶ G} : Inhabited (Modification η η)

def CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ ι : F ⟶ G} (Γ : Modification η θ) (Δ : Modification θ ι) : Modification η ι

Vertical composition of modifications.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.Modification.vcomp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ ι : F ⟶ G} (Γ : Modification η θ) (Δ : Modification θ ι) (a : B) : (Γ.vcomp Δ).app a = CategoryStruct.comp (Γ.app a) (Δ.app a)

structure CategoryTheory.Pseudofunctor.StrongTrans.Hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (η θ : F ⟶ G) : Type (max u₁ w₂)

Type-alias for modifications between strong transformations of pseudofunctors. This is the type used for the 2-homomorphisms in the bicategory of pseudofunctors.

• of :: (
• as : Modification η θ

  The underlying modification of strong transformations.

• )

theorem CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : Pseudofunctor B C} {η θ : F ⟶ G} {x y : Hom η θ} (as : x.as = y.as) : x = y

theorem CategoryTheory.Pseudofunctor.StrongTrans.Hom.ext_iff {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : Pseudofunctor B C} {η θ : F ⟶ G} {x y : Hom η θ} : x = y ↔ x.as = y.as

def CategoryTheory.Pseudofunctor.StrongTrans.homCategory {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} : Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)

Category structure on the strong transformations between pseudofunctors.

Note that this a scoped instance in the Pseudofunctor.StrongTrans namespace.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.homCategory_id_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} (Γ : F ⟶ G) (a : B) : (CategoryStruct.id Γ).as.app a = CategoryStruct.id (Γ.app a)

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.homCategory_comp_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {X✝ Y✝ Z✝ : F ⟶ G} (Γ : Hom X✝ Y✝) (Δ : Hom Y✝ Z✝) (a : B) : (CategoryStruct.comp Γ Δ).as.app a = CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)

instance CategoryTheory.Pseudofunctor.StrongTrans.instInhabitedHom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η : F ⟶ G} : Inhabited (η ⟶ η)

theorem CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ} (w : ∀ (b : B), m.as.app b = n.as.app b) : m = n

theorem CategoryTheory.Pseudofunctor.StrongTrans.homCategory.ext_iff {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ} : m = n ↔ ∀ (b : B), m.as.app b = n.as.app b

def CategoryTheory.Pseudofunctor.StrongTrans.isoMk {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f).hom = CategoryStruct.comp (η.naturality f).hom (Bicategory.whiskerRight (app a).hom (G.map f)) := by cat_disch) : η ≅ θ

Construct a modification isomorphism between strong transformations by giving object level isomorphisms, and checking naturality only in the forward direction.

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.isoMk_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f).hom = CategoryStruct.comp (η.naturality f).hom (Bicategory.whiskerRight (app a).hom (G.map f)) := by cat_disch) (a : B) : (isoMk app naturality).hom.as.app a = (app a).hom

@[simp]

theorem CategoryTheory.Pseudofunctor.StrongTrans.isoMk_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : Pseudofunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f).hom = CategoryStruct.comp (η.naturality f).hom (Bicategory.whiskerRight (app a).hom (G.map f)) := by cat_disch) (a : B) : (isoMk app naturality).inv.as.app a = (app a).inv