English
For R-modules: epi_iff_locallySurjective_on_lightProfinite states that an epi in LightCondensed modules is equivalent to a local surjectivity condition expressed via lifts through lightProfinite objects.
Русский
Для модулей R: утверждение epi_iff_locallySurjective_on_lightProfinite утверждает, что эпиморфизм в LightCondensed модулях эквивалентен локальной сюръективности, выраженной через подъёмы через объекты lightProfinite.
LaTeX
$$$\text{Epi}(f) \iff \text{LocallySurjective}(f) \text{ on LightProfinite.}$$$
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
