_example

Mathlib.CategoryTheory.Sites.PreservesSheafification

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

Lean4

example {D : Type*} [Category.{max v u} D] {FD : D → D → Type*} {CD : D → Type (max v u)}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{max v u} D FD] [PreservesLimits (forget D)]
    [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)]
    [∀ (J : MulticospanShape.{max v u, max v u}), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D]
    [(forget D).ReflectsIsomorphisms] : PreservesSheafification J (forget D) :=
  instPreservesSheafification _ _

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

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

Разделы

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

Аффилиация

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