σ₀_mk₀_eq

Mathlib.AlgebraicTopology.SimplicialSet.Nerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.nerve.σ₀_mk₀_eq

English

The σ0-map on mk0 x yields mk1 x and the identity on x.

Русский

Образ σ₀ при mk₀ x даёт mk₁ x и тождественный отображение на x.

LaTeX

$$$ (\mathrm{nerve}\; C).\sigma 0 (.\mk_0 x) = .mk_1 (\mathbb{1} x) $$$

Lean4

theorem σ₀_mk₀_eq (x : C) : (nerve C).σ (0 : Fin 1) (.mk₀ x) = .mk₁ (𝟙 x) :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru