English
Let R be a commutative ring, s ⊆ R with span s = ⊤, and for each t ∈ s a set p(t) with span(p(t)) = ⊤. Then the ideal generated by the range of mulNumerator(s, p) is the whole ring.
Русский
Пусть R — коммутативное кольцо, s ⊆ R и span(s) = ⊤, для каждого t ∈ s имеется p(t) с span(p(t)) = ⊤. Тогда порождающий диапазон mulNumerator(s, p) — это весь кольцо.
LaTeX
$$$\operatorname{Ideal.span}(\operatorname{Set.range}(\mathrm{IsLocalization.Away.mulNumerator}\,s\,p)) = \top$, при $\operatorname{Ideal.span}s = \top$ и $\forall t\in s,\ \operatorname{Ideal.span}(p(t)) = \top$.$$
Lean4
theorem span_range_mulNumerator_eq_top {s : Set R} (hsone : Ideal.span s = ⊤) {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)}
(htone : ∀ (r : s), Ideal.span (p r) = ⊤) : Ideal.span (Set.range (IsLocalization.Away.mulNumerator s p)) = ⊤ :=
by
rw [← Ideal.radical_eq_top, eq_top_iff, ← hsone, Ideal.span_le]
intro a ha
haveI : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩) :=
inferInstanceAs <| IsLocalization.Away (⟨a, ha⟩ : s).val (Rₜ ⟨a, ha⟩)
have h₁ :
Ideal.span (p ⟨a, ha⟩) ≤
Ideal.span (algebraMap R (Rₜ ⟨a, ha⟩) '' Set.range (IsLocalization.Away.mulNumerator s p)) :=
by
rw [Ideal.span_le]
intro x hx
rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]
refine ⟨a * (IsLocalization.Away.sec a x).1, Ideal.subset_span ⟨⟨⟨a, ha⟩, ⟨x, hx⟩⟩, rfl⟩, ?_⟩
use ⟨a ^ ((IsLocalization.Away.sec a x).2 + 1), _, rfl⟩
rw [IsLocalization.eq_mk'_iff_mul_eq, map_pow, map_mul, ← map_pow, pow_add, map_mul, ← mul_assoc,
IsLocalization.Away.sec_spec a x, mul_comm, pow_one]
have h₂ :
IsLocalization.mk' (Rₜ ⟨a, ha⟩) 1 (1 : Submonoid.powers a) ∈
Ideal.span (algebraMap R (Rₜ ⟨a, ha⟩) '' (Set.range <| IsLocalization.Away.mulNumerator s p)) :=
by
rw [IsLocalization.mk'_one]
apply h₁
simp [htone]
rw [IsLocalization.mem_span_map (Submonoid.powers a)] at h₂
obtain ⟨y, hy, ⟨-, m, rfl⟩, hyz⟩ := h₂
rw [IsLocalization.eq] at hyz
obtain ⟨⟨-, n, rfl⟩, hc⟩ := hyz
simp only [OneMemClass.coe_one, one_mul, mul_one] at hc
use n + m
simpa [pow_add, hc] using Ideal.mul_mem_left _ _ hy