mathlib documentation

category_theory.discrete_category

def category_theory.discrete  :
Type u₁Type u₁

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

Equations
@[instance]

The "discrete" category on a type, whose morphisms are equalities.

Because we do not allow morphisms in Prop (only in Type), somewhat annoyingly we have to define X ⟶ Y as ulift (plift (X = Y)).

See https://stacks.math.columbia.edu/tag/001A

Equations
theorem category_theory.discrete.eq_of_hom {α : Type u₁} {X Y : category_theory.discrete α} :
(X Y)X = Y

Extract the equation from a morphism in a discrete category.

@[simp]
theorem category_theory.discrete.id_def {α : Type u₁} (X : category_theory.discrete α) :
{down := {down := _}} = 𝟙 X

def category_theory.discrete.functor {C : Type u₂} [category_theory.category C] {I : Type u₁} :
(I → C)category_theory.discrete I C

Any function I → C gives a functor discrete I ⥤ C.

Equations
@[simp]
theorem category_theory.discrete.functor_obj {C : Type u₂} [category_theory.category C] {I : Type u₁} (F : I → C) (i : I) :

theorem category_theory.discrete.functor_map {C : Type u₂} [category_theory.category C] {I : Type u₁} (F : I → C) {i : category_theory.discrete I} (f : i i) :

def category_theory.discrete.nat_trans {C : Type u₂} [category_theory.category C] {I : Type u₁} {F G : category_theory.discrete I C} :
(Π (i : category_theory.discrete I), F.obj i G.obj i)(F G)

For functors out of a discrete category, a natural transformation is just a collection of maps, as the naturality squares are trivial.

Equations
def category_theory.discrete.nat_iso {C : Type u₂} [category_theory.category C] {I : Type u₁} {F G : category_theory.discrete I C} :
(Π (i : category_theory.discrete I), F.obj i G.obj i)(F G)

For functors out of a discrete category, a natural isomorphism is just a collection of isomorphisms, as the naturality squares are trivial.

Equations
@[simp]
theorem category_theory.discrete.nat_iso_hom_app {C : Type u₂} [category_theory.category C] {I : Type u₁} {F G : category_theory.discrete I C} (f : Π (i : category_theory.discrete I), F.obj i G.obj i) (i : I) :

@[simp]
theorem category_theory.discrete.nat_iso_inv_app {C : Type u₂} [category_theory.category C] {I : Type u₁} {F G : category_theory.discrete I C} (f : Π (i : category_theory.discrete I), F.obj i G.obj i) (i : I) :

@[simp]
theorem category_theory.discrete.nat_iso_app {C : Type u₂} [category_theory.category C] {I : Type u₁} {F G : category_theory.discrete I C} (f : Π (i : category_theory.discrete I), F.obj i G.obj i) (i : I) :

Every functor F from a discrete category is naturally isomorphic (actually, equal) to discrete.functor (F.obj).

Equations

We can convert an equivalence of discrete categories to a type-level equiv.

Equations
@[simp]
theorem category_theory.discrete.functor_map_id {J : Type v₁} {C : Type u₂} [category_theory.category C] (F : category_theory.discrete J C) {j : category_theory.discrete J} (f : j j) :
F.map f = 𝟙 (F.obj j)