mathlib3 documentation

category_theory.bicategory.natural_transformation

Oplax natural transformations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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