English
At a prime corresponding to a point of an affine open, the stalk is a localization at that prime.
Русский
На прайме, соответствующем точке аффинного открытого, stalk является локализацией по этому прайму.
LaTeX
$$$IsLocalization.AtPrime$$$
Lean4
/-- In an affine open set `U`, a family of basic open covers `U` iff the sections span `Γ(X, U)`.
See `iSup_basicOpen_of_span_eq_top` for the inverse direction without the affine-ness assumption.
-/
theorem basicOpen_union_eq_self_iff (s : Set Γ(X, U)) : ⨆ f : s, X.basicOpen (f : Γ(X, U)) = U ↔ Ideal.span s = ⊤ :=
by
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
· trans hU.fromSpec.base ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec.base ⁻¹' U.1
· refine ⟨fun h => by rw [h], ?_⟩
intro h
apply_fun Set.image hU.fromSpec.base at h
rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec] at h
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
ext1
refine Set.Subset.antisymm ?_ h
simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
intro x _
exact X.basicOpen_le x
· simp only [Opens.iSup_def, Set.preimage_iUnion]
congr! 1
· refine congr_arg (Set.iUnion ·) ?_
ext1 x
exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)
· exact congr_arg Opens.carrier hU.fromSpec_preimage_self
· simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.setOf_mem_eq]
