English
For X,Y light condensed and f: X ⟶ Y, f is epi iff for every LightProfinite S and every y ∈ Y(S), there exist S', φ:S' ⟶ S with φ surjective and x ∈ X(S') such that f_S'(x) = Y(φ)(y).
Русский
Для X,Y — светло-конденсированные и f: X ⟶ Y, f является эпиморфизмом тогда и только тогда, когда для каждого LightProfinite S и каждого y ∈ Y(S) существует S', φ:S' ⟶ S сюръективное и x ∈ X(S'), такое что f_S'(x) = Y(φ)(y).
LaTeX
$$$\text{Epi}(f) \iff \forall S:\text{LightProfinite},\; \forall y\in Y(S),\; \exists S', \phi:S'\to S\ (\text{Surjective}(\phi))\ (\exists x\in X(S')):\ f_{S'}(x) = Y(\phi)(y).$$$
Lean4
theorem epi_iff_locallySurjective_on_lightProfinite :
Epi f ↔
∀ (S : LightProfinite) (y : Y.val.obj ⟨S⟩),
(∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : X.val.obj ⟨S'⟩),
f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y) :=
by
rw [← isLocallySurjective_iff_epi']
exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f
