English
The range of the base of the composed map equals the intersection of the support of I with the affine open U.
Русский
Диапазон базового отображения композиции совпадает с пересечением поддержки I и открытого афинного U.
LaTeX
$$$ \\text{range }(I.glueDataObjι U ≫ U.1.ι).base = (I.support : Set X) \\cap U $$$
Lean4
theorem ker_glueDataObjι_appTop (U : X.affineOpens) :
RingHom.ker (I.glueDataObjι U).appTop.hom = (I.ideal U).comap U.1.topIso.hom.hom :=
by
let φ := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
rw [← Ideal.mk_ker (I := I.ideal _)]
change RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _
rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp, ← CommRingCat.hom_comp]
congr 2
simp only [Scheme.comp_app, TopologicalSpace.Opens.map_top, Category.assoc, Scheme.ΓSpecIso_naturality,
Scheme.Opens.topIso_hom]
rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]
simp only [Scheme.Opens.topIso_hom]
