epi_iff_surjective_on_stonean — Mathlib

English

Let f: X → Y be a morphism of CondensedSet. Then f is an epimorphism if and only if for every Stonean object S, the induced map on the evaluation at S, f_S: X(S) → Y(S), is surjective.

Русский

Пусть f: X → Y — морофизм CondensedSet. Тогда f является эпиморфизмом тогда и только тогда, когда для каждого объекта Stonean S отображение f_S: X(S) → Y(S) является сюръективным.

LaTeX

$$$$\operatorname{Epi}(f) \iff \forall S \in \mathrm{Stonean}, \; \operatorname{Surjective}(f_S)$$$$

Lean4

theorem epi_iff_surjective_on_stonean : Epi f ↔ ∀ (S : Stonean), Function.Surjective (f.val.app (op S.compHaus)) :=
  Condensed.epi_iff_surjective_on_stonean _ f

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