English
If two representations of the same x are given by non-degenerate data, then the underlying epi maps are equal.
Русский
Если два представления одного и того же x даны через недегенеративные данные, то соответствующие эпиморфные отображения равны.
LaTeX
$$$ \forall x, \forall f_1, y_1, \forall f_2, y_2, \big( X.map f_1.op y_1 = X.map f_2.op y_2 \Rightarrow f_1 = f_2 \big) $$$
Lean4
theorem unique_nonDegenerate_map (x : X _⦋n⦌) {m : ℕ} (f₁ : ⦋n⦌ ⟶ ⦋m⦌) [Epi f₁] (y₁ : X.nonDegenerate m)
(hy₁ : x = X.map f₁.op y₁) (f₂ : ⦋n⦌ ⟶ ⦋m⦌) (y₂ : X.nonDegenerate m) (hy₂ : x = X.map f₂.op y₂) : f₁ = f₂ :=
by
ext x : 3
suffices ∃ (hf₁ : SplitEpi f₁), hf₁.section_.toOrderHom (f₁.toOrderHom x) = x
by
obtain ⟨hf₁, hf₁'⟩ := this
dsimp at hf₁'
simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁) (f₁.toOrderHom x)).symm
obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁
let α (y : Fin (m + 1)) : Fin (n + 1) := if y = f₁.toOrderHom x then x else hf.section_.toOrderHom y
have hα₁ (y : Fin (m + 1)) : f₁.toOrderHom (α y) = y :=
by
dsimp [α]
split_ifs with hy
· rw [hy]
· apply SimplexCategory.congr_toOrderHom_apply hf.id
have hα₂ : Monotone α := by
rintro y₁ y₂ h
by_contra! h'
suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by cutsat] at h'
simpa only [hα₁] using f₁.toOrderHom.monotone h'.le
exact ⟨{ section_ := SimplexCategory.Hom.mk ⟨α, hα₂⟩, id := by ext : 3; apply hα₁ }, by simp [α]⟩
