HomogeneousLocalization — Mathlib

English

The canonical constructor mk sends a homogeneous fraction to its localization class.

Русский

Канонический конструктор mk переводит однородную дробь в её локализационный класс.

LaTeX

$$$\\mathrm{mk}: \\mathrm{NumDenSameDeg}_{\\mathcal{A}}{x} \\to \\mathrm{HomogeneousLocalization}_{\\mathcal{A}}{x}$$$

Lean4

/-- For `x : prime ideal of A`, `HomogeneousLocalization 𝒜 x` is `NumDenSameDeg 𝒜 x` modulo the
kernel of `embedding 𝒜 x`. This is essentially the subring of `Aₓ` where the numerator and
denominator share the same grading.
-/
def HomogeneousLocalization : Type _ :=
  Quotient (Setoid.ker <| HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x)

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