σ_obj

Mathlib.AlgebraicTopology.SimplicialSet.Nerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.nerve.σ_obj

English

In the nerve of a category, the σ-face maps pick out the predAbove component.

Русский

В нерве категории σ‑лица выбирают компонент predAbove.

LaTeX

$$$ ((\nerve C).σ i x).obj j = x.obj (i.predAbove j) $$$

Lean4

theorem σ_obj {n : ℕ} (i : Fin (n + 1)) (x : (nerve C) _⦋n⦌) (j : Fin (n + 2)) :
    ((nerve C).σ i x).obj j = x.obj (i.predAbove j) :=
  rfl

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

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

Разделы

Аффилиация

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