# mathlibdocumentation

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]
def category_theory.discrete_category (α : Type u₁) :

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
@[instance]
def category_theory.discrete.inhabited {α : Type u₁} [inhabited α] :

Equations
@[instance]

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

@[instance]

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

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

Equations
• = {obj := F, map := λ (X Y : (f : X Y), ulift.cases_on f (λ (f : plift (X = Y)), f.cases_on (λ (f : X = Y), f.dcases_on (λ (H_1 : Y = X), eq.rec (λ (f : X = X) (H_2 : f == _), 𝟙 (F X)) _ f) _ _)), map_id' := _, map_comp' := _}
@[simp]
theorem category_theory.discrete.functor_obj {C : Type u₂} {I : Type u₁} (F : I → C) (i : I) :
= F i

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

def category_theory.discrete.nat_trans {C : Type u₂} {I : Type u₁} {F G : C} :
(Π (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
@[simp]
theorem category_theory.discrete.nat_trans_app {C : Type u₂} {I : Type u₁} {F G : C} (f : Π (i : , F.obj i G.obj i) (i : category_theory.discrete I) :
= f i

def category_theory.discrete.nat_iso {C : Type u₂} {I : Type u₁} {F G : C} :
(Π (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₂} {I : Type u₁} {F G : C} (f : Π (i : , F.obj i G.obj i) (i : I) :
= (f i).hom

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

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

def category_theory.discrete.nat_iso_functor {C : Type u₂} {I : Type u₁} {F : C} :

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

Equations
@[simp]
theorem category_theory.discrete.equivalence_functor {I J : Type u₁} (e : I J) :

@[simp]
theorem category_theory.discrete.equivalence_unit_iso {I J : Type u₁} (e : I J) :

def category_theory.discrete.equivalence {I J : Type u₁} :
I J

We can promote a type-level equiv to an equivalence between the corresponding discrete categories.

Equations
@[simp]
theorem category_theory.discrete.equivalence_inverse {I J : Type u₁} (e : I J) :

@[simp]
theorem category_theory.discrete.equivalence_counit_iso {I J : Type u₁} (e : I J) :

def category_theory.discrete.equiv_of_equivalence {α β : Type u₁} :
α β

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

Equations
def category_theory.discrete.opposite (α : Type u₁) :

A discrete category is equivalent to its opposite category.

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