# mathlibdocumentation

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 #

• `oplax_nat_trans F G` : oplax natural transformations between oplax functors `F` and `G`
• `oplax_nat_trans.vcomp η θ` : the vertical composition of oplax natural transformations `η` and `θ`
• `oplax_nat_trans.category F G` : the category structure on the oplax natural transformations between `F` and `G`
structure category_theory.oplax_nat_trans {B : Type u₁} {C : Type u₂} (F G : 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`
@[simp]
theorem category_theory.oplax_nat_trans.naturality_naturality {B : Type u₁} {C : Type u₂} {F G : C} (self : G) {a b : B} {f g : a b} (η : f g) :
(self.app b) self.naturality g = self.naturality f (G.map₂ η)
@[simp]
theorem category_theory.oplax_nat_trans.naturality_id {B : Type u₁} {C : Type u₂} {F G : C} (self : G) (a : B) :
@[simp]
theorem category_theory.oplax_nat_trans.naturality_comp {B : Type u₁} {C : Type u₂} {F G : C} (self : G) {a b c : B} (f : a b) (g : b c) :
self.naturality (f g) (G.map_comp f g) = (self.app c) (F.map g) (self.app c)).hom (self.naturality g) (self.app b) (G.map g)).inv (G.map g) (category_theory.bicategory.associator (self.app a) (G.map f) (G.map g)).hom
@[simp]
theorem category_theory.oplax_nat_trans.naturality_id_assoc {B : Type u₁} {C : Type u₂} {F G : C} (self : G) (a : B) {X' : F.obj a G.obj a} (f' : self.app a 𝟙 (G.obj a) X') :
@[simp]
theorem category_theory.oplax_nat_trans.naturality_naturality_assoc {B : Type u₁} {C : Type u₂} {F G : C} (self : 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') :
(self.app b) self.naturality g f' = self.naturality f (G.map₂ η) f'
@[simp]
theorem category_theory.oplax_nat_trans.naturality_comp_assoc {B : Type u₁} {C : Type u₂} {F G : C} (self : 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) (G.map_comp f g) f' = (self.app c) (F.map g) (self.app c)).hom (self.naturality g) (self.app b) (G.map g)).inv (G.map g) (category_theory.bicategory.associator (self.app a) (G.map f) (G.map g)).hom f'
@[simp]
theorem category_theory.oplax_nat_trans.id_app {B : Type u₁} {C : Type u₂} (F : C) (a : B) :
= 𝟙 (F.obj a)
def category_theory.oplax_nat_trans.id {B : Type u₁} {C : Type u₂} (F : C) :

The identity oplax natural transformation.

Equations
@[simp]
theorem category_theory.oplax_nat_trans.id_naturality {B : Type u₁} {C : Type u₂} (F : C) (a b : B) (f : a b) :
@[protected, instance]
def category_theory.oplax_nat_trans.inhabited {B : Type u₁} {C : Type u₂} (F : C) :
Equations
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_naturality_assoc {B : Type u₁} {C : Type u₂} {G H : C} (θ : 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') :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_naturality {B : Type u₁} {C : Type u₂} {G H : C} (θ : H) {a b : B} {a' : C} (f : a' G.obj a) {g h : a b} (β : g h) :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_naturality {B : Type u₁} {C : Type u₂} {F G : C} (η : G) {a b : B} {a' : C} {f g : a b} (β : f g) (h : G.obj b a') :
= (G.map f) h).hom (G.map g) h).inv
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_naturality_assoc {B : Type u₁} {C : Type u₂} {F G : C} (η : 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') :
= (G.map f) h).hom (G.map g) h).inv f'
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_comp {B : Type u₁} {C : Type u₂} {G H : C} (θ : H) {a b c : B} {a' : C} (f : a' G.obj a) (g : a b) (h : b c) :
(θ.naturality (g h)) = (G.map h) (θ.app c)).hom (θ.app b) (H.map h)).inv (H.map g) (H.map h)).hom
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_comp_assoc {B : Type u₁} {C : Type u₂} {G H : C} (θ : 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') :
(θ.naturality (g h)) f' = (G.map h) (θ.app c)).hom (θ.app b) (H.map h)).inv (H.map g) (H.map h)).hom f'
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_comp {B : Type u₁} {C : Type u₂} {F G : C} (η : G) {a b c : B} {a' : C} (f : a b) (g : b c) (h : G.obj c a') :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_comp_assoc {B : Type u₁} {C : Type u₂} {F G : C} (η : 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') :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_id {B : Type u₁} {C : Type u₂} {G H : C} (θ : H) {a : B} {a' : C} (f : a' G.obj a) :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_left_naturality_id_assoc {B : Type u₁} {C : Type u₂} {G H : C} (θ : H) {a : B} {a' : C} (f : a' G.obj a) {X' : a' H.obj a} (f' : f θ.app a 𝟙 (H.obj a) X') :
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_id_assoc {B : Type u₁} {C : Type u₂} {F G : C} (η : G) {a : B} {a' : C} (f : G.obj a a') {X' : F.obj a a'} (f' : η.app a 𝟙 (G.obj a) f X') :
(G.map (𝟙 a)) f).hom =
@[simp]
theorem category_theory.oplax_nat_trans.whisker_right_naturality_id {B : Type u₁} {C : Type u₂} {F G : C} (η : G) {a : B} {a' : C} (f : G.obj a a') :
(G.map (𝟙 a)) f).hom =
@[simp]
theorem category_theory.oplax_nat_trans.vcomp_app {B : Type u₁} {C : Type u₂} {F G H : C} (η : G) (θ : H) (a : B) :
(η.vcomp θ).app a = η.app a θ.app a
@[simp]
theorem category_theory.oplax_nat_trans.vcomp_naturality {B : Type u₁} {C : Type u₂} {F G H : C} (η : G) (θ : H) (a b : B) (f : a b) :
(η.vcomp θ).naturality f = (η.app b) (θ.app b)).inv (G.map f) (θ.app b)).hom (θ.naturality f) (θ.app a) (H.map f)).inv
def category_theory.oplax_nat_trans.vcomp {B : Type u₁} {C : Type u₂} {F G H : C} (η : G) (θ : H) :

Vertical composition of oplax natural transformations.

Equations
@[simp]
theorem category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct_comp (B : Type u₁) (C : Type u₂) (F G H : C) (η : G) (θ : H) :
η θ = η.vcomp θ
@[simp]
@[protected, instance]
Equations
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 : C} {η θ : F G}  :
x = y x.app = y.app
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 : C} {η θ : F G} (h : x.app = y.app) :
x = y
@[ext]
structure category_theory.oplax_nat_trans.modification {B : Type u₁} {C : Type u₂} {F G : 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`
@[simp]
theorem category_theory.oplax_nat_trans.modification.naturality {B : Type u₁} {C : Type u₂} {F G : C} {η θ : G} (self : θ) {a b : B} (f : a b) :
(self.app b) θ.naturality f = η.naturality f (G.map f)
@[simp]
theorem category_theory.oplax_nat_trans.modification.naturality_assoc {B : Type u₁} {C : Type u₂} {F G : C} {η θ : G} (self : θ) {a b : B} (f : a b) {X' : F.obj a G.obj b} (f' : θ.app a G.map f X') :
(self.app b) θ.naturality f f' = η.naturality f (G.map f) f'
def category_theory.oplax_nat_trans.modification.id {B : Type u₁} {C : Type u₂} {F G : C} (η : F G) :

The identity modification.

Equations
@[simp]
theorem category_theory.oplax_nat_trans.modification.id_app {B : Type u₁} {C : Type u₂} {F G : C} (η : F G) (a : B) :
= 𝟙 (η.app a)
@[protected, instance]
def category_theory.oplax_nat_trans.modification.inhabited {B : Type u₁} {C : Type u₂} {F G : C} (η : F G) :
Equations
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_left_naturality_assoc {B : Type u₁} {C : Type u₂} {F G : C} {η θ : F G} {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') :
=
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_left_naturality {B : Type u₁} {C : Type u₂} {F G : C} {η θ : F G} {b c : B} {a' : C} (f : a' F.obj b) (g : b c) :
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_right_naturality {B : Type u₁} {C : Type u₂} {F G : C} {η θ : F G} {a b : B} {a' : C} (f : a b) (g : G.obj b a') :
(θ.app b) g).inv = (η.app b) g).inv
@[simp]
theorem category_theory.oplax_nat_trans.modification.whisker_right_naturality_assoc {B : Type u₁} {C : Type u₂} {F G : C} {η θ : F G} {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') :
(θ.app b) g).inv = (η.app b) g).inv
def category_theory.oplax_nat_trans.modification.vcomp {B : Type u₁} {C : Type u₂} {F G : C} {η θ ι : F G}  :

Vertical composition of modifications.

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

Category structure on the oplax natural transformations between oplax_functors.

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