of_le — Mathlib

English

If M ≤ N and every r in N maps to a unit in S under the algebra map, then N localizes to S.

Русский

Если M ≤ N и каждый элемент из N отображается под отображением алгебра в единицу в S, то N локализуется в S.

LaTeX

$$$\\text{IsLocalization } N S$ под условием: M \\le N и \\forall r\\in N, IsUnit(\\mathrm{algebraMap}\\, R S\\, r)$$$

Lean4

theorem of_le (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ r ∈ N, IsUnit (algebraMap R S r)) : IsLocalization N S
    where
  map_units r := h₂ r r.2
  surj
    s :=
    have ⟨⟨x, y, hy⟩, H⟩ := IsLocalization.surj M s
    ⟨⟨x, y, h₁ hy⟩, H⟩
  exists_of_eq
    {x y} := by
    rw [IsLocalization.eq_iff_exists M]
    rintro ⟨c, hc⟩
    exact ⟨⟨c, h₁ c.2⟩, hc⟩

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