English
Let f: X → Y be a morphism in CondensedMod R. Then f is epi if and only if for every CompHaus S and every y ∈ Y(S), there exists a surjective φ: S' → S and x ∈ X(S') with f_S'(x) = Y(φ)(y).
Русский
Пусть f: X → Y — морфизм в CondensedMod R. Тогда f является эпиморфизмом эквивалентно тому, что для каждого CompHaus S и каждого y ∈ Y(S) существует сюръективный картовый переход φ: S' → S и элемент x ∈ X(S') такой, что f_S'(x) = Y(φ)(y).
LaTeX
$$$$\operatorname{Epi}(f) \iff \forall (S: \mathrm{CompHaus})\ (y \in Y( S )), \; \exists (S': \mathrm{CompHaus}) (\varphi: S' \to S) (h: \operatorname{Surjective}(\varphi)) (x \in X(S')), \\ f_{S'}(x) = Y(\varphi)(y).$$$$
Lean4
theorem epi_iff_locallySurjective_on_compHaus :
Epi f ↔
∀ (S : CompHaus) (y : Y.val.obj ⟨S⟩),
(∃ (S' : CompHaus) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : X.val.obj ⟨S'⟩),
f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y) :=
Condensed.epi_iff_locallySurjective_on_compHaus _ f
