mathlib documentation

category_theory.discrete_category

source
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
source
@[instance]
def category_theory.discrete_category (α : Type u₁) :
category_theory.small_category (category_theory.discrete α)

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

Equations
source
@[instance]
def category_theory.discrete.subsingleton {α : Type u₁} [subsingleton α] :
subsingleton (category_theory.discrete α)

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

Extract the equation from a morphism in a discrete category.

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

source
@[instance]
def category_theory.discrete.category_theory.is_iso {I : Type u₁} {i j : category_theory.discrete I} (f : i ⟶ j) :
category_theory.is_iso f

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

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

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

source
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) :
(category_theory.discrete.functor F).map f = 𝟙 (F i)

source
def category_theory.discrete.nat_trans {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) :
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
source
@[simp]
theorem category_theory.discrete.nat_trans_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 : category_theory.discrete I) :
(category_theory.discrete.nat_trans f).app i = f i

source
def category_theory.discrete.nat_iso {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) :
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
source
@[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) :
(category_theory.discrete.nat_iso f).hom.app i = (f i).hom

source
@[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) :
(category_theory.discrete.nat_iso f).inv.app i = (f i).inv

source
@[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) :
(category_theory.discrete.nat_iso f).app i = f i

source
def category_theory.discrete.nat_iso_functor {C : Type u₂} [category_theory.category C] {I : Type u₁} {F : category_theory.discrete I ⥤ C} :
F ≅ category_theory.discrete.functor F.obj

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

Equations
source
@[simp]
theorem category_theory.discrete.equivalence_functor {I J : Type u₁} (e : I ≃ J) :
(category_theory.discrete.equivalence e).functor = category_theory.discrete.functor ⇑e

source
@[simp]
theorem category_theory.discrete.equivalence_unit_iso {I J : Type u₁} (e : I ≃ J) :
(category_theory.discrete.equivalence e).unit_iso = category_theory.discrete.nat_iso (λ (i : category_theory.discrete I), category_theory.eq_to_iso _)

source
def category_theory.discrete.equivalence {I J : Type u₁} (e : I ≃ J) :
category_theory.discrete I ≌ category_theory.discrete J

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

Equations
source
@[simp]
theorem category_theory.discrete.equivalence_inverse {I J : Type u₁} (e : I ≃ J) :
(category_theory.discrete.equivalence e).inverse = category_theory.discrete.functor ⇑(e.symm)

source
@[simp]
theorem category_theory.discrete.equivalence_counit_iso {I J : Type u₁} (e : I ≃ J) :
(category_theory.discrete.equivalence e).counit_iso = category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.eq_to_iso _)

source
@[simp]
theorem category_theory.discrete.equiv_of_equivalence_to_fun {α β : Type u₁} (h : category_theory.discrete α ≌ category_theory.discrete β) (a : category_theory.discrete α) :
⇑(category_theory.discrete.equiv_of_equivalence h) a = h.functor.obj a

source
def category_theory.discrete.equiv_of_equivalence {α β : Type u₁} (h : category_theory.discrete α ≌ category_theory.discrete β) :
α ≃ β

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

Equations
source
@[simp]
theorem category_theory.discrete.equiv_of_equivalence_inv_fun {α β : Type u₁} (h : category_theory.discrete α ≌ category_theory.discrete β) (a : category_theory.discrete β) :
(category_theory.discrete.equiv_of_equivalence h).inv_fun a = h.inverse.obj a

source
def category_theory.discrete.opposite (α : Type u₁) :
(category_theory.discrete α)ᵒᵖ ≌ category_theory.discrete α

A discrete category is equivalent to its opposite category.

Equations
source
@[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)