mapToFractionRing — Mathlib

English

There is a canonical map from a localization to the fraction ring when the submonoid is contained in the set of non-zerodivisors.

Русский

Существует каноническое отображение от локализации к полному полю частностей, когда подмножество локализации входит в множество ненулевых делителей.

LaTeX

$$$\\text{mapToFractionRing }(K,S,B,hS) : B \\to_A K$$$

Lean4

/-- The canonical map from a localization of `A` at `S` to the fraction ring
  of `A`, given that `S ≤ A⁰`. -/
noncomputable def mapToFractionRing (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S ≤ A⁰) :
    B →ₐ[A] K :=
  { IsLocalization.lift (map_isUnit_of_le K S hS) with commutes' := fun a => by simp }

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