mathlib3 documentation

category_theory.discrete_category

Discrete categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define discrete α as a structure containing a term a : α for any type α, and use this type alias to provide a small_category instance whose only morphisms are the identities.

There is an annoying technical difficulty that it has turned out to be inconvenient to allow categories with morphisms living in Prop, so instead of defining X ⟶ Y in discrete α as X = Y, one might define it as plift (X = Y). In fact, to allow discrete α to be a small_category (i.e. with morphisms in the same universe as the objects), we actually define the hom type X ⟶ Y as ulift (plift (X = Y)).

discrete.functor promotes a function f : I → C (for any category C) to a functor discrete.functor f : discrete I ⥤ C.

Similarly, discrete.nat_trans and discrete.nat_iso promote I-indexed families of morphisms, or I-indexed families of isomorphisms to natural transformations or natural isomorphism.

We show equivalences of types are the same as (categorical) equivalences of the corresponding discrete categories.

source
theorem category_theory.discrete.ext_iff {α : Type u₁} (x y : category_theory.discrete α) :
x = y ↔ x.as = y.as
source
@[ext]
structure category_theory.discrete (α : Type u₁) :
Type u₁
  • as : α

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

Instances for category_theory.discrete
source
theorem category_theory.discrete.ext {α : Type u₁} (x y : category_theory.discrete α) (h : x.as = y.as) :
x = y
source
@[simp]
theorem category_theory.discrete.mk_as {α : Type u₁} (X : category_theory.discrete α) :
{as := X.as} = X
source
def category_theory.discrete_equiv {α : Type u₁} :
category_theory.discrete α ≃ α

discrete α is equivalent to the original type α.

Equations
source
@[simp]
theorem category_theory.discrete_equiv_symm_apply_as {α : Type u₁} (as : α) :
(⇑(category_theory.discrete_equiv.symm) as).as = as
source
@[simp]
theorem category_theory.discrete_equiv_apply {α : Type u₁} (self : category_theory.discrete α) :
⇑category_theory.discrete_equiv self = self.as
source
@[protected, instance]
def category_theory.discrete.decidable_eq {α : Type u₁} [decidable_eq α] :
decidable_eq (category_theory.discrete α)
Equations
source
@[protected, 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
@[protected, instance]
def category_theory.discrete.inhabited {α : Type u₁} [inhabited α] :
inhabited (category_theory.discrete α)
Equations
source
@[protected, instance]
def category_theory.discrete.subsingleton {α : Type u₁} [subsingleton α] :
subsingleton (category_theory.discrete α)
source
meta def tactic.discrete_cases  :
tactic unit

A simple tactic to run cases on any discrete α hypotheses.

source
meta def tactic.interactive.discrete_cases  :
tactic unit

A simple tactic to run cases on any discrete α hypotheses.

source
@[protected, instance]
def category_theory.discrete.unique {α : Type u₁} [unique α] :
unique (category_theory.discrete α)
Equations
source
theorem category_theory.discrete.eq_of_hom {α : Type u₁} {X Y : category_theory.discrete α} (i : X ⟶ Y) :
X.as = Y.as

Extract the equation from a morphism in a discrete category.

source
@[reducible]
def category_theory.discrete.eq_to_hom {α : Type u₁} {X Y : category_theory.discrete α} (h : X.as = Y.as) :
X ⟶ Y

Promote an equation between the wrapped terms in X Y : discrete α to a morphism X ⟶ Y in the discrete category.

source
@[reducible]
def category_theory.discrete.eq_to_iso {α : Type u₁} {X Y : category_theory.discrete α} (h : X.as = Y.as) :
X ≅ Y

Promote an equation between the wrapped terms in X Y : discrete α to an isomorphism X ≅ Y in the discrete category.

source
@[reducible]
def category_theory.discrete.eq_to_hom' {α : Type u₁} {a b : α} (h : a = b) :
{as := a} ⟶ {as := b}

A variant of eq_to_hom that lifts terms to the discrete category.

source
@[reducible]
def category_theory.discrete.eq_to_iso' {α : Type u₁} {a b : α} (h : a = b) :
{as := a} ≅ {as := b}

A variant of eq_to_iso that lifts terms to the discrete category.

source
@[simp]
theorem category_theory.discrete.id_def {α : Type u₁} (X : category_theory.discrete α) :
{down := {down := _}} = 𝟙 X
source
@[protected, 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
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
Instances for category_theory.discrete.functor
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 {as := 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.as)
source
@[simp]
theorem category_theory.discrete.functor_comp_hom_app {C : Type u₂} [category_theory.category C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : category_theory.discrete I) :
(category_theory.discrete.functor_comp f g).hom.app X = 𝟙 ((category_theory.discrete.functor (f ∘ g)).obj X)
source
@[simp]
theorem category_theory.discrete.functor_comp_inv_app {C : Type u₂} [category_theory.category C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : category_theory.discrete I) :
(category_theory.discrete.functor_comp f g).inv.app X = 𝟙 ((category_theory.discrete.functor (f ∘ g)).obj X)
source
def category_theory.discrete.functor_comp {C : Type u₂} [category_theory.category C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
category_theory.discrete.functor (f ∘ g) ≅ category_theory.discrete.functor (category_theory.discrete.mk ∘ g) ⋙ category_theory.discrete.functor f

The discrete functor induced by a composition of maps can be written as a composition of two discrete functors.

Equations
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) (X : category_theory.discrete I) :
(category_theory.discrete.nat_iso f).hom.app X = (f X).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) (X : category_theory.discrete I) :
(category_theory.discrete.nat_iso f).inv.app X = (f X).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 : category_theory.discrete I) :
(category_theory.discrete.nat_iso f).app i = f i
source
@[simp]
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 ∘ category_theory.discrete.mk)

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

