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

Vertical composition of modifications.

Equations
@[protected, instance]

Category structure on the oplax natural transformations between oplax_functors.

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