epi_of_presheaf_epi

Mathlib.CategoryTheory.Sites.Sheaf

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

English

If e: P ≅ P' is an isomorphism of presheaves, then P is a sheaf iff P' is a sheaf.

Русский

Если e: P ≅ P' — изоморфизм прешейфа, то P шейф тогда и только тогда P' шейф.

LaTeX

$$$P \\cong P' \\Longrightarrow (\\mathrm{IsSheaf} J\\, P \\iff \\mathrm{IsSheaf} J\\, P').$$$

Lean4

instance epi_of_presheaf_epi {F G : Sheaf J A} (f : F ⟶ G) [h : Epi f.1] : Epi f :=
  (sheafToPresheaf J A).epi_of_epi_map h

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

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

Разделы

Аффилиация

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