natTransΓRes

Mathlib.CategoryTheory.Sites.GlobalSections

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

Lean4

/-- The natural transformation from the global sections functor to the sections functor on any
object `U`. -/
@[simps!]
noncomputable def natTransΓRes [HasGlobalSectionsFunctor J A] (U : Cᵒᵖ) : Γ J A ⟶ (sheafSections J A).obj U
    where
  app F := ΓRes F U
  naturality _ _ f := ΓRes_naturality f U

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

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

Разделы

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

Аффилиация

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