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 functorsF
andG
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 betweenF
andG
- app : Π (a : B), F.obj a ⟶ G.obj a
- naturality : Π {a b : B} (f : a ⟶ b), F.map f ≫ self.app b ⟶ self.app a ≫ G.map f
- naturality_naturality' : (∀ {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₂ η)) . "obviously"
- naturality_id' : (∀ (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) . "obviously"
- naturality_comp' : (∀ {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) . "obviously"
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
- category_theory.oplax_nat_trans.has_sizeof_inst
- category_theory.oplax_nat_trans.inhabited
The identity oplax natural transformation.
Equations
- category_theory.oplax_nat_trans.id F = {app := λ (a : B), 𝟙 (F.obj a), naturality := λ (a b : B) (f : a ⟶ b), (category_theory.bicategory.right_unitor (F.map f)).hom ≫ (category_theory.bicategory.left_unitor (F.map f)).inv, naturality_naturality' := _, naturality_id' := _, naturality_comp' := _}
Equations
Vertical composition of oplax natural transformations.
Equations
- η.vcomp θ = {app := λ (a : B), η.app a ≫ θ.app a, naturality := λ (a b : B) (f : a ⟶ b), (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, naturality_naturality' := _, naturality_id' := _, naturality_comp' := _}
Equations
- category_theory.oplax_nat_trans.category_theory.oplax_functor.category_theory.category_struct B C = {to_quiver := {hom := category_theory.oplax_nat_trans _inst_2}, id := category_theory.oplax_nat_trans.id _inst_2, comp := λ (F G H : category_theory.oplax_functor B C), category_theory.oplax_nat_trans.vcomp}
- app : Π (a : B), η.app a ⟶ θ.app a
- naturality' : (∀ {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)) . "obviously"
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
- category_theory.oplax_nat_trans.modification.has_sizeof_inst
- category_theory.oplax_nat_trans.modification.inhabited
The identity modification.
Equations
- category_theory.oplax_nat_trans.modification.id η = {app := λ (a : B), 𝟙 (η.app a), naturality' := _}
Vertical composition of modifications.
Category structure on the oplax natural transformations between oplax_functors.
Equations
- category_theory.oplax_nat_trans.category F G = {to_category_struct := {to_quiver := {hom := category_theory.oplax_nat_trans.modification G}, id := category_theory.oplax_nat_trans.modification.id G, comp := λ (η θ ι : F ⟶ G), category_theory.oplax_nat_trans.modification.vcomp}, id_comp' := _, comp_id' := _, assoc' := _}
Construct a modification isomorphism between oplax natural transformations by giving object level isomorphisms, and checking naturality only in the forward direction.
Equations
- category_theory.oplax_nat_trans.modification_iso.of_components app naturality = {hom := {app := λ (a : B), (app a).hom, naturality' := naturality}, inv := {app := λ (a : B), (app a).inv, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}