The bicategory of based categories #
In this file we define the type BasedCategory 𝒮
, and give it the structure of a strict
bicategory. Given a category 𝒮
, we define the type BasedCategory 𝒮
as the type of categories
𝒳
equipped with a functor 𝒳.p : 𝒳 ⥤ 𝒮
.
We also define a type of functors between based categories 𝒳
and 𝒴
, which we call
BasedFunctor 𝒳 𝒴
and denote as 𝒳 ⥤ᵇ 𝒴
. These are defined as functors between the underlying
categories 𝒳.obj
and 𝒴.obj
which commute with the projections to 𝒮
.
Natural transformations between based functors F G : 𝒳 ⥤ᵇ 𝒴
are given by the structure
BasedNatTrans F G
. These are defined as natural transformations α
between the functors
underlying F
and G
such that α.app a
lifts 𝟙 S
whenever 𝒳.p.obj a = S
.
A based category over 𝒮
is a category 𝒳
together with a functor p : 𝒳 ⥤ 𝒮
.
- obj : Type u₂
The type of objects in a
BasedCategory
- category : CategoryTheory.Category.{v₂, u₂} self.obj
The underlying category of a
BasedCategory
. - p : CategoryTheory.Functor self.obj 𝒮
The functor to the base.
Instances For
Equations
- CategoryTheory.instCategoryObj 𝒳 = 𝒳.category
The based category associated to a functor p : 𝒳 ⥤ 𝒮
.
Equations
- CategoryTheory.BasedCategory.ofFunctor p = { obj := 𝒳, category := inferInstance, p := p }
Instances For
A functor between based categories is a functor between the underlying categories that commutes with the projections.
- obj : 𝒳.obj → 𝒴.obj
- map_id : ∀ (X : 𝒳.obj), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
- map_comp : ∀ {X Y Z : 𝒳.obj} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
- w : self.comp 𝒴.p = 𝒳.p
Instances For
Notation for BasedFunctor
.
Equations
- CategoryTheory.«term_⥤ᵇ_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_⥤ᵇ_ 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ᵇ ") (Lean.ParserDescr.cat `term 26))
Instances For
The identity based functor.
Equations
- CategoryTheory.BasedFunctor.id 𝒳 = { toFunctor := CategoryTheory.Functor.id 𝒳.obj, w := ⋯ }
Instances For
Notation for the identity functor on a based category.
Equations
- CategoryTheory.BasedFunctor.«term𝟭» = Lean.ParserDescr.node `CategoryTheory.BasedFunctor.term𝟭 1024 (Lean.ParserDescr.symbol "𝟭")
Instances For
The composition of two based functors.
Equations
- F.comp G = { toFunctor := F.comp G.toFunctor, w := ⋯ }
Instances For
Notation for composition of based functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
For a based functor F : 𝒳 ⟶ 𝒴
, then whenever an arrow φ
in 𝒳
lifts some f
in 𝒮
,
then F(φ)
also lifts f
.
Equations
- ⋯ = ⋯
For a based functor F : 𝒳 ⟶ 𝒴
, and an arrow φ
in 𝒳
, then φ
lifts an arrow f
in 𝒮
if F(φ)
does.
A BasedNatTrans
between two BasedFunctor
s is a natural transformation α
between the
underlying functors, such that for all a : 𝒳
, α.app a
lifts 𝟙 S
whenever 𝒳.p.obj a = S
.
- app : (X : 𝒳.obj) → F.obj X ⟶ G.obj X
- naturality : ∀ ⦃X Y : 𝒳.obj⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
- isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (self.app a)
Instances For
Equations
- ⋯ = ⋯
The identity natural transformation is a BasedNatTrans
.
Equations
- CategoryTheory.BasedNatTrans.id F = { toNatTrans := CategoryTheory.NatTrans.id F.toFunctor, isHomLift' := ⋯ }
Instances For
Composition of BasedNatTrans
, given by composition of the underlying natural
transformations.
Equations
- α.comp β = { toNatTrans := α.vcomp β.toNatTrans, isHomLift' := ⋯ }
Instances For
Equations
The forgetful functor from the category of based functors 𝒳 ⥤ᵇ 𝒴
to the category of
functors of underlying categories, 𝒳.obj ⥤ 𝒴.obj
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The identity natural transformation is a based natural isomorphism.
Equations
- CategoryTheory.BasedNatIso.id F = { hom := CategoryTheory.CategoryStruct.id F, inv := CategoryTheory.CategoryStruct.id F, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
The inverse of a based natural transformation whose underlying natural transformation is an isomorphism.
Equations
- CategoryTheory.BasedNatIso.mkNatIso α isHomLift' = { hom := { toNatTrans := α.hom, isHomLift' := ⋯ }, inv := { toNatTrans := α.inv, isHomLift' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Left-whiskering in the bicategory BasedCategory
is given by whiskering the underlying functors
and natural transformations.
Equations
- CategoryTheory.BasedCategory.whiskerLeft F α = { toNatTrans := CategoryTheory.whiskerLeft F.toFunctor α.toNatTrans, isHomLift' := ⋯ }
Instances For
Right-whiskering in the bicategory BasedCategory
is given by whiskering the underlying
functors and natural transformations.
Equations
- CategoryTheory.BasedCategory.whiskerRight α H = { toNatTrans := CategoryTheory.whiskerRight α.toNatTrans H.toFunctor, isHomLift' := ⋯ }
Instances For
The category of based categories.
Equations
- CategoryTheory.BasedCategory.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
The bicategory of based categories.
Equations
- One or more equations did not get rendered due to their size.
The bicategory structure on BasedCategory.{v₂, u₂} 𝒮
is strict.
Equations
- ⋯ = ⋯