English
The map toBasicOpen is surjective: every section on a basic open is realized by some fraction in localization.
Русский
Отображение toBasicOpen сюръективно: каждая секция на базовом открытом реализуется как дробь в локализации.
LaTeX
$$$Function.Surjective (toBasicOpen\\, R\\, f)$$$
Lean4
theorem toBasicOpen_surjective (f : R) : Function.Surjective (toBasicOpen R f) :=
by
intro s
let ι : Type u := PrimeSpectrum.basicOpen f
choose a' h' iDh' hxDh' s_eq' using locally_const_basicOpen R (PrimeSpectrum.basicOpen f) s
obtain ⟨t, ht_cover'⟩ :=
(PrimeSpectrum.isCompact_basicOpen f).elim_finite_subcover (fun i : ι => PrimeSpectrum.basicOpen (h' i))
(fun i => PrimeSpectrum.isOpen_basicOpen)
-- Here, we need to show that our basic opens actually form a cover of `basicOpen f`
fun x hx => by rw [Set.mem_iUnion]; exact ⟨⟨x, hx⟩, hxDh' ⟨x, hx⟩⟩
simp only [← Opens.coe_iSup, SetLike.coe_subset_coe] at ht_cover'
obtain ⟨a, h, iDh, ht_cover, ah_ha, s_eq⟩ :=
normalize_finite_fraction_representation R (PrimeSpectrum.basicOpen f) s t a' h' iDh' ht_cover' s_eq'
clear s_eq' iDh' hxDh' ht_cover' a' h'
simp only [← SetLike.coe_subset_coe, Opens.coe_iSup] at ht_cover
replace ht_cover :
(PrimeSpectrum.basicOpen f : Set <| PrimeSpectrum R) ⊆
⋃ (i : ι) (x : i ∈ t), (PrimeSpectrum.basicOpen (h i) : Set _) :=
ht_cover
obtain ⟨n, hn⟩ : f ∈ (Ideal.span (h '' ↑t)).radical :=
by
rw [← PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, PrimeSpectrum.zeroLocus_span]
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl] at ht_cover
replace ht_cover : (PrimeSpectrum.zeroLocus { f })ᶜ ⊆ ⋃ (i : ι) (x : i ∈ t), (PrimeSpectrum.zeroLocus {h i})ᶜ :=
ht_cover
rw [Set.compl_subset_comm] at ht_cover
simp_rw [Set.compl_iUnion, compl_compl, ← PrimeSpectrum.zeroLocus_iUnion, ← Finset.set_biUnion_coe, ←
Set.image_eq_iUnion] at ht_cover
apply PrimeSpectrum.vanishingIdeal_anti_mono ht_cover
exact PrimeSpectrum.subset_vanishingIdeal_zeroLocus { f } (Set.mem_singleton f)
replace hn := Ideal.mul_mem_right f _ hn
rw [← pow_succ, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hn
rcases hn with ⟨b, b_supp, hb⟩
rw [Finsupp.linearCombination_apply_of_mem_supported R b_supp] at hb
dsimp at hb
use IsLocalization.mk' (Localization.Away f) (∑ i ∈ t, b i * a i) (⟨f ^ (n + 1), n + 1, rfl⟩ : Submonoid.powers _)
rw [toBasicOpen_mk']
-- Since the structure sheaf is a sheaf, we can show the desired equality locally.
-- Annoyingly, `Sheaf.eq_of_locally_eq'` requires an open cover indexed by a *type*, so we need to
-- coerce our finset `t` to a type first.
let tt := ((t : Set (PrimeSpectrum.basicOpen f)) : Type u)
apply
(structureSheaf R).eq_of_locally_eq' (fun i : tt => PrimeSpectrum.basicOpen (h i)) (PrimeSpectrum.basicOpen f)
fun i : tt => iDh i
· -- This feels a little redundant, since already have `ht_cover` as a hypothesis
-- Unfortunately, `ht_cover` uses a bounded union over the set `t`, while here we have the
-- Union indexed by the type `tt`, so we need some boilerplate to translate one to the other
intro x hx
rw [SetLike.mem_coe, TopologicalSpace.Opens.mem_iSup]
have := ht_cover hx
rw [← Finset.set_biUnion_coe, Set.mem_iUnion₂] at this
rcases this with ⟨i, i_mem, x_mem⟩
exact ⟨⟨i, i_mem⟩, x_mem⟩
rintro ⟨i, hi⟩
dsimp
change (structureSheaf R).1.map (iDh i).op _ = (structureSheaf R).1.map (iDh i).op _
rw [s_eq i hi, res_const]
-- Again, `res_const` spits out an additional goal
swap
· intro y hy
change y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))
rw [PrimeSpectrum.basicOpen_pow f (n + 1) (by cutsat)]
exact (leOfHom (iDh i) :) hy
apply const_ext
rw [← hb, Finset.sum_mul, Finset.mul_sum]
apply Finset.sum_congr rfl
intro j hj
rw [mul_assoc, ah_ha j hj i hi]
ring
