range_glueDataObjι_ι — Mathlib

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]

Похожие утверждения