instCartesianClosedSheafOfHasSheafifyOfFunctorOpposite

Mathlib.CategoryTheory.Sites.CartesianClosed

URI: https://scilib.ai/kg/mathlib#instCartesianClosedSheafOfHasSheafifyOfFunctorOpposite

Lean4

instance [HasSheafify J A] [CartesianMonoidalCategory A] [CartesianClosed (Cᵒᵖ ⥤ A)] : CartesianClosed (Sheaf J A) :=
  cartesianClosedOfReflective' (sheafToPresheaf _ _)
    { obj F := ⟨F.obj, (isSheaf_of_iso_iff F.2.choose_spec.some).1 (Sheaf.cond _)⟩
      map f := ⟨f⟩ } (Iso.refl _)

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

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

Разделы

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

Аффилиация

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