Theorems · Definition · algebraic topology

SSet.relativeCellComplexOfMono.l

{X Y : SSet} →
  (i : X ⟶ Y) →
    (d : ℕ) → SSet.relativeCellComplexOfMono.sigmaBoundary i d ⟶ SSet.relativeCellComplexOfMono.sigmaStdSimplex i d

the left morphism of the pushout square isPushout i d: this is the coproduct of copies of the boundary inclusion ∂Δ[d] ⟶ Δ[d] indexed by the nondegenerate d-simplices of Y not in the range of i.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Cited by

8 results in Mathlib

Foundations

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