ev01₂ — Mathlib

English

The arrow in the refl-Quiver OneTruncation₂ V from ev0₂ φ to ev1₂ φ is the edge δ2₂ on φ, i.e., ev01₂ φ.

Русский

Стрела в reflQuiver OneTruncation₂ V от ev0₂ φ к ev1₂ φ задаёт ребро δ2₂ на φ, то есть ev01₂ φ.

LaTeX

$$$ev01_2(\\varphi) : ev0_2(\\varphi) \\to ev1_2(\\varphi)$$$

Lean4

/-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
2nd face of a 2-simplex. -/
def ev01₂ {V : SSet.Truncated 2} (φ : V _⦋2⦌₂) : ev0₂ φ ⟶ ev1₂ φ :=
  ⟨V.map δ2₂.op φ, map_map_of_eq V (SimplexCategory.δ_comp_δ (j := 1) le_rfl), map_map_of_eq V rfl⟩

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