The denominator ideal of an element of an algebra

For x in an R-algebra K, the denominator ideal Algebra.denIdeal K x is the colon ideal (R : x) = {r : R | r • x ∈ R} — the r that clear the denominator of x. When K is the localization of R at its non-zero-divisors it is nonzero (Algebra.denIdeal_ne_bot), because any expression of x as a fraction exhibits a denominator in it.

This is general commutative algebra, used in TauCeti/RingTheory/DedekindDomain/SInteger/Basic.lean to show that every ideal of a ring of S-integers is extended from the base.

Split out of material adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll); following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

def Algebra.denIdeal {R : Type u_1} [CommSemiring R] (K : Type u_2) [Semiring K] [Algebra R K] (x : K) : Ideal R

The denominator ideal of x : K: the colon ideal (R : x) = {r : R | r • x ∈ R}.

It is an opaque def rather than an abbrev so that simp cannot rewrite through it with Submodule.mem_colon_singleton before mem_denIdeal_iff fires; membership is accessed through that lemma throughout, and the colon-ideal description through denIdeal_def.

Equations

• Algebra.denIdeal K x = Submodule.colon 1 {x}

theorem Algebra.denIdeal_def {R : Type u_1} [CommSemiring R] (K : Type u_2) [Semiring K] [Algebra R K] (x : K) : denIdeal K x = Submodule.colon 1 {x}

The defining equality of Algebra.denIdeal, exported because the definition is opaque: consumers reaching for colon-ideal operations rewrite with this, while mem_denIdeal_iff remains the membership normal form. Not a simp lemma — rewriting with it would undo mem_denIdeal_iff.

@[simp]

theorem Algebra.mem_denIdeal_iff {R : Type u_1} [CommSemiring R] (K : Type u_2) [Semiring K] [Algebra R K] {x : K} {r : R} : r ∈ denIdeal K x ↔ ∃ (s : R), (algebraMap R K) r * x = (algebraMap R K) s

Membership in the denominator ideal: r clears x into the image of R, in the sense that r * x is the image of some s : R.

theorem Algebra.denIdeal_ne_bot {R : Type u_1} [CommSemiring R] (K : Type u_2) [CommSemiring K] [Algebra R K] [Nontrivial R] [IsLocalization (nonZeroDivisors R) K] (x : K) : denIdeal K x ≠ ⊥

The denominator ideal of an element of a localization at the non-zero-divisors is nonzero: a denominator witnessing the element as a fraction lies in it.