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.

theorem CategoryTheory.LocallyDiscrete.ext_iff {C : Type u} {x : CategoryTheory.LocallyDiscrete C} {y : CategoryTheory.LocallyDiscrete C} : x = y ↔ x.as = y.as

theorem CategoryTheory.LocallyDiscrete.ext {C : Type u} {x : CategoryTheory.LocallyDiscrete C} {y : CategoryTheory.LocallyDiscrete C} (as : x.as = y.as) : x = y

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.

@[simp]

theorem CategoryTheory.LocallyDiscrete.mk_as {C : Type u} (a : CategoryTheory.LocallyDiscrete C) : { as := a.as } = a

@[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

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 := ⋯ }

instance CategoryTheory.LocallyDiscrete.instDecidableEq {C : Type u} [DecidableEq C] : DecidableEq (CategoryTheory.LocallyDiscrete C)

Equations

• CategoryTheory.LocallyDiscrete.instDecidableEq = CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv.decidableEq

instance CategoryTheory.LocallyDiscrete.instInhabited {C : Type u} [Inhabited C] : Inhabited (CategoryTheory.LocallyDiscrete C)

Equations

• CategoryTheory.LocallyDiscrete.instInhabited = { default := { as := default } }

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.

@[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

@[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

@[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

• a.homSmallCategory b = CategoryTheory.discreteCategory (a.as ⟶ b.as)

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

• ⋯ = ⋯

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.

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.

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

• ⋯ = ⋯

@[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 ⋯

@[reducible, inline]

abbrev CategoryTheory.Bicategory.IsLocallyDiscrete (B : Type u_1) [CategoryTheory.Bicategory B] : Prop

A bicategory is locally discrete if the categories of 1-morphisms are discrete.

Equations

• CategoryTheory.Bicategory.IsLocallyDiscrete B = ∀ (b c : B), CategoryTheory.IsDiscrete (b ⟶ c)

instance CategoryTheory.Bicategory.instIsLocallyDiscreteLocallyDiscrete (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.Bicategory.IsLocallyDiscrete (CategoryTheory.LocallyDiscrete C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Bicategory.instStrictOfIsLocallyDiscrete (B : Type u_1) [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] : CategoryTheory.Bicategory.Strict B

Equations

• ⋯ = ⋯

@[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 }

@[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 }

@[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

@[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 ⋯