English
Let R be a commutative ring, s a subset of R, and for every t in s a set p(t) of fractions in a localization of R at t. Define a map mulNumerator(s, p) that sends a pair (t, y) with t in s and y in t a to t multiplied by a numerator of y. If the span of s is the whole ring and every p(t) spans the unit ideal, then the ideal generated by the range of mulNumerator equals the unit ideal.
Русский
Пусть R — коммутативное кольцо, s — подмножество R, и для каждого t ∈ s задано множество p(t) долей в локализации R в t. Определим отображение mulNumerator(s, p), которое отображает пару (t, y) с y ∈ t в t, умноженное на числитель дроби y, на единицу. Если порождающее s идеал равен всей топ-ткому, и каждый p(t) порождает единичный идеал, то порождающий этот образ mulNumerator образует единичный идеал.
LaTeX
$$$\forall R\,[\text{CommRing }R],\ \forall s\subseteq R,\ (\operatorname{Ideal.span} s = \top) \Rightarrow \\ \forall p:(t:\,s)\to \text{Set}(R_t),\ (\forall t,\ \operatorname{Ideal.span}(p(t)) = \top) \Rightarrow \\ \operatorname{Ideal.span}(\operatorname{Set.range}(\mathrm{IsLocalization.Away.mulNumerator}\,s\,p)) = \top$$$
Lean4
/-- Given a set `s` in a ring `R` and for every `t : s` a set `p t` of fractions in
a localization of `R` at `t`, this is the function sending a pair `(t, y)`, with
`t : s` and `y : t a`, to `t` multiplied with a numerator of `y`. The range
of this function spans the unit ideal, if `s` and every `p t` do. -/
noncomputable def mulNumerator (s : Set R) {Rₜ : s → Type*} [∀ t, CommRing (Rₜ t)] [∀ t, Algebra R (Rₜ t)]
[∀ t, IsLocalization.Away t.val (Rₜ t)] (p : (t : s) → Set (Rₜ t)) (x : (t : s) × p t) : R :=
x.1 * (IsLocalization.Away.sec x.1.1 x.2.1).1
