familyOfElements

Mathlib.CategoryTheory.Sites.CoversTop

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements

Lean4

/-- A family of elements indexed by `Sieve.ofObjects Y X` that is induced by
`x : FamilyOfElementsOnObjects F Y`. See the equational lemma
`IsCompatible.familyOfElements_apply` which holds under the assumption `x.IsCompatible`. -/
noncomputable def familyOfElements (X : C) : Presieve.FamilyOfElements F (Sieve.ofObjects Y X).arrows := fun _ _ hf =>
  F.map hf.choose_spec.some.op (x _)

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

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

Разделы

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

Аффилиация

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