mathlib documentation

category_theory.bicategory.natural_transformation

Oplax natural transformations #

Just as there are natural transformations between functors, there are oplax natural transformations between oplax functors. The equality in the naturality of natural transformations is replaced by a specified 2-morphism F.map f ≫ app b ⟶ app a ≫ G.map f in the case of oplax natural transformations.

Main definitions #

source
structure category_theory.oplax_nat_trans {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) :
Type (max u₁ v₁ v₂ w₂)

If η is an oplax natural transformation between F and G, we have a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. We also have a 2-morphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b. These 2-morphisms satisfies the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

Instances for category_theory.oplax_nat_trans
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) :
category_theory.bicategory.whisker_right (F.map₂ η) (self.app b) ≫ self.naturality g = self.naturality f ≫ category_theory.bicategory.whisker_left (self.app a) (G.map₂ η)
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) (a : B) :
self.naturality (𝟙 a) ≫ category_theory.bicategory.whisker_left (self.app a) (G.map_id a) = category_theory.bicategory.whisker_right (F.map_id a) (self.app a) ≫ (category_theory.bicategory.left_unitor (self.app a)).hom ≫ (category_theory.bicategory.right_unitor (self.app a)).inv
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) :
self.naturality (f ≫ g) ≫ category_theory.bicategory.whisker_left (self.app a) (G.map_comp f g) = category_theory.bicategory.whisker_right (F.map_comp f g) (self.app c) ≫ (category_theory.bicategory.associator (F.map f) (F.map g) (self.app c)).hom ≫ category_theory.bicategory.whisker_left (F.map f) (self.naturality g) ≫ (category_theory.bicategory.associator (F.map f) (self.app b) (G.map g)).inv ≫ category_theory.bicategory.whisker_right (self.naturality f) (G.map g) ≫ (category_theory.bicategory.associator (self.app a) (G.map f) (G.map g)).hom
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_id_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) (a : B) {X' : F.obj a ⟶ G.obj a} (f' : self.app a ≫ 𝟙 (G.obj a) ⟶ X') :
self.naturality (𝟙 a) ≫ category_theory.bicategory.whisker_left (self.app a) (G.map_id a) ≫ f' = category_theory.bicategory.whisker_right (F.map_id a) (self.app a) ≫ (category_theory.bicategory.left_unitor (self.app a)).hom ≫ (category_theory.bicategory.right_unitor (self.app a)).inv ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {X' : F.obj a ⟶ G.obj b} (f' : self.app a ≫ G.map g ⟶ X') :
category_theory.bicategory.whisker_right (F.map₂ η) (self.app b) ≫ self.naturality g ≫ f' = self.naturality f ≫ category_theory.bicategory.whisker_left (self.app a) (G.map₂ η) ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.naturality_comp_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (self : category_theory.oplax_nat_trans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {X' : F.obj a ⟶ G.obj c} (f' : self.app a ≫ G.map f ≫ G.map g ⟶ X') :
self.naturality (f ≫ g) ≫ category_theory.bicategory.whisker_left (self.app a) (G.map_comp f g) ≫ f' = category_theory.bicategory.whisker_right (F.map_comp f g) (self.app c) ≫ (category_theory.bicategory.associator (F.map f) (F.map g) (self.app c)).hom ≫ category_theory.bicategory.whisker_left (F.map f) (self.naturality g) ≫ (category_theory.bicategory.associator (F.map f) (self.app b) (G.map g)).inv ≫ category_theory.bicategory.whisker_right (self.naturality f) (G.map g) ≫ (category_theory.bicategory.associator (self.app a) (G.map f) (G.map g)).hom ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.id_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (a : B) :
(category_theory.oplax_nat_trans.id F).app a = 𝟙 (F.obj a)
source
def category_theory.oplax_nat_trans.id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :
category_theory.oplax_nat_trans F F

