Modifications between oplax transformations

A modification Γ between oplax 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.

Main definitions

• Modification η θ : modifications between oplax transformations η and θ
• Modification.vcomp η θ : the vertical composition of oplax transformations η and θ
• OplaxTrans.category F G : the category structure on the oplax transformations between F and G

structure CategoryTheory.Oplax.Modification {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : 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-morphism.

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

  The naturality condition.

theorem CategoryTheory.Oplax.Modification.ext {B : Type u₁} : ∀ {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C} {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Oplax.Modification η θ}, x.app = y.app → x = y

@[simp]

theorem CategoryTheory.Oplax.Modification.naturality {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (self : CategoryTheory.Oplax.Modification η θ) {a : B} {b : B} (f : a ⟶ b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f))

The naturality condition.

@[simp]

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

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

The identity modification.

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Vertical composition of modifications.

Equations

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

@[simp]

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

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

Category structure on the oplax natural transformations between OplaxFunctors.

Equations

• CategoryTheory.Oplax.category F G = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

theorem CategoryTheory.Oplax.category_comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (G : CategoryTheory.OplaxFunctor B C) : ∀ {X Y Z : F ⟶ G} (Γ : CategoryTheory.Oplax.Modification X Y) (Δ : CategoryTheory.Oplax.Modification Y Z), CategoryTheory.CategoryStruct.comp Γ Δ = Γ.vcomp Δ

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

@[simp]

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

Version of Modification.id_app using category notation

@[simp]

theorem CategoryTheory.Oplax.Modification.comp_app' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {X : B} {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {α : F ⟶ G} {β : F ⟶ G} {γ : F ⟶ G} (m : α ⟶ β) (n : β ⟶ γ) : (CategoryTheory.CategoryStruct.comp m n).app X = CategoryTheory.CategoryStruct.comp (m.app X) (n.app X)

Version of Modification.comp_app using category notation

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

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.ModificationIso.ofComponents_inv_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))) (a : B) : (CategoryTheory.Oplax.ModificationIso.ofComponents app naturality).inv.app a = (app a).inv

@[simp]

theorem CategoryTheory.Oplax.ModificationIso.ofComponents_hom_app {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {F : CategoryTheory.OplaxFunctor B C} {G : CategoryTheory.OplaxFunctor B C} {η : F ⟶ G} {θ : F ⟶ G} (app : (a : B) → η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))) (a : B) : (CategoryTheory.Oplax.ModificationIso.ofComponents app naturality).hom.app a = (app a).hom