effectiveEpi_tfae — Mathlib

English

For a morphism π in CompHaus, the following are equivalent: π is effective epi, π is epi, and π is surjective.

Русский

Для морфизма π в CompHaus выполняются эквивалентности: π — эффективный эпиморфизм, π — эпиморфизм, и π — сюръективен.

LaTeX

$$$\mathrm{EffectiveEpi}(\pi) \iff \mathrm{EPI}(\pi) \iff \mathrm{Surjective}(\pi)$$$

Lean4

theorem effectiveEpi_tfae {B X : CompHaus.{u}} (π : X ⟶ B) : TFAE [EffectiveEpi π, Epi π, Function.Surjective π] :=
  by
  tfae_have 1 → 2 := fun _ ↦ inferInstance
  tfae_have 2 ↔ 3 := epi_iff_surjective π
  tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩
  tfae_finish

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