English
For r ∈ 𝒜(n) with n ≥ 1, the preimage of the basic open basicOpen 𝒜(r) along the morphism fromOfGlobalSections coincides with the basic open X.basicOpen(f(r)).
Русский
Для элемента r ∈ 𝒜(n) с n ≥ 1, прообраз базовой открытой ∖basicOpen∖(𝒜 r) по морфизму fromOfGlobalSections равен базовой открытой X.basicOpen(f(r)).
LaTeX
$$$\forall r\in\mathcal A(n),\; n>0:\quad (\text{fromOfGlobalSections }\mathcal A f hf)^{-1}(\text{basicOpen}_\mathcal A(r)) = X\text{.basicOpen}(f(r)).$$$
Lean4
theorem fromOfGlobalSections_preimage_basicOpen {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) :
fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r = X.basicOpen (f r) :=
by
apply le_antisymm
· intro x hx
obtain ⟨i, x, rfl⟩ := (openCoverOfMapIrrelevantEqTop 𝒜 f hf).exists_eq x
simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, ← Scheme.comp_base_apply,
fromOfGlobalSections, Scheme.Cover.ι_glueMorphisms] at hx
simp only [openCoverOfMapIrrelevantEqTop, Scheme.openCoverOfIsOpenCover_X, toBasicOpenOfGlobalSections,
Scheme.isoOfEq_inv, Category.assoc, basicOpenIsoSpec_inv_ι] at hx
simp only [Scheme.comp_coeBase, Scheme.homOfLE_base, homOfLE_leOfHom, TopCat.hom_comp, ContinuousMap.comp_assoc,
ContinuousMap.comp_apply, morphismRestrict_base, TopologicalSpace.Opens.carrier_eq_coe] at hx
rw [← SetLike.mem_coe, ← Set.mem_preimage, ← TopologicalSpace.Opens.map_coe,
Proj.awayι_preimage_basicOpen (𝒜 := 𝒜) i.2.2.2 i.2.2.1 hr hn, ← Set.mem_preimage, ←
TopologicalSpace.Opens.map_coe, ←
Function.Injective.mem_set_image (Spec.map (CommRingCat.ofHom (algebraMap Γ(X, ⊤) _))).isOpenEmbedding.injective,
← Scheme.comp_base_apply, basicOpenIsoSpecAway, IsOpenImmersion.isoOfRangeEq_hom_fac] at hx
rw [← Scheme.toSpecΓ_preimage_basicOpen, TopologicalSpace.Opens.map_coe, Set.mem_preimage]
refine Set.mem_of_subset_of_mem (Set.image_subset_iff.mpr ?_) hx
change PrimeSpectrum.basicOpen _ ≤ PrimeSpectrum.basicOpen _
simp only [CommRingCat.ofHom_comp, CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp,
Function.comp_apply, HomogeneousLocalization.algebraMap_apply, HomogeneousLocalization.Away.val_mk,
Localization.mk_eq_mk', IsLocalization.map_mk', map_pow, PrimeSpectrum.basicOpen_le_basicOpen_iff,
IsLocalization.mk'_mem_iff]
exact Ideal.pow_mem_of_mem _ (Ideal.le_radical (Ideal.mem_span_singleton_self _)) _ i.2.2.1
· intro x hx
let I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, r, hn, hr⟩
obtain ⟨x, rfl⟩ : x ∈ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I).opensRange := by
simpa [openCoverOfMapIrrelevantEqTop] using hx
simp only [TopologicalSpace.Opens.map_coe, Set.mem_preimage, SetLike.mem_coe, ← Scheme.comp_base_apply,
fromOfGlobalSections, Scheme.Cover.ι_glueMorphisms]
simp
