pullback

Mathlib.CategoryTheory.Sites.IsSheafFor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.FamilyOfElements.pullback

Lean4

/-- Given a family of elements of a sieve `S` on `X`, and a map `Y ⟶ X`, we can obtain a
family of elements of `S.pullback f` by taking the same elements.
-/
def pullback (f : Y ⟶ X) (x : FamilyOfElements P (S : Presieve X)) : FamilyOfElements P (S.pullback f : Presieve Y) :=
  fun _ g hg => x (g ≫ f) hg

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

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

Разделы

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

Аффилиация

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