map_restrict — Mathlib

English

For a morphism f and a presheaf F, the pushforward map on morphisms corresponds to the map on sections after applying Opens.map f.

Русский

Для морфизма f и расш. F отображение pushforward между морфизмами соответствует отображению секций после применения Opens.map f.

LaTeX

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

Lean4

theorem map_restrict {F G : X.Presheaf C} (e : F ⟶ G) {U V : Opens X} (h : U ≤ V) (x : ToType (F.obj (op V))) :
    e.app _ (x |_ U) = e.app _ x |_ U := by
  delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, NatTrans.naturality, ConcreteCategory.comp_apply]

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