isIso_of_nonDegenerate — Mathlib

English

If x is non-degenerate and x = X.map f.op y with epi f, then f is an isomorphism.

Русский

Если x недегенеративен и x = X.map f.op y с эпиморфизмом f, то f — изоморфизм.

LaTeX

$$$ x \in X_{\text{nonDegenerate}}(n) \Rightarrow \big( f: [n] \to m \text{ epi} \big) \Rightarrow \text{IsIso}(f) $$$

Lean4

theorem isIso_of_nonDegenerate (x : X.nonDegenerate n) {m : SimplexCategory} (f : ⦋n⦌ ⟶ m) [Epi f] (y : X.obj (op m))
    (hy : X.map f.op y = x) : IsIso f := by
  obtain ⟨x, hx⟩ := x
  induction m using SimplexCategory.rec with
  | _ m
  rw [mem_nonDegenerate_iff_notMem_degenerate] at hx
  by_contra!
  refine hx ⟨_, not_le.1 (fun h ↦ this ?_), f, y, hy⟩
  rw [SimplexCategory.isIso_iff_of_epi]
  exact le_antisymm h (SimplexCategory.len_le_of_epi f)

Похожие утверждения