English
The range of the base of the composed glue data morphism equals the intersection of the ambient space with the zero locus of I.ideal.
Русский
Диапазон базы композиции glueDataObjι U ≫ ι равен пересечению среды пространства с нулевой локусом I.ideal.
LaTeX
$$$ \\text{range }(I.glueDataObjι U ≫ U.1.ι).base = X.zeroLocus (Submodule.setLike.coe (I.ideal U)) \\cap U $$$
Lean4
theorem range_glueDataObjι_ι (U : X.affineOpens) :
Set.range ⇑(I.glueDataObjι U ≫ U.1.ι).base = X.zeroLocus (U := U) (I.ideal U) ∩ U :=
by
simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp, range_glueDataObjι]
rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.comp_base, IsAffineOpen.isoSpec_inv_ι,
IsAffineOpen.fromSpec_image_zeroLocus]