Equations
source
@[simp]
def category_theory.discrete.comp_nat_iso_discrete {C : Type u₂} [category_theory.category C] {I : Type u₁} {D : Type u₃} [category_theory.category D] (F : I → C) (G : C ⥤ D) :
category_theory.discrete.functor F ⋙ G ≅ category_theory.discrete.functor (G.obj ∘ F)

Composing discrete.functor F with another functor G amounts to composing F with G.obj

Equations
source
@[simp]
theorem category_theory.discrete.equivalence_functor {I : Type u₁} {J : Type u₂} (e : I ≃ J) :
(category_theory.discrete.equivalence e).functor = category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑e)
source
@[simp]
theorem category_theory.discrete.equivalence_unit_iso {I : Type u₁} {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.discrete.eq_to_iso _)
source
def category_theory.discrete.equivalence {I : Type u₁} {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 : Type u₁} {J : Type u₂} (e : I ≃ J) :
(category_theory.discrete.equivalence e).inverse = category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑(e.symm))
source
@[simp]
theorem category_theory.discrete.equivalence_counit_iso {I : Type u₁} {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.discrete.eq_to_iso _)
source
@[simp]
theorem category_theory.discrete.equiv_of_equivalence_apply {α : Type u₁} {β : Type u₂} (h : category_theory.discrete α ≌ category_theory.discrete β) (ᾰ : α) :
⇑(category_theory.discrete.equiv_of_equivalence h) ᾰ = (category_theory.discrete.as ∘ h.functor.obj ∘ category_theory.discrete.mk) ᾰ
source
@[simp]
theorem category_theory.discrete.equiv_of_equivalence_symm_apply {α : Type u₁} {β : Type u₂} (h : category_theory.discrete α ≌ category_theory.discrete β) (ᾰ : β) :
⇑((category_theory.discrete.equiv_of_equivalence h).symm) ᾰ = (category_theory.discrete.as ∘ h.inverse.obj ∘ category_theory.discrete.mk) ᾰ
source
def category_theory.discrete.equiv_of_equivalence {α : Type u₁} {β : Type u₂} (h : category_theory.discrete α ≌ category_theory.discrete β) :
α ≃ β

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

Equations
source
@[protected]
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.opposite_functor_obj_as (α : Type u₁) (X : (category_theory.discrete α)ᵒᵖ) :
((category_theory.discrete.opposite α).functor.obj X).as = (opposite.unop X).as
source
@[simp]
theorem category_theory.discrete.opposite_inverse_obj (α : Type u₁) (ᾰ : category_theory.discrete α) :
(category_theory.discrete.opposite α).inverse.obj ᾰ = opposite.op ᾰ
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)