Subcomplexes of a simplicial set

Given a simplicial set X, this file defines the type X.Subcomplex of subcomplexes of X as an abbreviation for Subpresheaf X. It also introduces a coercion from X.Subcomplex to SSet.

Implementation note

SSet.{u} is defined as Cᵒᵖ ⥤ Type u, but it is not an abbreviation. This is the reason why Subpresheaf.ι is redefined here as Subcomplex.ι so that this morphism appears as a morphism in SSet instead of a morphism in the category of presheaves.

@[reducible, inline]

abbrev SSet.Subcomplex (X : SSet) : Type u

The complete lattice of subcomplexes of a simplicial set.

Equations

• X.Subcomplex = CategoryTheory.Subpresheaf X

@[reducible, inline]

abbrev SSet.Subcomplex.toSSet {X : SSet} (A : X.Subcomplex) : SSet

The underlying simplicial set of a subcomplex.

Equations

• A.toSSet = CategoryTheory.Subpresheaf.toPresheaf A

instance SSet.instCoeOutSubcomplex {X : SSet} : CoeOut X.Subcomplex SSet

Equations

• SSet.instCoeOutSubcomplex = { coe := fun (S : X.Subcomplex) => CategoryTheory.Subpresheaf.toPresheaf S }

@[reducible, inline]

abbrev SSet.Subcomplex.ι {X : SSet} (A : X.Subcomplex) : CategoryTheory.Subpresheaf.toPresheaf A ⟶ X

If A : Subcomplex X, this is the inclusion A ⟶ X in the category SSet.

Equations

• A.ι = CategoryTheory.Subpresheaf.ι A

instance SSet.instMonoι {X : SSet} (A : X.Subcomplex) : CategoryTheory.Mono A.ι