overPullback — Mathlib

English

For any X, Y and a morphism f: X → Y, the map Over.map f preserves coverings between J.over X and J.over Y.

Русский

Для любых объектов X, Y и морфизма f: X → Y отображение Over.map f сохраняет покрытия между J.over X и J.over Y.

LaTeX

$$$\\forall X\\,Y\\;f:\\,X\\to Y\\;\\mathrm{CoverPreserving}\\ (J.\\mathrm{over}\\,X)\\ (J.\\mathrm{over}\\,Y)\\ (\\mathrm{Over.map}\\ f)$$$

Lean4

/-- The pullback functor `Sheaf J A ⥤ Sheaf (J.over X) A` -/
abbrev overPullback (A : Type u') [Category.{v'} A] (X : C) : Sheaf J A ⥤ Sheaf (J.over X) A :=
  (Over.forget X).sheafPushforwardContinuous _ _ _

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