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 #

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
@[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') :
@[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') :
@[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
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