Theorems · Definition · algebraic topology

SSet.relativeCellComplexOfMono

{X Y : SSet} →
  (i : X ⟶ Y) → [CategoryTheory.Mono i] → HomotopicalAlgebra.RelativeCellComplex (fun n x => (SSet.boundary n).ι) i

If i : X ⟶ Y is a monomorphism of simplicial sets, then it is a relative cell complex with basic cells given by boundary inclusions ∂Δ[d] ⟶ Δ[d], one for each nondegenerate d-simplex of Y not in the range of X.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Cited by

14 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Mono