ΓNatIsoLim

Mathlib.CategoryTheory.Sites.GlobalSections

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.ΓNatIsoLim

Lean4

/-- Global sections of sheaves are naturally isomorphic to the limits of the underlying presheaves.
Note that while `HasLimitsOfShape Cᵒᵖ A` is needed here to talk about `lim` as a functor, global
sections are still limits without it - see `Sheaf.isLimitConeΓ`. -/
noncomputable def ΓNatIsoLim [HasLimitsOfShape Cᵒᵖ A] : Γ J A ≅ sheafToPresheaf J A ⋙ lim :=
  (constantSheafΓAdj J A).rightAdjointUniq (constLimAdj.comp (sheafificationAdjunction J A))

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

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

Разделы

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

Аффилиация

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