instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify

Mathlib.CategoryTheory.Sites.Sheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify

Lean4

instance [HasWeakSheafify J A] : Reflective (sheafToPresheaf J A)
    where
  L := presheafToSheaf J A
  adj := sheafificationAdjunction _ _

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

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

Разделы

Аффилиация

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