epi_iff_surjective_on_stonean — Mathlib

English

The Condensed epi criterion transfers to Stonean and presheaf contexts.

Русский

Критерий эпиморфизма переноится на контекст Stonean и прешефа.

LaTeX

$$$\\mathrm{epi\\_iff\\_surjective\\_on\\_stonean}(f)$$$

Lean4

theorem epi_iff_surjective_on_stonean : Epi f ↔ ∀ (S : Stonean), Function.Surjective (f.val.app (op S.compHaus)) :=
  by
  rw [← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi, ←
    Presheaf.coherentExtensiveEquivalence.functor.epi_map_iff_epi, ← isLocallySurjective_iff_epi']
  exact extensiveTopology.isLocallySurjective_iff (D := A) _

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