English
There is a canonical constant map from any X to Y determined by a chosen vertex y ∈ Y_⟨0⟩, sending every n-simplex to y via Y-map.
Русский
Существует каноническая константная карта из X в Y, заданная вершиной y ∈ Y_0, отправляющая каждый n-элемент в y через отображение Y.
LaTeX
$$$\text{const}_{y}: X \to Y\quad\text{with}\quad (\text{const}_{y})_{n} = Y.map\big((n.unop).const\{0\}\big)^{\mathrm{op}}(y)$$$
Lean4
/-- The constant map of simplicial sets `X ⟶ Y` induced by a simplex `y : Y _[0]`. -/
@[simps]
def const {X Y : SSet.{u}} (y : Y _⦋0⦌) : X ⟶ Y
where
app n _ := Y.map (n.unop.const _ 0).op y
naturality _ _
_ := by
ext
dsimp
rw [← FunctorToTypes.map_comp_apply]
rfl
