English
The opensRange under glueDataObjMap composed with glueDataObjι matches the opens described by preimages through isomorphisms.
Русский
opensRange под glueDataObjMap после glueDataObjι совпадает с открытыми, заданными предобразами через изоморфизмы.
LaTeX
$$$ (I.glueDataObjMap ⋯).opensRange = (TopologicalSpace.Opens.map (I.glueDataObjι ⋯).base).obj (X.basicOpen f) $$$
Lean4
theorem opensRange_glueDataObjMap {V : X.affineOpens} (f : Γ(X, V.1)) :
(I.glueDataObjMap (X.affineBasicOpen_le f)).opensRange = (I.glueDataObjι V) ⁻¹ᵁ (V.1.ι ⁻¹ᵁ X.basicOpen f) :=
by
letI := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f
have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
ext1
refine (localization_away_comap_range _ f').trans ?_
rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen, ← Scheme.preimage_comp, glueDataObjι_ι]
rfl