glueDataObjι_ι — Mathlib

English

The base of the glued data morphism is precisely the image of the zero locus under the quotient by I(ideal).

Русский

База отображения glueDataObjι равна образу нулевого множества по фактор-модуля по I.

LaTeX

$$$ \\text{range }(I.glueDataObjι U).base = U.2.isoSpec.inv.base '' \\operatorname{PrimeSpectrum.zeroLocus}(I.ideal U) $$$

Lean4

theorem glueDataObjι_ι (U : X.affineOpens) :
    I.glueDataObjι U ≫ U.1.ι = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk _)) ≫ U.2.fromSpec := by
  rw [glueDataObjι, Category.assoc]; rfl

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