algebraMap_injective_of_span_eq_top

English

If s ⊆ R spans the top ideal and the localized product map is injective, then the algebra map R → Localization.Away a.1 is injective componentwise.

Русский

Если множество s породило топовую идею, то отображение алгебраMap инъективно на компоненте Away a.1.

LaTeX

$$$\text{algebraMap is injective under span top}$$$

Lean4

theorem algebraMap_injective_of_span_eq_top (s : Set R) (span_eq : Ideal.span s = ⊤) :
    Function.Injective (algebraMap R <| Π a : s, Away a.1) := fun x y eq ↦
  by
  suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this
  by_contra ne
  have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalization.eq_iff_exists (.powers r.1) _).mp (congr_fun eq r)
  exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

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