English
Let f: X → Y be a morphism of schemes. For an open U ⊆ Y and an affine open V ⊆ U, the kernel of the restricted morphism f|_U evaluated on V equals the kernel of f evaluated at the corresponding pullback data along the inclusion of V into Y via U.
Русский
Пусть f: X → Y — морфизм схем. Пусть U ⊆ Y — открытое, а V ⊆ U — аффайн-открытое. Тогда ядро ограниченного морфизма f|_U на V равно ядру f, рассчитанному через соответствующие данные вытяжки по включению V в Y через U.
LaTeX
$$$\operatorname{ker}(f|_U)_V = \operatorname{ker}(f)_{\langle U \hookrightarrow Y, V\rangle}$$$
Lean4
theorem ker_morphismRestrict_ideal (f : X.Hom Y) [QuasiCompact f] (U : Y.Opens) (V : U.toScheme.affineOpens) :
(f ∣_ U).ker.ideal V = f.ker.ideal ⟨U.ι ''ᵁ V, V.2.image_of_isOpenImmersion _⟩ :=
by
have inst : QuasiCompact (f ∣_ U) :=
MorphismProperty.of_isPullback (isPullback_morphismRestrict _ _).flip inferInstance
ext x
simpa [Scheme.Hom.appLE] using
map_eq_zero_iff _
(ConcreteCategory.bijective_of_isIso (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1
