ideal_comap_of_isOpenImmersion — Mathlib

English

If f is an open immersion, the comap of the ideal under f equals the comap of the closed subscheme-ideal under the corresponding preimage.

Русский

Если f — открытое внедрение, то перенос идеала через f равен переносу через соответствующее обратное изображение для закрытых подсхем.

LaTeX

$$$ (I.comap f).ideal U = (I.ideal ⟨f ''ᵁ U, U.2.image_of_isOpenImmersion f⟩).comap (f.appIso U).inv.hom $$$

Lean4

theorem ideal_comap_of_isOpenImmersion (I : Y.IdealSheafData) (f : X ⟶ Y) [IsOpenImmersion f] (U : X.affineOpens) :
    (I.comap f).ideal U = (I.ideal ⟨f ''ᵁ U, U.2.image_of_isOpenImmersion f⟩).comap (f.appIso U).inv.hom :=
  by
  refine (ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _ (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_
  simp

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