English
Let X,Y be LightCondensed objects over some category and f: X ⟶ Y. Then f is locally surjective 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 — LightCondensed объекты, f: X ⟶ Y. Тогда f локально сюръективен тогда и только тогда, когда для каждого LightProfinite S и каждого y ∈ Y(S) существует S', φ:S' ⟶ S с сюрьективным φ и x ∈ X(S'), такое что f_S'(x) = Y(φ)(y).
LaTeX
$$$\text{LocallySurjective}(f) \iff \forall S\in \text{LightProfinite},\; 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 isLocallySurjective_iff_locallySurjective_on_lightProfinite :
IsLocallySurjective f ↔
∀ (S : LightProfinite) (y : ToType (Y.val.obj ⟨S⟩)),
(∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : ToType (X.val.obj ⟨S'⟩)),
f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y) :=
by
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff]
simp_rw [LightProfinite.effectiveEpi_iff_surjective]
