English
The boundary ∂Δ[n] is the subcomplex of Δ[n] consisting of those n-simplices whose underlying order-preserving map is not surjective.
Русский
Граница ∂Δ[n] — это подвпункт Δ[n], состоящий из тех n-симпликсов, чей соответствующий монотонный переход не сюръективен.
LaTeX
$$$ \\partial \\Delta[n] = \\{ s ∈ \\Delta[n] \\mid \\text{the underlying order map is not surjective} \\}$$$
Lean4
/-- Given a term in the cone over the diagram
`(proj (op ⦋n⦌) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)` where `X` is
Strict Segal, one can produce an `n`-simplex in `X`. -/
@[simp]
noncomputable def lift {X : SSet.{u}} (sx : StrictSegal X) {n}
(s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)) (x : s.pt) : X _⦋n⦌ :=
sx.spineToSimplex
{ vertex := fun i ↦ s.π.app (.mk (Y := op ⦋0⦌₂) (.op (SimplexCategory.const _ _ i))) x
arrow := fun i ↦ s.π.app (.mk (Y := op ⦋1⦌₂) (.op (mkOfLe _ _ (Fin.castSucc_le_succ i)))) x
arrow_src := fun i ↦
by
let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶ strArrowMk₂ (⦋0⦌.const _ i.castSucc) :=
StructuredArrow.homMk (δ 1).op (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
exact congr_fun (s.w φ) x
arrow_tgt := fun i ↦ by
dsimp
let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶ strArrowMk₂ (⦋0⦌.const _ i.succ) :=
StructuredArrow.homMk (δ 0).op (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
exact congr_fun (s.w φ) x }
