Documentation

Mathlib.CategoryTheory.Bicategory.LocallyDiscrete

Locally discrete bicategories #

A category C can be promoted to a strict bicategory LocallyDiscrete C. The objects and the 1-morphisms in LocallyDiscrete C are the same as the objects and the morphisms, respectively, in C, and the 2-morphisms in LocallyDiscrete C are the equalities between 1-morphisms. In other words, the category consisting of the 1-morphisms between each pair of objects X and Y in LocallyDiscrete C is defined as the discrete category associated with the type X ⟶ Y.

source
def CategoryTheory.LocallyDiscrete (C : Type u) :
Type u

A type synonym for promoting any type to a category, with the only morphisms being equalities.

Equations
Instances For
    source
    instance CategoryTheory.LocallyDiscrete.instInhabitedLocallyDiscrete {C : Type u} [Inhabited C] :
    Inhabited (CategoryTheory.LocallyDiscrete C)
    Equations
    • CategoryTheory.LocallyDiscrete.instInhabitedLocallyDiscrete = { default := default }
    source
    instance CategoryTheory.LocallyDiscrete.instCategoryStructLocallyDiscrete {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] :
    CategoryTheory.CategoryStruct.{v, u} (CategoryTheory.LocallyDiscrete C)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.LocallyDiscrete.homSmallCategory {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : CategoryTheory.LocallyDiscrete C) (Y : CategoryTheory.LocallyDiscrete C) :
    CategoryTheory.SmallCategory (X ⟶ Y)
    Equations
    source
    instance CategoryTheory.LocallyDiscrete.subsingleton2Hom {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : CategoryTheory.LocallyDiscrete C} {Y : CategoryTheory.LocallyDiscrete C} (f : X ⟶ Y) (g : X ⟶ Y) :
    Subsingleton (f ⟶ g)
    Equations
    • ⋯ = ⋯
    source
    theorem CategoryTheory.LocallyDiscrete.eq_of_hom {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : CategoryTheory.LocallyDiscrete C} {Y : CategoryTheory.LocallyDiscrete C} {f : X ⟶ Y} {g : X ⟶ Y} (η : f ⟶ g) :
    f = g

    Extract the equation from a 2-morphism in a locally discrete 2-category.

    source
    instance CategoryTheory.locallyDiscreteBicategory (C : Type u) [CategoryTheory.Category.{v, u} C] :
    CategoryTheory.Bicategory (CategoryTheory.LocallyDiscrete C)

    The locally discrete bicategory on a category is a bicategory in which the objects and the 1-morphisms are the same as those in the underlying category, and the 2-morphisms are the equalities between 1-morphisms.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.locallyDiscreteBicategory.strict (C : Type u) [CategoryTheory.Category.{v, u} C] :
    CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C)

    A locally discrete bicategory is strict.

    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.toOplaxFunctor_mapComp {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    ∀ {a b c : CategoryTheory.LocallyDiscrete I} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Functor.toOplaxFunctor F).mapComp f g = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_map₂ {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    ∀ {a b : CategoryTheory.LocallyDiscrete I} {f g : a ⟶ b} (η : f ⟶ g), (CategoryTheory.Functor.toOplaxFunctor F).map₂ η = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.toOplaxFunctor_mapId {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (i : CategoryTheory.LocallyDiscrete I) :
    (CategoryTheory.Functor.toOplaxFunctor F).mapId i = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_map {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    ∀ {X Y : CategoryTheory.LocallyDiscrete I} (f : X ⟶ Y), (CategoryTheory.Functor.toOplaxFunctor F).map f = F.map f.as
    source
    @[simp]
    theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrefunctor_obj {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    ∀ (a : I), (CategoryTheory.Functor.toOplaxFunctor F).obj a = F.obj a
    source
    def CategoryTheory.Functor.toOplaxFunctor {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
    CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete I) B

    If B is a strict bicategory and I is a (1-)category, any functor (of 1-categories) I ⥤ B can be promoted to an oplax functor from LocallyDiscrete I to B.

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