familyOfElementsOfSection

Mathlib.CategoryTheory.Subpresheaf.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.familyOfElementsOfSection

Lean4

/-- Given an `F`-section `s` on `U` and a subpresheaf `G`, we may define a family of elements in
`G` consisting of the restrictions of `s` -/
def familyOfElementsOfSection {U : Cᵒᵖ} (s : F.obj U) : (G.sieveOfSection s).1.FamilyOfElements G.toPresheaf :=
  fun _ i hi => ⟨F.map i.op s, hi⟩

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

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

Разделы

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

Аффилиация

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