functorPushforward

Mathlib.CategoryTheory.Sites.IsSheafFor

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

Lean4

/-- Given a family of elements of a sieve `S` on `X` whose values factors through `F`, we can
realize it as a family of elements of `S.functorPushforward F`. Since the preimage is obtained by
choice, this is not well-defined generally.
-/
noncomputable def functorPushforward {D : Type u₂} [Category.{v₂} D] (F : D ⥤ C) {X : D} {T : Presieve X}
    (x : FamilyOfElements (F.op ⋙ P) T) : FamilyOfElements P (T.functorPushforward F) := fun Y f h =>
  by
  obtain ⟨Z, g, h, h₁, _⟩ := getFunctorPushforwardStructure h
  exact P.map h.op (x g h₁)

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

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

Разделы

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

Аффилиация

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