Modifications between transformations of oplax functors

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

A modification Γ between oplax transformations η and θ (of oplax 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 (F.map f ◁ app b) ≫ θ.naturality f = η.naturality f ≫ (app a ▷ G.map f).

Modifications between strong transformations are defined similarly.

Main definitions

Given two oplax functors F and G, we define:

• 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 a scoped instance in the Oplax.OplaxTrans namespace, so you need to run open scoped Oplax.OplaxTrans to access it.

• StrongTrans.Modification η θ: modifications between strong transformations η and θ between F and G.

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

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

A modification Γ between oplax natural transformations η 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 = η.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.Oplax.OplaxTrans.Modification.ext_iff {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : OplaxFunctor B C} {η θ : F ⟶ G} {x y : Modification η θ} : x = y ↔ x.app = y.app

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

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.Modification.naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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)) = CategoryStruct.comp (Bicategory.whiskerLeft f (η.naturality g)) (Bicategory.whiskerLeft f (Bicategory.whiskerRight (Γ.app b) (G.map g)))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.Modification.whiskerLeft_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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)) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (η.naturality g)) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (Γ.app b) (G.map g))) h)

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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) g)) = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b) g).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) g) (Bicategory.whiskerRight (Bicategory.whiskerRight (Γ.app a) (G.map f)) g))

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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) g) h)) = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b) g).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f) g) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (Γ.app a) (G.map f)) g) h))

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

The identity modification.

Equations

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

@[simp]

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

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

Equations

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

def CategoryTheory.Oplax.OplaxTrans.Modification.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.OplaxTrans.Modification.vcomp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} {η θ ι : F ⟶ G} (Γ : Modification η θ) (Δ : Modification θ ι) (a : B) : (Γ.vcomp Δ).app a = CategoryStruct.comp (Γ.app a) (Δ.app a)

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

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

• of :: (
• as : Modification η θ

  The underlying modification of oplax transformations.

• )

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

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

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

Category structure on the oplax natural transformations between OplaxFunctors.

Note that this a scoped instance in the Oplax.OplaxTrans namespace.

Equations

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

@[simp]

theorem CategoryTheory.Oplax.OplaxTrans.homCategory_comp_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.OplaxTrans.homCategory_id_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (Γ : F ⟶ G) (a : B) : (CategoryStruct.id Γ).as.app a = CategoryStruct.id (Γ.app a)

instance CategoryTheory.Oplax.OplaxTrans.instInhabitedHomOplaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} {η : F ⟶ G} : Inhabited (η ⟶ η)

Equations

• CategoryTheory.Oplax.OplaxTrans.instInhabitedHomOplaxFunctor = { default := CategoryTheory.CategoryStruct.id η }

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

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

def CategoryTheory.Oplax.OplaxTrans.isoMk {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.OplaxTrans.isoMk_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.OplaxTrans.isoMk_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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

@[deprecated CategoryTheory.Oplax.OplaxTrans.isoMk (since := "2025-11-11")]

def CategoryTheory.Oplax.OplaxTrans.ModificationIso.ofComponents {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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) : η ≅ θ

Alias of CategoryTheory.Oplax.OplaxTrans.isoMk.

---

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

Equations

• @CategoryTheory.Oplax.OplaxTrans.ModificationIso.ofComponents = @CategoryTheory.Oplax.OplaxTrans.isoMk

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

A modification Γ between strong natural transformations η and θ (between oplax 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).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-morphisms.

• 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.Oplax.StrongTrans.Modification.ext_iff {B : Type u₁} {inst✝ : Bicategory B} {C : Type u₂} {inst✝¹ : Bicategory C} {F G : OplaxFunctor B C} {η θ : F ⟶ G} {x y : Modification η θ} : x = y ↔ x.app = y.app

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

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.Modification.naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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)

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

The modification between the underlying strong transformations of oplax functors

Equations

• Γ.toOplax = { app := fun (a : B) => Γ.app a, naturality := ⋯ }

@[simp]

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

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

Equations

• CategoryTheory.Oplax.StrongTrans.Modification.hasCoeToOplax = { coe := CategoryTheory.Oplax.StrongTrans.Modification.toOplax }

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

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

Equations

• CategoryTheory.Oplax.StrongTrans.Modification.mkOfOplax Γ = { app := fun (a : B) => Γ.app a, naturality := ⋯ }

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.Modification.whiskerLeft_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.Modification.whiskerLeft_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.Modification.whiskerRight_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.Modification.id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : F ⟶ G) : Modification η η

The identity modification.

Equations

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

@[simp]

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

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

Equations

• CategoryTheory.Oplax.StrongTrans.Modification.instInhabited = { default := CategoryTheory.Oplax.StrongTrans.Modification.id η }

def CategoryTheory.Oplax.StrongTrans.Modification.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.Modification.vcomp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} {η θ ι : F ⟶ G} (Γ : Modification η θ) (Δ : Modification θ ι) (a : B) : (Γ.vcomp Δ).app a = CategoryStruct.comp (Γ.app a) (Δ.app a)

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

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

• of :: (
• as : Modification η θ

  The underlying modification of strong transformations.

• )

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

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

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

Category structure on the strong natural transformations between oplax functors.

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

Equations

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

@[simp]

theorem CategoryTheory.Oplax.StrongTrans.homCategory_comp_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.homCategory_id_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (Γ : F ⟶ G) (a : B) : (CategoryStruct.id Γ).as.app a = CategoryStruct.id (Γ.app a)

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

Equations

• CategoryTheory.Oplax.StrongTrans.instInhabitedHomOplaxFunctor = { default := CategoryTheory.CategoryStruct.id η }

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

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

def CategoryTheory.Oplax.StrongTrans.isoMk {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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 natural transformations (of oplax functors) 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.Oplax.StrongTrans.isoMk_hom_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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.Oplax.StrongTrans.isoMk_inv_as_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor 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