English
Given a graded algebra 𝒜 and a ring map f with the irrelevant ideal mapped to the whole ring, the collection of basic opens D(f(r)) for homogeneous r of positive degree forms an open cover of X.
Русский
При заданной градационной алгебре 𝒜 и отображении колец f, маппинг нерелевантного идеала к всему кольцу порождает открытое покрытие X базовыми открытыми D(f(r)) для однородных r положительной степени.
LaTeX
$$$ openCoverOfMapIrrelevantEqTop 𝒜 f hf : X.OpenCover $$$
Lean4
@[reassoc]
theorem homOfLE_toBasicOpenOfGlobalSections_ι {H : f t = x} {h0d : 0 < d} {hd : t ∈ 𝒜 d} {H' : f t' = x'}
{h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A} (hts : t * s = t') {n : ℕ} (hn : d + n = d') (hs : s ∈ 𝒜 n) :
X.homOfLE (by aesop) ≫ toBasicOpenOfGlobalSections 𝒜 f H h0d hd ≫ (basicOpen 𝒜 t).ι =
toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd' ≫ (basicOpen 𝒜 t').ι :=
by
simp only [toBasicOpenOfGlobalSections, Scheme.isoOfEq_inv, ← Scheme.Hom.resLE_eq_morphismRestrict,
CommRingCat.ofHom_comp, Spec.map_comp, Scheme.Hom.map_resLE_assoc, Category.assoc, basicOpenIsoSpec_inv_ι]
have hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x := by aesop (add simp PrimeSpectrum.basicOpen_mul)
rw [← Scheme.Hom.resLE_map_assoc _ (by simp [X.toSpecΓ_preimage_basicOpen]) hx'x]
congr 1
simp only [← Iso.inv_comp_eq]
subst hts hn
rw [← SpecMap_awayMap_awayι (𝒜 := 𝒜) hd h0d hs rfl,
basicOpenIsoSpecAway_inv_homOfLE_assoc (R := Γ(X, ⊤)) x (f s) x' (by simp [← H', H]), Iso.inv_hom_id_assoc]
simp only [← Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp]
congr 3
ext
simp only [RingHom.coe_comp, Function.comp_apply, HomogeneousLocalization.algebraMap_apply,
HomogeneousLocalization.val_awayMap]
simp only [← RingHom.comp_apply]
congr 1
apply IsLocalization.ringHom_ext (M := .powers t)
ext i
simp [IsLocalization.Away.awayToAwayRight_eq]
