W_toSheafify

Mathlib.CategoryTheory.Sites.Localization

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

English

W of the sheafification map equals W of the adjunction unit, i.e., W(toSheafify J P) holds.

Русский

W для отображения преобразования в шейф, то есть J.W(toSheafify J P).

LaTeX

$$$J.W(\mathrm{toSheafify}(J, P)).$$$

Lean4

theorem W_toSheafify (P : Cᵒᵖ ⥤ A) : J.W (toSheafify J P) :=
  J.W_adj_unit_app (sheafificationAdjunction J A) P

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

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

Разделы

Аффилиация

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