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.

structure CategoryTheory.BasedCategory (𝒮 : Type u₁) [Category.{v₁, u₁} 𝒮] : Type (max (max (max u₁ (u₂ + 1)) v₁) (v₂ + 1))

A based category over 𝒮 is a category 𝒳 together with a functor p : 𝒳 ⥤ 𝒮.

• obj : Type u₂

  The type of objects in a BasedCategory

• category : Category.{v₂, u₂} self.obj

  The underlying category of a BasedCategory.

• p : Functor self.obj 𝒮

  The functor to the base.

instance CategoryTheory.instCategoryObj {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) : Category.{v₂, u₂} 𝒳.obj

Equations

• CategoryTheory.instCategoryObj 𝒳 = 𝒳.category

def CategoryTheory.BasedCategory.ofFunctor {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : Type u₂} [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) : BasedCategory 𝒮

The based category associated to a functor p : 𝒳 ⥤ 𝒮.

Equations

• CategoryTheory.BasedCategory.ofFunctor p = { obj := 𝒳, category := inferInstance, p := p }

structure CategoryTheory.BasedFunctor {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) extends CategoryTheory.Functor 𝒳.obj 𝒴.obj : Type (max (max (max u₂ u₃) v₂) v₃)

A functor between based categories is a functor between the underlying categories that commutes with the projections.

• obj : 𝒳.obj → 𝒴.obj
• map {X Y : 𝒳.obj} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : 𝒳.obj) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
• map_comp {X Y Z : 𝒳.obj} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
• w : self.comp 𝒴.p = 𝒳.p

def CategoryTheory.«term_⥤ᵇ_» : Lean.TrailingParserDescr

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))

def CategoryTheory.BasedFunctor.id {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) : BasedFunctor 𝒳 𝒳

The identity based functor.

Equations

• CategoryTheory.BasedFunctor.id 𝒳 = { toFunctor := CategoryTheory.Functor.id 𝒳.obj, w := ⋯ }

@[simp]

theorem CategoryTheory.BasedFunctor.id_toFunctor {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) : (id 𝒳).toFunctor = Functor.id 𝒳.obj

def CategoryTheory.BasedFunctor.«term𝟭» : Lean.ParserDescr

Notation for the identity functor on a based category.

Equations

