English
Every morphism from any Δ to the 0-simplex Δ^0 is equal to the unique morphism, i.e., the Hom-set is a singleton.
Русский
Каждый морфизм из любого Δ в 0-словарь Δ^0 равен единственному морфизму, т.е. множество морфизмов единично.
LaTeX
$$∀ Δ, (Δ ⟶ ⦋0⦌)) = singleton$$
Lean4
/-- The second simplicial identity -/
@[reassoc]
theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.castSucc) :
δ i.castSucc ≫ σ j.succ = σ j ≫ δ i := by
ext k : 3
dsimp [σ, δ]
rcases le_or_gt i k with (hik | hik)
· rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik), Fin.succ_predAbove_succ,
Fin.succAbove_of_le_castSucc]
rcases le_or_gt k (j.castSucc) with (hjk | hjk)
· rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]
· rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]
exact H.trans_lt hjk
· rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hik)]
have hjk := H.trans_lt' hik
rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr (hjk.trans (Fin.castSucc_lt_succ _)).le),
Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
Fin.castSucc_castPred]
rwa [Fin.castSucc_castPred]
