Documentation

Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete

The Nerve of a Codiscrete Category #

In the codiscrete category on a type X, every hom-type is given by Unit. When we take the nerve of such a category, the n-simplices become equivalent to X-vectors of length n + 1. Therefore, if X has decidable equality, so does the type of n-simplices in this nerve.

source
def CategoryTheory.Codiscrete.equivFun {X : Type u} {n : ℕ} :
(nerve (Codiscrete X)).obj (Opposite.op { len := n }) ≃ (Fin (n + 1) → X)

Since the morphisms in a codiscrete category do not carry information, an n-simplex of coherentIso is equivalent to an X-vector of length (n + 1).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Codiscrete.equivFun_apply {X : Type u} {n : ℕ} (f : (nerve (Codiscrete X)).obj (Opposite.op { len := n })) (k : Fin (n + 1)) :
    equivFun f k = (f.obj k).as
    source
    @[simp]
    theorem CategoryTheory.Codiscrete.equivFun_symm_apply_obj_as {X : Type u} {n : ℕ} (f : Fin (n + 1) → X) (k : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)) :
    ((equivFun.symm f).obj k).as = f k
    source
    @[simp]
    theorem CategoryTheory.Codiscrete.equivFun_symm_apply_map {X : Type u} {n : ℕ} (f : Fin (n + 1) → X) {X✝ Y✝ : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)} (x✝ : X✝ ⟶ Y✝) :
    (equivFun.symm f).map x✝ = ({ as := f X✝ }.iso { as := f Y✝ }).hom
    source
    @[implicit_reducible]
    instance CategoryTheory.Codiscrete.instDecidableEqObjOppositeSimplexCategoryNerveOpMk {X : Type u} {n : ℕ} [DecidableEq X] :
    DecidableEq ((nerve (Codiscrete X)).obj (Opposite.op { len := n }))

    If a type X has decidable equality, the nerve of the codiscrete category on X has decidable equality as well.

    Equations