epi_of_isLocallySurjective

Mathlib.CategoryTheory.Sites.LocallySurjective

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.epi_of_isLocallySurjective

English

For a presheaf morphism f between Type w presheaves, IsLocallySurjective f is equivalent to IsIso (imageι f).

Русский

Для морфизма прешефов типа Type w IsLocallySurjective f эквивалентно IsIso (imageι f).

LaTeX

$$$\text{IsLocallySurjective}_J(f) \iff \text{IsIso}(\mathrm{imageι}(f))$$$

Lean4

instance epi_of_isLocallySurjective [IsLocallySurjective φ] : Epi φ :=
  (sheafCompose J (forget A)).epi_of_epi_map inferInstance

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru