eq_id_of_epi — Mathlib

English

If i: x ⟶ x is epi, then i equals the identity on x.

Русский

Если i: x ⟶ x эпиморфизм, то i равен тождественному на x.

LaTeX

$$$\\\\forall x \\\\in \\\\text{SimplexCategory},\\\\forall i: x \\\\to x,[\\\\text{Epi } i] \\\Rightarrow i = \\mathsf{Id}_x$$$

Lean4

theorem eq_id_of_epi {x : SimplexCategory} (i : x ⟶ x) [Epi i] : i = 𝟙 _ :=
  by
  suffices IsIso i from eq_id_of_isIso _
  apply isIso_of_bijective
  dsimp
  rw [Fintype.bijective_iff_surjective_and_card i.toOrderHom, ← epi_iff_surjective, eq_self_iff_true, and_true]
  infer_instance

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