English
Let M be a module object over a commutative ring R and U an open subset of the prime spectrum of R. For any section s of the tilde construction over U and any point x ∈ U, there exists a smaller open V ⊆ U containing x, together with a morphism i: V → U and elements f ∈ M, g ∈ R so that the localized constant section on V matches the image of s under i, and the matching is determined fiberwise by a compatible local expression.
Русский
Пусть M — модуль над кольцом R и U — открытое множество в прайм спектре R. Для любой секции s модуля на U в конструкции tilde и любой точке x ∈ U существует более маленькое открытое V ⊆ U, содержащее x, отображение i: V → U и элементы f ∈ M, g ∈ R так, что локализованная константная секция на V совпадает с образом s через i, причём совпадение задаётся покомпонентно локальным выражением.
LaTeX
$$$\\forall U \\subseteq \\mathrm{PrimeSpectrum.Top}(R),\\; s \\in (\\tilde{M})\\text{.obj}(op U),\\; x \\in U,\\; x \\in U \\Rightarrow \\exists (V \\in \\mathrm{Opens}(\\mathrm{PrimeSpectrum.Top}(R))) (x \\in V) (i: V \\to U) (f \\in M) (g \\in R) (hg : _) ,\\; \\text{const } M f g V hg = (\\tilde{M}).map i^{op} s$,$$
Lean4
theorem exists_const (U) (s : (tildeInModuleCat M).obj (op U)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
∃ (V : Opens (PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : M) (g : R) (hg : _),
const M f g V hg = (tildeInModuleCat M).map i.op s :=
let ⟨V, hxV, iVU, f, g, hfg⟩ := s.2 ⟨x, hx⟩
⟨V, hxV, iVU, f, g, fun y hyV => (hfg ⟨y, hyV⟩).1,
Subtype.eq <|
funext fun y => by
obtain ⟨h1, (h2 : g • s.1 ⟨y, _⟩ = LocalizedModule.mk f 1)⟩ := hfg y
exact
show LocalizedModule.mk f ⟨g, by exact h1⟩ = s.1 (iVU y)
by
set x := s.1 (iVU y); change g • x = _ at h2; clear_value x
induction x using LocalizedModule.induction_on with
| h a b =>
rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] at h2
obtain ⟨c, hc⟩ := h2
exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩⟩
