English
Any section on an open set can be locally represented on a basic open by a constant function coming from R.
Русский
Любая секция на открытом множестве локально представима на базовом открытом константой, восходящей к R.
LaTeX
$$$\\exists f,g,iDh$ such that $\\text{const } f g (\\text{basicOpen } g) = (structureSheaf R).1.map(i^op)\\; s$.$$
Lean4
theorem locally_const_basicOpen (U : Opens (PrimeSpectrum.Top R)) (s : (structureSheaf R).1.obj (op U)) (x : U) :
∃ (f g : R) (i : PrimeSpectrum.basicOpen g ⟶ U),
x.1 ∈ PrimeSpectrum.basicOpen g ∧
(const R f g (PrimeSpectrum.basicOpen g) fun _ hy => hy) = (structureSheaf R).1.map i.op s :=
by
-- First, any section `s` can be represented as a fraction `f/g` on some open neighborhood of `x`
-- and we may pass to a `basicOpen h`, since these form a basis
obtain ⟨V, hxV : x.1 ∈ V.1, iVU, f, g, hVDg : V ≤ PrimeSpectrum.basicOpen g, s_eq⟩ := exists_const R U s x.1 x.2
obtain ⟨_, ⟨h, rfl⟩, hxDh, hDhV : PrimeSpectrum.basicOpen h ≤ V⟩ :=
PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open hxV
V.2
-- The problem is of course, that `g` and `h` don't need to coincide.
-- But, since `basicOpen h ≤ basicOpen g`, some power of `h` must be a multiple of `g`
obtain ⟨n, hn⟩ :=
(PrimeSpectrum.basicOpen_le_basicOpen_iff h g).mp
(Set.Subset.trans hDhV hVDg)
-- Actually, we will need a *nonzero* power of `h`.
-- This is because we will need the equality `basicOpen (h ^ n) = basicOpen h`, which only
-- holds for a nonzero power `n`. We therefore artificially increase `n` by one.
replace hn := Ideal.mul_mem_right h (Ideal.span { g }) hn
rw [← pow_succ, Ideal.mem_span_singleton'] at hn
obtain ⟨c, hc⟩ := hn
have basic_opens_eq := PrimeSpectrum.basicOpen_pow h (n + 1) (by cutsat)
have i_basic_open := eqToHom basic_opens_eq ≫ homOfLE hDhV
use f * c, h ^ (n + 1), i_basic_open ≫ iVU, (basic_opens_eq.symm.le :) hxDh
rw [op_comp, Functor.map_comp, ConcreteCategory.comp_apply, ← s_eq, res_const]
-- Note that the last rewrite here generated an additional goal, which was a parameter
-- of `res_const`. We prove this goal first
swap
· intro y hy
rw [basic_opens_eq] at hy
exact (Set.Subset.trans hDhV hVDg :) hy
apply const_ext
rw [mul_assoc f c g, hc]
/-
Auxiliary lemma for surjectivity of `toBasicOpen`.
A local representation of a section `s` as fractions `a i / h i` on finitely many basic opens
`basicOpen (h i)` can be "normalized" in such a way that `a i * h j = h i * a j` for all `i, j`
-/
