pushforward

Mathlib.Topology.Sheaves.Functors

URI: https://scilib.ai/kg/mathlib#TopCat.Sheaf.pushforward

English

The map on pushforward respects the underlying presheaf map.

Русский

Отображение переноса поддерживает отображение прешейфа.

LaTeX

$$$((pushforward C f).map α).val = (Presheaf.pushforward C f).map α.1$$$

Lean4

/-- The pushforward functor.
-/
def pushforward (f : X ⟶ Y) : X.Sheaf C ⥤ Y.Sheaf C :=
  (Opens.map f).sheafPushforwardContinuous _ _ _

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

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

Разделы

Аффилиация

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