Strong natural transformations #
A strong natural transformation is an oplax natural transformation such that each component 2-cell is an isomorphism.
Main definitions #
StrongOplaxNatTrans F G
: strong natural transformations between oplax functorsF
andG
.mkOfOplax η η'
: given an oplax natural transformationη
such that each component 2-cell is an isomorphism,mkOfOplax
gives the corresponding strong natural transformation.StrongOplaxNatTrans.vcomp η θ
: the vertical composition of strong natural transformationsη
andθ
.StrongOplaxNatTrans.category F G
: a category structure on pseudofunctors betweenF
andG
, where the morphisms are strong natural transformations.
TODO #
After having defined lax functors, we should define 3 different types of strong natural transformations:
- strong natural transformations between oplax functors (as defined here).
- strong natural transformations between lax functors.
- strong natural transformations between pseudofunctors. From these types of strong natural transformations, we can define the underlying natural transformations between the underlying oplax resp. lax functors. Many properties can then be inferred from these.
References #
A strong natural transformation between oplax functors F
and G
is a natural transformation
that is "natural up to 2-isomorphisms".
More precisely, it consists of the following:
- a 1-morphism
η.app a : F.obj a ⟶ G.obj a
for each objecta : B
. - a 2-isomorphism
η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f
for each 1-morphismf : a ⟶ b
. - These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.
- app : (a : B) → F.obj a ⟶ G.obj a
- naturality : {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp (F.map f) (self.app b) ≅ CategoryTheory.CategoryStruct.comp (self.app a) (G.map f)
- naturality_naturality : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g).hom = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
- naturality_id : ∀ (a : B), CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
- naturality_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))
Instances For
The underlying oplax natural transformation of a strong natural transformation.
Equations
Instances For
Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.
Equations
- CategoryTheory.StrongOplaxNatTrans.mkOfOplax η η' = { app := η.app, naturality := fun {a b : B} => η'.naturality, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }
Instances For
Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity strong natural transformation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Vertical composition of strong natural transformations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.