Modifications between transformations of lax functors

In this file we define modifications of lax and oplax transformations of lax functors.

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

Modifications between oplax transformations are defined similarly.

Main definitions

Given two lax functors F and G, we define:

• LaxTrans.Modification η θ: modifications between lax transformations η and θ between F and G.

• LaxTrans.homCategory F G: the category structure on the lax transformations between F and G, where composition is given by vertical composition. Note that this is a scoped instance in the Lax.LaxTrans namespace, so you need to run open scoped Lax.LaxTrans to access it.

• OplaxTrans.Modification η θ: modifications between oplax transformations η and θ between F and G.

• OplaxTrans.homCategory F G: the category structure on the oplax transformations between F and G, where composition is given by vertical composition. Note that this is a scoped instance in the Lax.OplaxTrans namespace, so you need to run open scoped Lax.OplaxTrans to access it.

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

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

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

  The underlying family of 2-morphisms.

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

  The naturality condition.

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

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

@[simp]

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

The naturality condition.

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

The identity modification.

Equations

• CategoryTheory.Lax.LaxTrans.Modification.id η = { app := fun (a : B) => CategoryTheory.CategoryStruct.id (η.app a), naturality := ⋯ }

@[simp]

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

@[implicit_reducible]

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

Equations

• CategoryTheory.Lax.LaxTrans.Modification.instInhabited = { default := CategoryTheory.Lax.LaxTrans.Modification.id η }

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

Vertical composition of modifications.

Equations

• Γ.vcomp Δ = { app := fun (a : B) => CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a), naturality := ⋯ }

@[simp]

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

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

Type-alias for modifications between lax transformations of lax functors. This is the type used for the 2-homomorphisms in the bicategory of lax functors equipped with lax transformations.

• of :: (
• as : Modification η θ

  The underlying modification of lax transformations.

• )

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

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

@[implicit_reducible]

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

Category structure on the lax natural transformations between lax functors.

Note that this is a scoped instance in the Lax.LaxTrans namespace.

Equations

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

@[simp]

theorem CategoryTheory.Lax.LaxTrans.homCategory_comp_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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)

@[simp]

theorem CategoryTheory.Lax.LaxTrans.homCategory_id_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryStruct.id η).as.app a = CategoryStruct.id (η.app a)

@[implicit_reducible]

instance CategoryTheory.Lax.LaxTrans.instInhabitedHomLaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η : F ⟶ G} : Inhabited (η ⟶ η)

Equations

• CategoryTheory.Lax.LaxTrans.instInhabitedHomLaxFunctor = { default := CategoryTheory.CategoryStruct.id η }

theorem CategoryTheory.Lax.LaxTrans.homCategory.ext {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ} (h : ∀ (a : B), Γ.as.app a = Δ.as.app a) : Γ = Δ

theorem CategoryTheory.Lax.LaxTrans.homCategory.ext_iff {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ} : Γ = Δ ↔ ∀ (a : B), Γ.as.app a = Δ.as.app a

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

  The underlying family of 2-morphisms.

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

  The naturality condition.

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

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

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.Modification.naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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) h) = CategoryStruct.comp (η.naturality f) (CategoryStruct.comp (Bicategory.whiskerRight (self.app a) (G.map f)) h)

The naturality condition.

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

The identity modification.

Equations

• CategoryTheory.Lax.OplaxTrans.Modification.id η = { app := fun (a : B) => CategoryTheory.CategoryStruct.id (η.app a), naturality := ⋯ }

@[simp]

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

@[implicit_reducible]

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

Equations

• CategoryTheory.Lax.OplaxTrans.Modification.instInhabited = { default := CategoryTheory.Lax.OplaxTrans.Modification.id η }

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

Vertical composition of modifications.

Equations

• Γ.vcomp Δ = { app := fun (a : B) => CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a), naturality := ⋯ }

@[simp]

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

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

Type-alias for modifications between oplax transformations of lax functors. This is the type used for the 2-homomorphisms in the bicategory of lax functors equipped with oplax transformations.

• of :: (
• as : Modification η θ

  The underlying modification of oplax transformations.

• )

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

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

@[implicit_reducible]

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

Category structure on the oplax natural transformations between lax functors.

Note that this is a scoped instance in the Lax.OplaxTrans namespace.

Equations

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

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.homCategory_comp_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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)

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.homCategory_id_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} (η : F ⟶ G) (a : B) : (CategoryStruct.id η).as.app a = CategoryStruct.id (η.app a)

@[implicit_reducible]

instance CategoryTheory.Lax.OplaxTrans.instInhabitedHomLaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η : F ⟶ G} : Inhabited (η ⟶ η)

Equations

• CategoryTheory.Lax.OplaxTrans.instInhabitedHomLaxFunctor = { default := CategoryTheory.CategoryStruct.id η }

theorem CategoryTheory.Lax.OplaxTrans.homCategory.ext {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ} (h : ∀ (a : B), Γ.as.app a = Δ.as.app a) : Γ = Δ

theorem CategoryTheory.Lax.OplaxTrans.homCategory.ext_iff {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor B C} {η θ : F ⟶ G} {Γ Δ : η ⟶ θ} : Γ = Δ ↔ ∀ (a : B), Γ.as.app a = Δ.as.app a

def CategoryTheory.Lax.OplaxTrans.isoMk {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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) = CategoryStruct.comp (η.naturality f) (Bicategory.whiskerRight (app a).hom (G.map f)) := by cat_disch) : η ≅ θ

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

Equations

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

@[simp]

theorem CategoryTheory.Lax.OplaxTrans.isoMk_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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) = CategoryStruct.comp (η.naturality f) (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.Lax.OplaxTrans.isoMk_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : LaxFunctor 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) = CategoryStruct.comp (η.naturality f) (Bicategory.whiskerRight (app a).hom (G.map f)) := by cat_disch) (a : B) : (isoMk app naturality).inv.as.app a = (app a).inv