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 𝒳 equiped 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₁) [CategoryTheory.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 : CategoryTheory.Category.{v₂, u₂} self.obj

  The underlying category of a BasedCategory.

• p : CategoryTheory.Functor self.obj 𝒮

  The functor to the base.

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

Equations

• CategoryTheory.instCategoryObj 𝒳 = 𝒳.category

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

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

Equations

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

structure CategoryTheory.BasedFunctor {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮) (𝒴 : CategoryTheory.BasedCategory 𝒮) extends CategoryTheory.Functor : 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 (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

theorem CategoryTheory.BasedFunctor.w {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (self : CategoryTheory.BasedFunctor 𝒳 𝒴) : 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))

@[simp]

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

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

The identity based functor.

Equations

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

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

@[simp]

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

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

The composition of two based functors.

Equations

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

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₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) : F.comp (CategoryTheory.BasedFunctor.id 𝒴) = F

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.BasedFunctor.preserves_isHomLift {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R : 𝒮} {S : 𝒮} {a : 𝒳.obj} {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.

Equations

• ⋯ = ⋯

theorem CategoryTheory.BasedFunctor.isHomLift_map {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R : 𝒮} {S : 𝒮} {a : 𝒳.obj} {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₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R : 𝒮} {S : 𝒮} {a : 𝒳.obj} {b : 𝒳.obj} (f : R ⟶ S) (φ : a ⟶ b) : 𝒴.p.IsHomLift f (F.map φ) ↔ 𝒳.p.IsHomLift f φ

structure CategoryTheory.BasedNatTrans {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) (G : CategoryTheory.BasedFunctor 𝒳 𝒴) extends CategoryTheory.NatTrans : 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), 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)

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

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

def CategoryTheory.BasedNatTrans.id {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) : CategoryTheory.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.comp_toNatTrans {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} {F : CategoryTheory.BasedFunctor 𝒳 𝒴} {G : CategoryTheory.BasedFunctor 𝒳 𝒴} {H : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans F G) (β : CategoryTheory.BasedNatTrans G H) : (α.comp β).toNatTrans = α.vcomp β.toNatTrans

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.BasedNatTrans.homCategory 𝒳 𝒴 = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

@[simp]

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

@[simp]

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

def CategoryTheory.BasedNatTrans.forgetful {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮) (𝒴 : CategoryTheory.BasedCategory 𝒮) : CategoryTheory.Functor (CategoryTheory.BasedFunctor 𝒳 𝒴) (CategoryTheory.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.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.BasedNatIso.id {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.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 := ⋯ }

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

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

Equations

• CategoryTheory.BasedNatIso.mkNatIso α isHomLift' = { hom := { toNatTrans := α.hom, isHomLift' := ⋯ }, inv := { toNatTrans := α.inv, isHomLift' := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

@[simp]

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

def CategoryTheory.BasedCategory.whiskerLeft {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {G : CategoryTheory.BasedFunctor 𝒴 𝒵} {H : CategoryTheory.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.whiskerRight_toNatTrans {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} {F : CategoryTheory.BasedFunctor 𝒳 𝒴} {G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : F ⟶ G) (H : CategoryTheory.BasedFunctor 𝒴 𝒵) : (CategoryTheory.BasedCategory.whiskerRight α H).toNatTrans = CategoryTheory.whiskerRight α.toNatTrans H.toFunctor

def CategoryTheory.BasedCategory.whiskerRight {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} {F : CategoryTheory.BasedFunctor 𝒳 𝒴} {G : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : F ⟶ G) (H : CategoryTheory.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.instCategory_comp {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] : ∀ {X Y Z : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor X Y) (G : CategoryTheory.BasedFunctor Y Z), CategoryTheory.CategoryStruct.comp F G = F.comp G

@[simp]

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

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

The category of based categories.

Equations

• CategoryTheory.BasedCategory.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.BasedCategory.bicategory {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] : CategoryTheory.Bicategory (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] : CategoryTheory.Bicategory.Strict (CategoryTheory.BasedCategory 𝒮)

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

Equations

• ⋯ = ⋯