English
The morphism awayι composed with toSpecZero equals the canonical Spec map coming from the zero ring localization.
Русский
Гомоморфизм awayι в сочетании с toSpecZero равен каноническому отображению Spec, полученному из нулевой локализации кольца.
LaTeX
$$awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 _))$$
Lean4
@[reassoc]
theorem awayι_toSpecZero : awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 _)) :=
by
rw [toSpecZero, basicOpenToSpec, awayι]
simp only [Category.assoc, Iso.inv_comp_eq, basicOpenIsoSpec_hom]
have (U) (e : U = ⊤) :
(basicOpen 𝒜 f).ι ≫ (Scheme.topIso _).inv ≫ (Scheme.isoOfEq _ e).inv = Scheme.homOfLE _ (le_top.trans_eq e.symm) :=
by
simp only [← Category.assoc, Iso.comp_inv_eq]
simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]
rw [reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_map_assoc, basicOpenToSpec, Category.assoc, ← Spec.map_comp, ←
Spec.map_comp, ← Spec.map_comp]
rfl
