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.

instance SSet.instBalanced : CategoryTheory.Balanced SSet

@[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.Subcomplex.instCoeOut {X : SSet} : CoeOut X.Subcomplex SSet

Equations

• SSet.Subcomplex.instCoeOut = { coe := fun (S : X.Subcomplex) => S.toSSet }

@[reducible, inline]

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

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

Equations

• A.ι = CategoryTheory.Subpresheaf.ι A

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

@[reducible, inline]

abbrev SSet.Subcomplex.ofSimplex {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : X.Subcomplex

The subcomplex of a simplicial set that is generated by a simplex.

Equations

• SSet.Subcomplex.ofSimplex x = CategoryTheory.Subpresheaf.ofSection x

theorem SSet.Subcomplex.mem_ofSimplex_obj {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) : x ∈ (ofSimplex x).obj (Opposite.op (SimplexCategory.mk n))

theorem SSet.Subcomplex.ofSimplex_le_iff {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) (A : X.Subcomplex) : ofSimplex x ≤ A ↔ x ∈ A.obj (Opposite.op (SimplexCategory.mk n))

theorem SSet.Subcomplex.mem_ofSimplex_obj_iff {X : SSet} {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) {m : SimplexCategoryᵒᵖ} (y : X.obj m) : y ∈ (ofSimplex x).obj m ↔ ∃ (f : Opposite.unop m ⟶ SimplexCategory.mk n), X.map f.op x = y

@[reducible, inline]

abbrev SSet.Subcomplex.range {X Y : SSet} (f : X ⟶ Y) : Y.Subcomplex

The range of a morphism of simplicial sets, as a subcomplex.

Equations

• SSet.Subcomplex.range f = CategoryTheory.Subpresheaf.range f

@[reducible, inline]

abbrev SSet.Subcomplex.toRange {X Y : SSet} (f : X ⟶ Y) : X ⟶ (range f).toSSet

The morphism X ⟶ Subcomplex.range f induced by f : X ⟶ Y.

Equations

• SSet.Subcomplex.toRange f = CategoryTheory.Subpresheaf.toRange f

@[simp]

theorem SSet.Subcomplex.toRange_ι {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (toRange f) (range f).ι = f

@[simp]

theorem SSet.Subcomplex.toRange_ι_assoc {X Y : SSet} (f : X ⟶ Y) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (toRange f) (CategoryTheory.CategoryStruct.comp (range f).ι h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem SSet.Subcomplex.toRange_app_val {X Y : SSet} (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ) : ↑((toRange f).app Δ x) = f.app Δ x

instance SSet.Subcomplex.instEpiToRange {X Y : SSet} (f : X ⟶ Y) : CategoryTheory.Epi (toRange f)

instance SSet.Subcomplex.instMonoToRange {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (toRange f)

instance SSet.Subcomplex.instIsIsoToRangeOfMono {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.IsIso (toRange f)