English
Under a quasi-compact map f: X → Y and an affine open U ⊆ Y with certain affine preimages, the ideal on U after mapping equals the comap of the corresponding ideal in Y along the induced ring map.
Русский
При квазикмаппинге f: X → Y и афинном открытом U в Y с условиями на прообраз, идеал на U после отображения равен композиции (сжатии) соответствующего идеала через индуцированное отображение колец.
LaTeX
$$$ (I.map f).ideal U = (I.ideal ⟨_, H⟩).comap (f.app U).hom $$$
Lean4
theorem ideal_map (I : X.IdealSheafData) (f : X ⟶ Y) [QuasiCompact f] (U : Y.affineOpens) (H : IsAffineOpen (f ⁻¹ᵁ U)) :
(I.map f).ideal U = (I.ideal ⟨_, H⟩).comap (f.app U).hom :=
by
have : RingHom.ker (I.subschemeObjIso ⟨_, H⟩).inv.hom = ⊥ :=
RingHom.ker_coe_equiv (I.subschemeObjIso ⟨_, H⟩).symm.commRingCatIsoToRingEquiv
simp [map, ← RingHom.comap_ker, subschemeι_app _ ⟨_, H⟩, this, ← RingHom.ker_eq_comap_bot]
