Documentation

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

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₁) [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 : 𝒳 ⥤ 𝒮.

Instances For

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

    Equations
    Instances For
      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.

      Instances For
        theorem CategoryTheory.BasedFunctor.w {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} (self : CategoryTheory.BasedFunctor 𝒳 𝒴) :
        self.comp 𝒴.p = 𝒳.p

        The identity based functor.

        Equations
        Instances For

          Notation for the identity functor on a based category.

          Equations
          Instances For
            @[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

            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
                @[simp]
                @[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.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 φ

                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.

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

                  The identity natural transformation is a BasedNatTrans.

                  Equations
                  Instances For
                    @[simp]

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

                    Equations
                    • α.comp β = { toNatTrans := α.vcomp β.toNatTrans, isHomLift' := }
                    Instances For
                      theorem CategoryTheory.BasedNatTrans.homCategory.ext_iff {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮} {𝒴 : CategoryTheory.BasedCategory 𝒮} {F : CategoryTheory.BasedFunctor 𝒳 𝒴} {G : CategoryTheory.BasedFunctor 𝒳 𝒴} {α : F G} {β : F G} :
                      α = β α.toNatTrans = β.toNatTrans
                      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) :
                      α = β

                      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

                        The identity natural transformation is a based natural isomorphism.

                        Equations
                        Instances For
                          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 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
                            Instances For

                              Right-whiskering in the bicategory BasedCategory is given by whiskering the underlying functors and natural transformations.

                              Equations
                              Instances For

                                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
                                • =