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
theorem CategoryTheory.LocallyDiscrete.ext_iff {C : Type u} (x : CategoryTheory.LocallyDiscrete C) (y : CategoryTheory.LocallyDiscrete C) :
x = y ↔ x.as = y.as
source
theorem CategoryTheory.LocallyDiscrete.ext {C : Type u} (x : CategoryTheory.LocallyDiscrete C) (y : CategoryTheory.LocallyDiscrete C) (as : x.as = y.as) :
x = y
source
structure CategoryTheory.LocallyDiscrete (C : Type u) :
Type u

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
    source
    @[simp]
    theorem CategoryTheory.LocallyDiscrete.mk_as {C : Type u} (a : CategoryTheory.LocallyDiscrete C) :
    { as := a.as } = a
    source
    @[simp]
    theorem CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_apply {C : Type u} (self : CategoryTheory.LocallyDiscrete C) :
    CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv self = self.as
    source
    @[simp]
    theorem CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as {C : Type u} (as : C) :
    (CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.symm as).as = as
    source
    def CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv {C : Type u} :
    CategoryTheory.LocallyDiscrete C ≃ C

    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
      source
      instance CategoryTheory.LocallyDiscrete.instDecidableEq {C : Type u} [DecidableEq C] :
      DecidableEq (CategoryTheory.LocallyDiscrete C)
      Equations
      • CategoryTheory.LocallyDiscrete.instDecidableEq = CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.decidableEq
      source
      instance CategoryTheory.LocallyDiscrete.instInhabited {C : Type u} [Inhabited C] :
      Inhabited (CategoryTheory.LocallyDiscrete C)
      Equations
      • CategoryTheory.LocallyDiscrete.instInhabited = { default := { as := default } }
      source
      instance CategoryTheory.LocallyDiscrete.categoryStruct {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
      @[simp]
      theorem CategoryTheory.LocallyDiscrete.id_as {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : CategoryTheory.LocallyDiscrete C) :
      (CategoryTheory.CategoryStruct.id a).as = CategoryTheory.CategoryStruct.id a.as
      source
      @[simp]
      theorem CategoryTheory.LocallyDiscrete.comp_as {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a : CategoryTheory.LocallyDiscrete C} {b : CategoryTheory.LocallyDiscrete C} {c : CategoryTheory.LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) :
      (CategoryTheory.CategoryStruct.comp f g).as = CategoryTheory.CategoryStruct.comp f.as g.as
      source
      @[instance 900]
      instance CategoryTheory.LocallyDiscrete.homSmallCategory {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : CategoryTheory.LocallyDiscrete C) (b : CategoryTheory.LocallyDiscrete C) :
      CategoryTheory.SmallCategory (a ⟶ b)
      Equations
      source
      instance CategoryTheory.LocallyDiscrete.subsingleton2Hom {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {a : CategoryTheory.LocallyDiscrete C} {b : CategoryTheory.LocallyDiscrete C} (f : a ⟶ b) (g : a ⟶ b) :
      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.toPseudoFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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), F.toPseudoFunctor.map₂ η = CategoryTheory.eqToHom ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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) (i : CategoryTheory.LocallyDiscrete I) :
      F.toPseudoFunctor.obj i = F.obj i.as
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_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) :
      F.toPseudoFunctor.mapId i = CategoryTheory.eqToIso ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_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), F.toPseudoFunctor.mapComp f g = CategoryTheory.eqToIso ⋯
      source
      @[simp]
      theorem CategoryTheory.Functor.toPseudoFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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), F.toPseudoFunctor.map f = F.map f.as
      source
      def CategoryTheory.Functor.toPseudoFunctor {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] {B : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) :
      CategoryTheory.Pseudofunctor (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 a pseudofunctor from LocallyDiscrete I to B.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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), F.toOplaxFunctor.map₂ η = CategoryTheory.eqToHom ⋯
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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) (i : CategoryTheory.LocallyDiscrete I) :
        F.toOplaxFunctor.obj i = F.obj i.as
        source
        @[simp]
        theorem CategoryTheory.Functor.toOplaxFunctor_toPrelaxFunctor_toPrelaxFunctorStruct_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), F.toOplaxFunctor.map f = F.map f.as
        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), F.toOplaxFunctor.mapComp f g = 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) :
        F.toOplaxFunctor.mapId i = CategoryTheory.eqToHom ⋯
        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
          source
          @[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) :
          F.map₂ (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
          source
          @[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
          source
          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
            source
            @[simp]
            theorem Quiver.Hom.id_toLoc {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (a : C) :
            (CategoryTheory.CategoryStruct.id a).toLoc = CategoryTheory.CategoryStruct.id { as := a }
            source
            @[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) :
            (CategoryTheory.CategoryStruct.comp f g).toLoc = CategoryTheory.CategoryStruct.comp f.toLoc g.toLoc
            source
            @[simp]
            theorem CategoryTheory.LocallyDiscrete.eqToHom_toLoc {C : Type u} [CategoryTheory.Category.{v, u} C] {a : C} {b : C} (h : a = b) :
            (CategoryTheory.eqToHom h).toLoc = CategoryTheory.eqToHom ⋯