English
For a 2-truncated nerve of a partially ordered set, a simplex s lies in the image of the σ_i map if and only if the i-th and (i+1)-st vertices coincide, i.e., s.obj i.castSucc = s.obj i.succ.
Русский
Для 2‑уровневого нерва частично упорядоченного множества, симплекс s принадлежит образу σ_i тогда и только тогда, когда i-я вершина совпадает с (i+1)-й вершиной: s.obj i.castSucc = s.obj i.succ.
LaTeX
$$$ s \in \mathrm{range}(\sigma_i) \;\text{iff}\; s.obj i.castSucc = s.obj i.succ $$$
Lean4
theorem mem_range_nerve_σ_iff (s : (nerve X) _⦋n + 1⦌) (i : Fin (n + 1)) :
s ∈ Set.range ((nerve X).σ i) ↔ s.obj i.castSucc = s.obj i.succ :=
by
constructor
· rintro ⟨s, rfl⟩
simp [nerve.σ_obj]
· intro h
refine ⟨(nerve X).δ i.castSucc s, ?_⟩
ext j
rw [nerve.σ_obj, nerve.δ_obj]
by_cases h₁ : i.castSucc < j
· obtain ⟨j, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h₁)
rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]
· simp only [not_lt] at h₁
grind [SimplexCategory.len_mk, → Fin.succAbove_of_castSucc_lt, → Fin.predAbove_of_le_castSucc,
Fin.castSucc_castPred, Fin.castPred_castSucc, Fin.succAbove_castSucc_self, → LE.le.lt_or_eq]
