English
The inverse of the forward part of pullbackAwayιIso composed with snd yields the awayMap on the right side.
Русский
Обратный образ forward части pullbackAwayιIso, композиция с snd, даёт awayMap справа.
LaTeX
$$$(pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv \\circ \\mathrm{Limits.pullback.snd} = \\mathrm{awayMap}(𝒜, f_deg, hx)$$$
Lean4
/-- Given a graded ring `A` and a map `f : A →+* Γ(X, ⊤)`,
for each homogeneous `t` of positive degree, it induces a map from `D(f(t)) ⟶ D₊(t)`. -/
def toBasicOpenOfGlobalSections (H : f t = x) (h0d : 0 < d) (hd : t ∈ 𝒜 d) : (X.basicOpen x).toScheme ⟶ basicOpen 𝒜 t :=
by
refine ?_ ≫ (basicOpenIsoSpec _ _ hd h0d).inv
refine (X.isoOfEq (X.toSpecΓ_preimage_basicOpen x)).inv ≫ X.toSpecΓ ∣_ _ ≫ ?_
refine
(basicOpenIsoSpecAway _).hom ≫ Spec.map (CommRingCat.ofHom (RingHom.comp ?_ (algebraMap _ (Localization.Away t))))
refine IsLocalization.map (M := .powers t) (T := .powers x) _ f ?_
· rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_powers]
simp [H]