The identity oplax natural transformation.

Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.id_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) (a b : B) (f : a ⟶ b) :
(category_theory.oplax_nat_trans.id F).naturality f = (category_theory.bicategory.right_unitor (F.map f)).hom ≫ (category_theory.bicategory.left_unitor (F.map f)).inv
source
@[protected, instance]
def category_theory.oplax_nat_trans.inhabited {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :
inhabited (category_theory.oplax_nat_trans F F)
Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {X' : a' ⟶ H.obj b} (f' : f ≫ θ.app a ≫ H.map h ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map₂ β) (θ.app b)) ≫ category_theory.bicategory.whisker_left f (θ.naturality h) ≫ f' = category_theory.bicategory.whisker_left f (θ.naturality g) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map₂ β)) ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map₂ β) (θ.app b)) ≫ category_theory.bicategory.whisker_left f (θ.naturality h) = category_theory.bicategory.whisker_left f (θ.naturality g) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map₂ β))
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :
category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map₂ β) (η.app b)) h ≫ category_theory.bicategory.whisker_right (η.naturality g) h = category_theory.bicategory.whisker_right (η.naturality f) h ≫ (category_theory.bicategory.associator (η.app a) (G.map f) h).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map₂ β) h) ≫ (category_theory.bicategory.associator (η.app a) (G.map g) h).inv
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') {X' : F.obj a ⟶ a'} (f' : (η.app a ≫ G.map g) ≫ h ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map₂ β) (η.app b)) h ≫ category_theory.bicategory.whisker_right (η.naturality g) h ≫ f' = category_theory.bicategory.whisker_right (η.naturality f) h ≫ (category_theory.bicategory.associator (η.app a) (G.map f) h).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map₂ β) h) ≫ (category_theory.bicategory.associator (η.app a) (G.map g) h).inv ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :
category_theory.bicategory.whisker_left f (θ.naturality (g ≫ h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map_comp g h)) = category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map_comp g h) (θ.app c)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (G.map g) (G.map h) (θ.app c)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (G.map g) (θ.naturality h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (G.map g) (θ.app b) (H.map h)).inv ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (θ.naturality g) (H.map h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (θ.app a) (H.map g) (H.map h)).hom
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_comp_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {X' : a' ⟶ H.obj c} (f' : f ≫ θ.app a ≫ H.map g ≫ H.map h ⟶ X') :
category_theory.bicategory.whisker_left f (θ.naturality (g ≫ h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map_comp g h)) ≫ f' = category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map_comp g h) (θ.app c)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (G.map g) (G.map h) (θ.app c)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (G.map g) (θ.naturality h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (G.map g) (θ.app b) (H.map h)).inv ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (θ.naturality g) (H.map h)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator (θ.app a) (H.map g) (H.map h)).hom ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
category_theory.bicategory.whisker_right (η.naturality (f ≫ g)) h ≫ (category_theory.bicategory.associator (η.app a) (G.map (f ≫ g)) h).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map_comp f g) h) = category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map_comp f g) (η.app c)) h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (F.map f) (F.map g) (η.app c)).hom h ≫ (category_theory.bicategory.associator (F.map f) (F.map g ≫ η.app c) h).hom ≫ category_theory.bicategory.whisker_left (F.map f) (category_theory.bicategory.whisker_right (η.naturality g) h) ≫ (category_theory.bicategory.associator (F.map f) (η.app b ≫ G.map g) h).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (F.map f) (η.app b) (G.map g)).inv h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (η.naturality f) (G.map g)) h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (η.app a) (G.map f) (G.map g)).hom h ≫ (category_theory.bicategory.associator (η.app a) (G.map f ≫ G.map g) h).hom
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_comp_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') {X' : F.obj a ⟶ a'} (f' : η.app a ≫ (G.map f ≫ G.map g) ≫ h ⟶ X') :
category_theory.bicategory.whisker_right (η.naturality (f ≫ g)) h ≫ (category_theory.bicategory.associator (η.app a) (G.map (f ≫ g)) h).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map_comp f g) h) ≫ f' = category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map_comp f g) (η.app c)) h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (F.map f) (F.map g) (η.app c)).hom h ≫ (category_theory.bicategory.associator (F.map f) (F.map g ≫ η.app c) h).hom ≫ category_theory.bicategory.whisker_left (F.map f) (category_theory.bicategory.whisker_right (η.naturality g) h) ≫ (category_theory.bicategory.associator (F.map f) (η.app b ≫ G.map g) h).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (F.map f) (η.app b) (G.map g)).inv h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (η.naturality f) (G.map g)) h ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator (η.app a) (G.map f) (G.map g)).hom h ≫ (category_theory.bicategory.associator (η.app a) (G.map f ≫ G.map g) h).hom ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) :
category_theory.bicategory.whisker_left f (θ.naturality (𝟙 a)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map_id a)) = category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map_id a) (θ.app a)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.left_unitor (θ.app a)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.right_unitor (θ.app a)).inv
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_id_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {G H : category_theory.oplax_functor B C} (θ : category_theory.oplax_nat_trans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) {X' : a' ⟶ H.obj a} (f' : f ≫ θ.app a ≫ 𝟙 (H.obj a) ⟶ X') :
category_theory.bicategory.whisker_left f (θ.naturality (𝟙 a)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (θ.app a) (H.map_id a)) ≫ f' = category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (G.map_id a) (θ.app a)) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.left_unitor (θ.app a)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.right_unitor (θ.app a)).inv ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_id_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') {X' : F.obj a ⟶ a'} (f' : η.app a ≫ 𝟙 (G.obj a) ≫ f ⟶ X') :
category_theory.bicategory.whisker_right (η.naturality (𝟙 a)) f ≫ (category_theory.bicategory.associator (η.app a) (G.map (𝟙 a)) f).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map_id a) f) ≫ f' = category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map_id a) (η.app a)) f ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor (η.app a)).hom f ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.right_unitor (η.app a)).inv f ≫ (category_theory.bicategory.associator (η.app a) (𝟙 (G.obj a)) f).hom ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') :
category_theory.bicategory.whisker_right (η.naturality (𝟙 a)) f ≫ (category_theory.bicategory.associator (η.app a) (G.map (𝟙 a)) f).hom ≫ category_theory.bicategory.whisker_left (η.app a) (category_theory.bicategory.whisker_right (G.map_id a) f) = category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (F.map_id a) (η.app a)) f ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor (η.app a)).hom f ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.right_unitor (η.app a)).inv f ≫ (category_theory.bicategory.associator (η.app a) (𝟙 (G.obj a)) f).hom
source
@[simp]
theorem category_theory.oplax_nat_trans.vcomp_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) (θ : category_theory.oplax_nat_trans G H) (a : B) :
(η.vcomp θ).app a = η.app a ≫ θ.app a
source
@[simp]
theorem category_theory.oplax_nat_trans.vcomp_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) (θ : category_theory.oplax_nat_trans G H) (a b : B) (f : a ⟶ b) :
(η.vcomp θ).naturality f = (category_theory.bicategory.associator (F.map f) (η.app b) (θ.app b)).inv ≫ category_theory.bicategory.whisker_right (η.naturality f) (θ.app b) ≫ (category_theory.bicategory.associator (η.app a) (G.map f) (θ.app b)).hom ≫ category_theory.bicategory.whisker_left (η.app a) (θ.naturality f) ≫ (category_theory.bicategory.associator (η.app a) (θ.app a) (H.map f)).inv
source
def category_theory.oplax_nat_trans.vcomp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G H : category_theory.oplax_functor B C} (η : category_theory.oplax_nat_trans F G) (θ : category_theory.oplax_nat_trans G H) :
category_theory.oplax_nat_trans F H