• CategoryTheory.BasedFunctor.«term𝟭» = Lean.ParserDescr.node `CategoryTheory.BasedFunctor.«term𝟭» 1024 (Lean.ParserDescr.symbol "𝟭")

def CategoryTheory.BasedFunctor.comp {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) (G : BasedFunctor 𝒴 𝒵) : BasedFunctor 𝒳 𝒵

The composition of two based functors.

Equations

• F.comp G = { toFunctor := F.comp G.toFunctor, w := ⋯ }

@[simp]

theorem CategoryTheory.BasedFunctor.comp_toFunctor {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) (G : BasedFunctor 𝒴 𝒵) : (F.comp G).toFunctor = F.comp G.toFunctor

def CategoryTheory.BasedFunctor.«term_⋙_» : Lean.TrailingParserDescr

Notation for composition of based functors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.BasedFunctor.comp_id {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : F.comp (id 𝒴) = F

@[simp]

theorem CategoryTheory.BasedFunctor.id_comp {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : (id 𝒳).comp F = F

@[simp]

theorem CategoryTheory.BasedFunctor.comp_assoc {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} {𝒜 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) (G : BasedFunctor 𝒴 𝒵) (H : BasedFunctor 𝒵 𝒜) : (F.comp G).comp H = F.comp (G.comp H)

@[simp]

theorem CategoryTheory.BasedFunctor.w_obj {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) (a : 𝒳.obj) : 𝒴.p.obj (F.obj a) = 𝒳.p.obj a

instance CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) (a : 𝒳.obj) : 𝒴.p.IsHomLift (CategoryStruct.id (𝒳.p.obj a)) (CategoryStruct.id (F.obj a))

instance CategoryTheory.BasedFunctor.preserves_isHomLift {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S) (φ : a ⟶ b) [𝒳.p.IsHomLift f φ] : 𝒴.p.IsHomLift f (F.map φ)

For a based functor F : 𝒳 ⟶ 𝒴, then whenever an arrow φ in 𝒳 lifts some f in 𝒮, then F(φ) also lifts f.

theorem CategoryTheory.BasedFunctor.isHomLift_map {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S) (φ : a ⟶ b) [𝒴.p.IsHomLift f (F.map φ)] : 𝒳.p.IsHomLift f φ

For a based functor F : 𝒳 ⟶ 𝒴, and an arrow φ in 𝒳, then φ lifts an arrow f in 𝒮 if F(φ) does.

theorem CategoryTheory.BasedFunctor.isHomLift_iff {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S) (φ : a ⟶ b) : 𝒴.p.IsHomLift f (F.map φ) ↔ 𝒳.p.IsHomLift f φ

structure CategoryTheory.BasedNatTrans {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F G : BasedFunctor 𝒳 𝒴) extends CategoryTheory.NatTrans F.toFunctor G.toFunctor : Type (max u₂ v₃)

A BasedNatTrans between two BasedFunctors 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) : CategoryStruct.comp (F.map f) (self.app Y) = CategoryStruct.comp (self.app X) (G.map f)
• isHomLift' (a : 𝒳.obj) : 𝒴.p.IsHomLift (CategoryStruct.id (𝒳.p.obj a)) (self.app a)

theorem CategoryTheory.BasedNatTrans.ext {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α β : BasedNatTrans F G) (h : α.toNatTrans = β.toNatTrans) : α = β

theorem CategoryTheory.BasedNatTrans.ext_iff {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} {α β : BasedNatTrans F G} : α = β ↔ α.toNatTrans = β.toNatTrans

instance CategoryTheory.BasedNatTrans.app_isHomLift {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : BasedNatTrans F G) (a : 𝒳.obj) : 𝒴.p.IsHomLift (CategoryStruct.id (𝒳.p.obj a)) (α.app a)

theorem CategoryTheory.BasedNatTrans.isHomLift {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : BasedNatTrans F G) {a : 𝒳.obj} {S : 𝒮} (ha : 𝒳.p.obj a = S) : 𝒴.p.IsHomLift (CategoryStruct.id S) (α.app a)

def CategoryTheory.BasedNatTrans.id {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : BasedNatTrans F F

The identity natural transformation is a BasedNatTrans.

Equations

• CategoryTheory.BasedNatTrans.id F = { toNatTrans := CategoryTheory.NatTrans.id F.toFunctor, isHomLift' := ⋯ }

@[simp]

theorem CategoryTheory.BasedNatTrans.id_toNatTrans {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : (id F).toNatTrans = NatTrans.id F.toFunctor

def CategoryTheory.BasedNatTrans.comp {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G H : BasedFunctor 𝒳 𝒴} (α : BasedNatTrans F G) (β : BasedNatTrans G H) : BasedNatTrans F H

Composition of BasedNatTrans, given by composition of the underlying natural transformations.

Equations

• α.comp β = { toNatTrans := α.vcomp β.toNatTrans, isHomLift' := ⋯ }

@[simp]

theorem CategoryTheory.BasedNatTrans.comp_toNatTrans {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G H : BasedFunctor 𝒳 𝒴} (α : BasedNatTrans F G) (β : BasedNatTrans G H) : (α.comp β).toNatTrans = α.vcomp β.toNatTrans

instance CategoryTheory.BasedNatTrans.homCategory {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) : Category.{max u₂ v₃, max (max (max u₂ v₂) u₃) v₃} (BasedFunctor 𝒳 𝒴)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.BasedNatTrans.homCategory_id {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) (F : BasedFunctor 𝒳 𝒴) : CategoryStruct.id F = id F

@[simp]

theorem CategoryTheory.BasedNatTrans.homCategory_comp {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) {X✝ Y✝ Z✝ : BasedFunctor 𝒳 𝒴} (α : BasedNatTrans X✝ Y✝) (β : BasedNatTrans Y✝ Z✝) : CategoryStruct.comp α β = α.comp β

theorem CategoryTheory.BasedNatTrans.homCategory.ext {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α β : F ⟶ G) (h : α.toNatTrans = β.toNatTrans) : α = β

theorem CategoryTheory.BasedNatTrans.homCategory.ext_iff {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} {α β : F ⟶ G} : α = β ↔ α.toNatTrans = β.toNatTrans

def CategoryTheory.BasedNatTrans.forgetful {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) : Functor (BasedFunctor 𝒳 𝒴) (Functor 𝒳.obj 𝒴.obj)

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.

@[simp]

theorem CategoryTheory.BasedNatTrans.forgetful_map {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) {X✝ Y✝ : BasedFunctor 𝒳 𝒴} (α : X✝ ⟶ Y✝) : (forgetful 𝒳 𝒴).map α = α.toNatTrans

@[simp]

theorem CategoryTheory.BasedNatTrans.forgetful_obj {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) (𝒴 : BasedCategory 𝒮) (F : BasedFunctor 𝒳 𝒴) : (forgetful 𝒳 𝒴).obj F = F.toFunctor

instance CategoryTheory.BasedNatTrans.instReflectsIsomorphismsBasedFunctorFunctorObjForgetful {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} : (forgetful 𝒳 𝒴).ReflectsIsomorphisms

instance CategoryTheory.BasedNatTrans.instIsIsoFunctorObjOfBasedFunctor {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : F ⟶ G) [IsIso α] : IsIso α.toNatTrans

def CategoryTheory.BasedNatIso.id {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : F ≅ F

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 := ⋯ }

@[simp]

theorem CategoryTheory.BasedNatIso.id_inv {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : (id F).inv = CategoryStruct.id F

@[simp]

theorem CategoryTheory.BasedNatIso.id_hom {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) : (id F).hom = CategoryStruct.id F

def CategoryTheory.BasedNatIso.mkNatIso {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : F.toFunctor ≅ G.toFunctor) (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (CategoryStruct.id (𝒳.p.obj a)) (α.hom.app a)) : F ≅ G

The inverse of a based natural transformation whose underlying natural transformation is an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.BasedNatIso.isIso_of_toNatTrans_isIso {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : F ⟶ G) [IsIso α.toNatTrans] : IsIso α

def CategoryTheory.BasedCategory.whiskerLeft {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) {G H : BasedFunctor 𝒴 𝒵} (α : G ⟶ H) : F.comp G ⟶ F.comp H

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' := ⋯ }

@[simp]

theorem CategoryTheory.BasedCategory.whiskerLeft_toNatTrans {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} (F : BasedFunctor 𝒳 𝒴) {G H : BasedFunctor 𝒴 𝒵} (α : G ⟶ H) : (whiskerLeft F α).toNatTrans = CategoryTheory.whiskerLeft F.toFunctor α.toNatTrans

def CategoryTheory.BasedCategory.whiskerRight {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : F ⟶ G) (H : BasedFunctor 𝒴 𝒵) : F.comp H ⟶ G.comp H

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' := ⋯ }

@[simp]

theorem CategoryTheory.BasedCategory.whiskerRight_toNatTrans {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {𝒳 : BasedCategory 𝒮} {𝒴 : BasedCategory 𝒮} {𝒵 : BasedCategory 𝒮} {F G : BasedFunctor 𝒳 𝒴} (α : F ⟶ G) (H : BasedFunctor 𝒴 𝒵) : (whiskerRight α H).toNatTrans = CategoryTheory.whiskerRight α.toNatTrans H.toFunctor

instance CategoryTheory.BasedCategory.instCategory {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] : Category.{max u₂ v₂, max (max (max (u₂ + 1) (v₂ + 1)) u₁) v₁} (BasedCategory 𝒮)

The category of based categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.BasedCategory.id_def {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (𝒳 : BasedCategory 𝒮) : CategoryStruct.id 𝒳 = BasedFunctor.id 𝒳

@[simp]

theorem CategoryTheory.BasedCategory.comp_def {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {X✝ Y✝ Z✝ : BasedCategory 𝒮} (F : BasedFunctor X✝ Y✝) (G : BasedFunctor Y✝ Z✝) : CategoryStruct.comp F G = F.comp G

instance CategoryTheory.BasedCategory.bicategory {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] : Bicategory (BasedCategory 𝒮)

The bicategory of based categories.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.BasedCategory.instStrict {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] : Bicategory.Strict (BasedCategory 𝒮)

The bicategory structure on BasedCategory.{v₂, u₂} 𝒮 is strict.