English
For each x in SSet.S there exists a unique n and y with y.subcomplex = x.subcomplex; i.e., existence and uniqueness of the matching nondegenerate simplex.
Русский
Для каждого x в SSet.S существует единственный n и y с равенством y.subcomplex = x.subcomplex; существует и уникально соответствующее неdegenerate‑симплекс.
LaTeX
$$$\exists!\; y:\; X.N,\; y.subcomplex = x.subcomplex$$$
Lean4
theorem existsUnique_n (x : X.S) : ∃! (y : X.N), y.subcomplex = x.subcomplex :=
existsUnique_of_exists_of_unique
(by
obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
· simp only [Subcomplex.ofSimplex_le_iff]
have := isSplitEpi_of_epi f
have : Function.Injective (X.map f.op) := by
rw [← mono_iff_injective]
infer_instance
refine ⟨(section_ f).op, this ?_⟩
dsimp
rw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← op_comp, Category.assoc,
IsSplitEpi.id, Category.comp_id]
· simp only [Subcomplex.ofSimplex_le_iff]
exact ⟨f.op, rfl⟩)
(fun y₁ y₂ h₁ h₂ ↦ N.subcomplex_injective (by rw [h₁, h₂]))
