English
A refinement of the previous equality showing functorial compatibility with the isomorphism basicOpenIsoSpec.
Русский
Уточнение равенства, показывающее совместимость по отношению к изоморфизму basicOpenIsoSpec.
LaTeX
$$awayι 𝒜 f f_deg hm ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 _))$$
Lean4
@[reassoc]
theorem awayMap_awayToSection :
CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x =
awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩)).op :=
by
ext a
apply Subtype.ext
ext ⟨i, hi⟩
obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a
simp only [homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
erw [ProjectiveSpectrum.Proj.awayToSection_apply]
rw [CommRingCat.hom_ofHom, val_awayMap_mk, Localization.mk_eq_mk', IsLocalization.map_mk', ← Localization.mk_eq_mk']
refine Localization.mk_eq_mk_iff.mpr ?_
rw [Localization.r_iff_exists]
use 1
simp only [OneMemClass.coe_one, RingHom.id_apply, one_mul, hx]
ring
