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.

A wrapper for promoting any category to a bicategory, with the only 2-morphisms being equalities.

  • as : C

    A wrapper for promoting any category to a bicategory, with the only 2-morphisms being equalities.

Instances For
    @[simp]
    @[simp]
    theorem CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_apply {C : Type u} (self : CategoryTheory.LocallyDiscrete C) :
    CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv self = self.as
    @[simp]
    theorem CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as {C : Type u} (as : C) :
    (CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.symm as).as = as

    LocallyDiscrete C is equivalent to the original type C.

    Equations
    • CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv = { toFun := CategoryTheory.LocallyDiscrete.as, invFun := CategoryTheory.LocallyDiscrete.mk, left_inv := , right_inv := }
    Instances For
      Equations
      • CategoryTheory.LocallyDiscrete.instDecidableEq = CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.decidableEq
      Equations
      • CategoryTheory.LocallyDiscrete.instInhabited = { default := { as := default } }

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

      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.

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

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

        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
          @[simp]
          theorem CategoryTheory.PrelaxFunctor.map₂_eqToHom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {a : B} {b : B} {f : a b} {g : a b} (h : f = g) :
          @[simp]
          theorem Quiver.Hom.toLoc_as {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a : C} {b : C} (f : a b) :
          f.toLoc.as = f
          def Quiver.Hom.toLoc {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a : C} {b : C} (f : a b) :
          { as := a } { as := b }

          The 1-morphism in LocallyDiscrete C associated to a given morphism f : a ⟶ b in C

          Equations
          • f.toLoc = { as := f }
          Instances For
            @[simp]
            theorem Quiver.Hom.comp_toLoc {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a : C} {b : C} {c : C} (f : a b) (g : b c) :