effectiveEpi_tfae — Mathlib

English

For any profinite π: X ⟶ B, the following three properties are equivalent: EffectiveEpi π, Epi π, and surjectivity of π.

Русский

Для любого проективного отображения π: X ⟶ B три свойства — эффективная эпиморфность, эпиморфность и сюръективность — эквивалентны.

LaTeX

$$$\\mathrm{TFAE}\\,[\\mathrm{EffectiveEpi}(\\pi),\\mathrm{Epi}(\\pi),\\mathrm{Surjective}(\\pi)].$$$

Lean4

theorem effectiveEpi_tfae {B X : Profinite.{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π ↦ ⟨⟨CompHausLike.effectiveEpiStruct π hπ⟩⟩
  tfae_finish

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