Vertical composition of oplax natural transformations.

Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct_to_quiver_hom (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) :
(F ⟶ G) = category_theory.oplax_nat_trans F G
source
@[simp]
theorem category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct_comp (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F G H : category_theory.oplax_functor B C) (η : category_theory.oplax_nat_trans F G) (θ : category_theory.oplax_nat_trans G H) :
η ≫ θ = η.vcomp θ
source
@[simp]
theorem category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct_id (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] (F : category_theory.oplax_functor B C) :
𝟙 F = category_theory.oplax_nat_trans.id F
source
@[protected, instance]
def category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct (B : Type u₁) [category_theory.bicategory B] (C : Type u₂) [category_theory.bicategory C] :
category_theory.category_struct (category_theory.oplax_functor B C)
Equations
source
theorem category_theory.oplax_nat_trans.modification.ext_iff {B : Type u₁} {_inst_1 : category_theory.bicategory B} {C : Type u₂} {_inst_2 : category_theory.bicategory C} {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (x y : category_theory.oplax_nat_trans.modification η θ) :
x = y ↔ x.app = y.app
source
theorem category_theory.oplax_nat_trans.modification.ext {B : Type u₁} {_inst_1 : category_theory.bicategory B} {C : Type u₂} {_inst_2 : category_theory.bicategory C} {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (x y : category_theory.oplax_nat_trans.modification η θ) (h : x.app = y.app) :
x = y
source
@[ext]
structure category_theory.oplax_nat_trans.modification {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor 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.

Instances for category_theory.oplax_nat_trans.modification
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : category_theory.oplax_nat_trans F G} (self : category_theory.oplax_nat_trans.modification η θ) {a b : B} (f : a ⟶ b) :
category_theory.bicategory.whisker_left (F.map f) (self.app b) ≫ θ.naturality f = η.naturality f ≫ category_theory.bicategory.whisker_right (self.app a) (G.map f)
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : category_theory.oplax_nat_trans F G} (self : category_theory.oplax_nat_trans.modification η θ) {a b : B} (f : a ⟶ b) {X' : F.obj a ⟶ G.obj b} (f' : θ.app a ≫ G.map f ⟶ X') :
category_theory.bicategory.whisker_left (F.map f) (self.app b) ≫ θ.naturality f ≫ f' = η.naturality f ≫ category_theory.bicategory.whisker_right (self.app a) (G.map f) ≫ f'
source
def category_theory.oplax_nat_trans.modification.id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) :
category_theory.oplax_nat_trans.modification η η

The identity modification.

Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.id_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) (a : B) :
(category_theory.oplax_nat_trans.modification.id η).app a = 𝟙 (η.app a)
source
@[protected, instance]
def category_theory.oplax_nat_trans.modification.inhabited {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} (η : F ⟶ G) :
inhabited (category_theory.oplax_nat_trans.modification η η)
Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_left_naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) {X' : a' ⟶ G.obj c} (f' : f ≫ θ.app b ≫ G.map g ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (F.map g) (Γ.app c)) ≫ category_theory.bicategory.whisker_left f (θ.naturality g) ≫ f' = category_theory.bicategory.whisker_left f (η.naturality g) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (Γ.app b) (G.map g)) ≫ f'
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_left_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left (F.map g) (Γ.app c)) ≫ category_theory.bicategory.whisker_left f (θ.naturality g) = category_theory.bicategory.whisker_left f (η.naturality g) ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right (Γ.app b) (G.map g))
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_right_naturality {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') :
category_theory.bicategory.whisker_left (F.map f) (category_theory.bicategory.whisker_right (Γ.app b) g) ≫ (category_theory.bicategory.associator (F.map f) (θ.app b) g).inv ≫ category_theory.bicategory.whisker_right (θ.naturality f) g = (category_theory.bicategory.associator (F.map f) (η.app b) g).inv ≫ category_theory.bicategory.whisker_right (η.naturality f) g ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (Γ.app a) (G.map f)) g
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_right_naturality_assoc {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {X' : F.obj a ⟶ a'} (f' : (θ.app a ≫ G.map f) ≫ g ⟶ X') :
category_theory.bicategory.whisker_left (F.map f) (category_theory.bicategory.whisker_right (Γ.app b) g) ≫ (category_theory.bicategory.associator (F.map f) (θ.app b) g).inv ≫ category_theory.bicategory.whisker_right (θ.naturality f) g ≫ f' = (category_theory.bicategory.associator (F.map f) (η.app b) g).inv ≫ category_theory.bicategory.whisker_right (η.naturality f) g ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right (Γ.app a) (G.map f)) g ≫ f'
source
def category_theory.oplax_nat_trans.modification.vcomp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ ι : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) (Δ : category_theory.oplax_nat_trans.modification θ ι) :
category_theory.oplax_nat_trans.modification η ι

