pushforward — Mathlib

English

A variant of the pushforward that records explicit behavior on app at an open U.

Русский

Вариант pushforward, фиксирующий поведение на применении к открытому множеству U.

LaTeX

$$((pushforward C f).map α).app U = α.app (op ((Opens.map f).obj U.unop))$$

Lean4

/-- The pushforward functor. -/
@[simps!]
def pushforward {X Y : TopCat.{w}} (f : X ⟶ Y) : X.Presheaf C ⥤ Y.Presheaf C :=
  (whiskeringLeft _ _ _).obj (Opens.map f).op

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