English
The composition of the forward map with the Spec-structure map equals X mapped to Spec Γ(X, O_X) via the ring hom f, i.e., the forward map to Spec A⁰_f respects Spec-structure.
Русский
Композиция прямого отображения с отображением в Spec нейтрализуется через спектр Γ(X, O_X) по кольцо f; то есть построение совместимо со структурой Spec.
LaTeX
$$$(fromOfGlobalSections 𝒜 f hf) \circ toSpecZero 𝒜 = X.toSpecΓ \circ Spec.map (f)$.$$
Lean4
@[reassoc]
theorem fromOfGlobalSections_toSpecZero (f : A →+* Γ(X, ⊤)) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal.map f = ⊤) :
fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜 = X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap _ _))) :=
by
refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_
simp only [fromOfGlobalSections, toBasicOpenOfGlobalSections, CommRingCat.ofHom_comp, Category.assoc,
Scheme.Cover.ι_glueMorphisms_assoc, basicOpenIsoSpec_inv_ι_assoc, awayι_toSpecZero, Iso.inv_comp_eq]
simp only [openCoverOfMapIrrelevantEqTop, Scheme.openCoverOfIsOpenCover_X, Scheme.openCoverOfIsOpenCover_f,
Scheme.isoOfEq_hom_ι_assoc, ← morphismRestrict_ι_assoc]
congr 1
simp only [basicOpenIsoSpecAway, ← CommRingCat.ofHom_comp, ← Spec.map_comp, ← Iso.eq_inv_comp,
IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, ← HomogeneousLocalization.algebraMap_eq]
congr 2
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ A, ← RingHom.comp_assoc,
IsLocalization.map_comp, RingHom.comp_assoc]