Vertical composition of modifications.

Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.modification.vcomp_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ ι : F ⟶ G} (Γ : category_theory.oplax_nat_trans.modification η θ) (Δ : category_theory.oplax_nat_trans.modification θ ι) (a : B) :
(Γ.vcomp Δ).app a = Γ.app a ≫ Δ.app a
source
@[simp]
theorem category_theory.oplax_nat_trans.category_comp {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) (η θ ι : F ⟶ G) (Γ : category_theory.oplax_nat_trans.modification η θ) (Δ : category_theory.oplax_nat_trans.modification θ ι) :
Γ ≫ Δ = Γ.vcomp Δ
source
@[protected, instance]
def category_theory.oplax_nat_trans.category {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) :
category_theory.category (F ⟶ G)

Category structure on the oplax natural transformations between oplax_functors.

Equations
source
@[simp]
theorem category_theory.oplax_nat_trans.category_id {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] (F G : category_theory.oplax_functor B C) (η : F ⟶ G) :
𝟙 η = category_theory.oplax_nat_trans.modification.id η
source
@[simp]
theorem category_theory.oplax_nat_trans.modification_iso.of_components_hom_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (app : Π (a : B), η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), category_theory.bicategory.whisker_left (F.map f) (app b).hom ≫ θ.naturality f = η.naturality f ≫ category_theory.bicategory.whisker_right (app a).hom (G.map f)) (a : B) :
(category_theory.oplax_nat_trans.modification_iso.of_components app naturality).hom.app a = (app a).hom
source
@[simp]
theorem category_theory.oplax_nat_trans.modification_iso.of_components_inv_app {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (app : Π (a : B), η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), category_theory.bicategory.whisker_left (F.map f) (app b).hom ≫ θ.naturality f = η.naturality f ≫ category_theory.bicategory.whisker_right (app a).hom (G.map f)) (a : B) :
(category_theory.oplax_nat_trans.modification_iso.of_components app naturality).inv.app a = (app a).inv
source
def category_theory.oplax_nat_trans.modification_iso.of_components {B : Type u₁} [category_theory.bicategory B] {C : Type u₂} [category_theory.bicategory C] {F G : category_theory.oplax_functor B C} {η θ : F ⟶ G} (app : Π (a : B), η.app a ≅ θ.app a) (naturality : ∀ {a b : B} (f : a ⟶ b), category_theory.bicategory.whisker_left (F.map f) (app b).hom ≫ θ.naturality f = η.naturality f ≫ category_theory.bicategory.whisker_right (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