English
x ∈ degenerate n iff there exists m, epi f and y with x = X.map f.op y and x ∈ range of X.map f.op.
Русский
x ∈ degenerate n тогда и только тогда, когда существует m, epi f и y с x = X.map f.op y и x лежит в образе X.map f.op.
LaTeX
$$$ x \in X_{\text{degenerate}}(n) \;\iff\; \exists m< n, \exists f: [n] \to [m], \text{ epi } f, \ x \in \mathrm{range}(X.map f^{op}) $$$
Lean4
theorem mem_degenerate_iff (x : X _⦋n⦌) :
x ∈ X.degenerate n ↔ ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f), x ∈ Set.range (X.map f.op) :=
by
constructor
· rintro ⟨m, hm, f, y, hy⟩
rw [← image.fac f, op_comp] at hy
have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)
exact ⟨(image f).len, by cutsat, factorThruImage f, inferInstance, by aesop⟩
· rintro ⟨m, hm, f, hf, hx⟩
exact ⟨m, hm, f, hx⟩
