instIsLocalizationFunctorOppositeSheafPresheafToSheafW

Mathlib.CategoryTheory.Sites.Localization

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

← MathLib Explorer

English

The functor presheafToSheaf J A is a localization with respect to W.

Русский

Функтор presheafToSheaf J A образует локализацию по отношению к W.

LaTeX

$$$(\mathrm{presheafToSheaf}(J,A)).IsLocalization(J.W).$$$

Lean4

instance : (presheafToSheaf J A).IsLocalization J.W :=
  by
  rw [W_eq_inverseImage_isomorphisms]
  exact (sheafificationAdjunction J A).isLocalization

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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