morphismRestrict_base — Mathlib

English

The base map of the restricted morphism equals the restricted base map up to the natural identifications of the open embedding.

Русский

Базовая карта ограниченного морфизма совпадает с ограниченной базовой картой через естественные изоморфизмы открытого внедрения.

LaTeX

$$$ (f|_U).base = U.1.restrictPreimage( f.base)$$$

Lean4

theorem morphismRestrict_base {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    ⇑(f ∣_ U).base = U.1.restrictPreimage f.base :=
  funext fun x => Subtype.ext (morphismRestrict_base_coe f U x)

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