Oplax functors #
An oplax functor F
between bicategories B
and C
consists of
- a function between objects
F.obj : B ⟶ C
, - a family of functions between 1-morphisms
F.map : (a ⟶ b) → (F.obj a ⟶ F.obj b)
, - a family of functions between 2-morphisms
F.map₂ : (f ⟶ g) → (F.map f ⟶ F.map g)
, - a family of 2-morphisms
F.mapId a : F.map (𝟙 a) ⟶ 𝟙 (F.obj a)
, - a family of 2-morphisms
F.mapComp f g : F.map (f ≫ g) ⟶ F.map f ≫ F.map g
, and - certain consistency conditions on them.
Main definitions #
CategoryTheory.OplaxFunctor B C
: an oplax functor between bicategoriesB
andC
CategoryTheory.OplaxFunctor.comp F G
: the composition of oplax functors
Future work #
There are two types of functors between bicategories, called lax and oplax functors, depending on
the directions of mapId
and mapComp
. We may need both in mathlib in the future, but for
now we only define oplax functors.
A prelax functor between bicategories consists of functions between objects,
1-morphisms, and 2-morphisms. This structure will be extended to define OplaxFunctor
.
- obj : B → C
The action of a prelax functor on 2-morphisms.
Instances For
Equations
- CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor = { coe := CategoryTheory.PrelaxFunctor.toPrefunctor }
The identity prelax functor.
Equations
- CategoryTheory.PrelaxFunctor.id B = let __src := 𝟭q B; { toPrefunctor := __src, map₂ := fun {a b : B} {f g : a ⟶ b} (η : f ⟶ g) => η }
Instances For
Equations
- CategoryTheory.PrelaxFunctor.instInhabited = { default := CategoryTheory.PrelaxFunctor.id B }
Composition of prelax functors.
Equations
Instances For
An oplax functor F
between bicategories B
and C
consists of a function between objects
F.obj
, a function between 1-morphisms F.map
, and a function between 2-morphisms F.map₂
.
Unlike functors between categories, F.map
do not need to strictly commute with the composition,
and do not need to strictly preserve the identity. Instead, there are specified 2-morphisms
F.map (𝟙 a) ⟶ 𝟙 (F.obj a)
and F.map (f ≫ g) ⟶ F.map f ≫ F.map g
.
F.map₂
strictly commute with compositions and preserve the identity. They also preserve the
associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains
of 2-morphisms.
- obj : B → C
- mapId : (a : B) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).obj a)
- mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → (↑self.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g)
- mapComp_naturality_left : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) ((↑self.toPrelaxFunctor).map g))
- mapComp_naturality_right : ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (self.mapComp f g') = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.map₂ η))
- map₂_id : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id ((↑self.toPrelaxFunctor).map f)
- map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
- map₂_associator : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) ((↑self.toPrelaxFunctor).map h)) (CategoryTheory.Bicategory.associator ((↑self.toPrelaxFunctor).map f) ((↑self.toPrelaxFunctor).map g) ((↑self.toPrelaxFunctor).map h)).hom)
- map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) ((↑self.toPrelaxFunctor).map f)) (CategoryTheory.Bicategory.leftUnitor ((↑self.toPrelaxFunctor).map f)).hom)
- map₂_rightUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((↑self.toPrelaxFunctor).map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor ((↑self.toPrelaxFunctor).map f)).hom)
Instances For
Equations
- CategoryTheory.OplaxFunctor.hasCoeToPrelax = { coe := CategoryTheory.OplaxFunctor.toPrelaxFunctor }
Function between 1-morphisms as a functor.
Equations
Instances For
An oplax functor F : B ⥤ C
sends 2-isomorphisms η : f ≅ f
to 2-isomorphisms
F.map f ≅ F.map g
Equations
- F.map₂Iso η = (F.mapFunctor a b).mapIso η
Instances For
Equations
- ⋯ = ⋯
The identity oplax functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.OplaxFunctor.instInhabited = { default := CategoryTheory.OplaxFunctor.id B }
Composition of oplax functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A structure on an oplax functor that promotes an oplax functor to a pseudofunctor.
See Pseudofunctor.mkOfOplax
.
- mapIdIso : (a : B) → (↑F.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id ((↑F.toPrelaxFunctor).obj a)
- mapCompIso : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → (↑F.toPrelaxFunctor).map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp ((↑F.toPrelaxFunctor).map f) ((↑F.toPrelaxFunctor).map g)
- mapIdIso_hom : ∀ {a : B}, (self.mapIdIso a).hom = F.mapId a