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 #

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