English
Let f: X → Y be a morphism in CondensedMod R. Then epi f if and only if for every Stonean S, the map f_S: X(S) → Y(S) is surjective, where S is viewed through compHaus and the module-structure is respected.
Русский
Пусть f: X → Y — морфизм в CondensedMod R. Тогда f эпиморфизм тогда и только тогда, когда для каждого Stonean S отображение f_S: X(S) → Y(S) сюръективно, причём S рассматривается через compHaus и учитывается модульная структура.
LaTeX
$$$$\operatorname{Epi}(f) \iff \forall S \in \mathrm{Stonean}, \; \operatorname{Surjective}\big(f_S\big).$$$$
Lean4
theorem epi_iff_surjective_on_stonean : Epi f ↔ ∀ (S : Stonean), Function.Surjective (f.val.app (op S.compHaus)) :=
have : HasLimitsOfSize.{u, u + 1} (ModuleCat R) := hasLimitsOfSizeShrink.{u, u + 1, u + 1, u + 1} _
Condensed.epi_iff_surjective_on_stonean _ f
