English
There is a precise description of how the images of basic opens behave under glueDataObjMap, in terms of opens inside the affine basic opens.
Русский
Существует точное описание поведения изображений базовых открытых множеств под glueDataObjMap в терминах открытых подмножеств внутри афинного базового открытого множества.
LaTeX
$$$ (I.glueDataObjMap (X.affineBasicOpen_le f)).opensRange = \\dots $$$
Lean4
theorem isLocalization_away {U V : X.affineOpens} (h : U ≤ V) (f : Γ(X, V.1)) (hU : U = X.affineBasicOpen f) :
letI := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal h)).toAlgebra
IsLocalization.Away (Ideal.Quotient.mk (I.ideal V) f) (Γ(X, U) ⧸ (I.ideal U)) :=
by
letI := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal h)).toAlgebra
let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f
letI := (X.presheaf.map (homOfLE (X := X.Opens) h).op).hom.toAlgebra
have : IsLocalization.Away f Γ(X, U) := by subst hU; exact V.2.isLocalization_of_eq_basicOpen _ _ rfl
simp only [IsLocalization.Away, ← Submonoid.map_powers]
refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _ Ideal.Quotient.mk_surjective ?_ ?_
· simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]; rfl
· simp only [Ideal.mk_ker, RingHom.algebraMap_toAlgebra, I.map_ideal', le_refl]
