span_range_mulNumerator_eq_top — Mathlib

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

Похожие утверждения