sheafify_isSheaf

Mathlib.CategoryTheory.Sites.ConcreteSheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.sheafify_isSheaf

English

If P is a sheaf, then the morphism to its sheafification is an isomorphism.

Русский

Если P - шеф, то морфизм к её шефификации является изоморфизмом.

LaTeX

$$isIso (toSheafification J P)$$

Lean4

theorem sheafify_isSheaf (P : Cᵒᵖ ⥤ D) : Presheaf.IsSheaf J (J.sheafify P) :=
  GrothendieckTopology.Plus.isSheaf_plus_plus _ _

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

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

Разделы

Аффилиация

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