ev12₂ — Mathlib

English

The arrow in the refl-Quiver OneTruncation₂ V from ev1₂ φ to ev2₂ φ is given by the edge δ0₂ on φ, i.e., ev12₂ φ.

Русский

Стрелка в reflQuiver OneTruncation₂ V от ev1₂ φ к ev2₂ φ задаётся ребром δ0₂ на φ, то есть ev12₂ φ.

LaTeX

$$$ev12_2(\\varphi) : ev1_2(\\varphi) \\to ev2_2(\\varphi)$$$

Lean4

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

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