English
For U ≤ V, the image of I.ideal(V) along the restriction map equals I.ideal(U).
Русский
Для U ≤ V изображение I.ideal(V) по ограничению равняется I.ideal(U).
LaTeX
$$$ (I.ideal V).map (X.presheaf.map (homOfLE h).op).hom = I.ideal U $$$
Lean4
theorem map_ideal {U V : X.affineOpens} (h : U ≤ V) : (I.ideal V).map (X.presheaf.map (homOfLE h).op).hom = I.ideal U :=
by
rw [U.2.ideal_ext_iff]
intro x hxU
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩
have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)
rw [← I.map_ideal_basicOpen] at this
apply_fun Ideal.map (X.presheaf.germ (X.basicOpen g) x (hfg ▸ hxf)).hom at this
simp only [Ideal.map_map, ← CommRingCat.hom_comp, affineBasicOpen_coe, X.presheaf.germ_res] at this ⊢
simp only [homOfLE_leOfHom, TopCat.Presheaf.germ_res', this]
