English
Two morphisms from a horn are equal if they agree on all suitable faces.
Русский
Два морфизма из горна равны, если они совпадают на всех допустимых гранях.
LaTeX
$$$\text{Two morphisms from a horn are equal if they agree on all suitable faces}$$$
Lean4
/-- Two morphisms from a horn are equal if they are equal on all suitable faces. -/
protected theorem hom_ext {n : ℕ} {i : Fin (n + 2)} {S : SSet} (σ₁ σ₂ : (Λ[n + 1, i] : SSet.{u}) ⟶ S)
(h : ∀ (j) (h : j ≠ i), σ₁.app _ (face i j h) = σ₂.app _ (face i j h)) : σ₁ = σ₂ :=
by
rw [← Subpresheaf.equalizer_eq_iff]
apply le_antisymm (Subpresheaf.equalizer_le σ₁ σ₂)
simp only [horn_eq_iSup, iSup_le_iff, Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]
intro j hj
exact (Subpresheaf.mem_equalizer_iff σ₁ σ₂ (face i j hj)).2 (by apply h)
