English
There is a definable predicate on sections over open subsets U of Spec R that characterizes being a local fraction: a section f is a local fraction if and only if there exist m in M and s in R such that for every x in U, s does not vanish on the localization at x and s·f equals the localization of m.
Русский
Существует предикат на секциях над открытым подмножеством U спектра, который характеризует существование дроби: f есть дробь на U тогда и только тогда существуют m ∈ M и s ∈ R такие, что для каждого x ∈ U, s не обращается в ноль в локализации на x и s·f равняется локализации m.
LaTeX
$$$\forall U: \text{Opens}(\mathrm{PrimeSpectrum.Top}\,R),\; f: U \to \mathrm{Localizations}\,M,\; (\text{isLocallyFraction}\,M).pred\,f = \cdots$$$
Lean4
@[simp]
theorem isLocallyFraction_pred {U : Opens (PrimeSpectrum.Top R)} (f : ∀ x : U, Localizations M x) :
(isLocallyFraction M).pred f =
∀ y : U,
∃ (V : _) (_ : y.1 ∈ V) (i : V ⟶ U),
∃ (m : M) (s : R),
∀ x : V, s ∉ x.1.asIdeal ∧ s • f (i x) = LocalizedModule.mkLinearMap x.1.asIdeal.primeCompl M m :=
rfl
