ι0₂ — Mathlib

English

The reflexive quiver underlying a nerve is isomorphic to the reflexive quiver underlying the category itself.

Русский

Рефлексивная графовая система, лежащая в основе нерва, изоморфна графовой системе, лежащей в основе самой категории.

LaTeX

$$$$\text{ofNerve₂} \simeq \text{ReflQuiv.forget}$$$$

Lean4

/-- The map that picks up the initial vertex of a 2-simplex, as a morphism in the 2-truncated
simplex category. -/
def ι0₂ : (⦋0⦌₂) ⟶ ⦋2⦌₂ :=
  δ₂ (n := 0) 1 ≫ δ₂ (n := 1) 1

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