Denominators of elements of an algebra

For an element x of an R-algebra S, with R a principal ideal ring, the denominator Algebra.denominator R x is a generator of the colon ideal (integralClosure R S).colon {x}, that is, of the ideal of scalars r : R clearing the denominators of x, in the sense that r • x is integral over R. When R = ℤ, its absolute value is the natural-number denominator Algebra.natDenominator x.

The definition needs no hypothesis on x, but it is only meaningful for x algebraic over R: IsAlgebraic.denominator_ne_zero shows the denominator is then nonzero, whereas no nonzero multiple of a transcendental element is integral, so that the colon ideal is trivial and the denominator is 0. See the example below, taking x to be the variable in ℤ[X].

Main definitions

• Algebra.denominator: the denominator of an element, over a principal ideal ring
• Algebra.natDenominator: the natural-number denominator of an element, over ℤ

Main results

• Algebra.denominator_dvd_iff: denominator R x divides exactly the r : R with r • x integral over R
• IsAlgebraic.denominator_ne_zero: the denominator of an algebraic element is nonzero

noncomputable def Algebra.denominator (R : Type u_1) {S : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] (x : S) : R

The denominator of an element x of an R-algebra: a generator of the ideal of scalars r : R such that r • x is integral over R. It is nonzero as soon as x is algebraic over R; see IsAlgebraic.denominator_ne_zero.

Equations

• Algebra.denominator R x = Submodule.IsPrincipal.generator ((Subalgebra.toSubmodule (integralClosure R S)).colon {x})

theorem Algebra.denominator_def (R : Type u_1) {S : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] (x : S) : denominator R x = Submodule.IsPrincipal.generator ((Subalgebra.toSubmodule (integralClosure R S)).colon {x})

theorem Algebra.denominator_dvd_iff {R : Type u_1} {S : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] {r : R} {x : S} : denominator R x ∣ r ↔ IsIntegral R (r • x)

theorem Algebra.isIntegral_denominator_smul {R : Type u_1} {S : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] (x : S) : IsIntegral R (denominator R x • x)

noncomputable def Algebra.natDenominator {S : Type u_2} [CommRing S] (x : S) : ℕ

The natural-number denominator of an element x of a ring: it is the absolute value of the denominator of x over ℤ.

Equations

• Algebra.natDenominator x = (Algebra.denominator ℤ x).natAbs

theorem Algebra.natDenominator_def {S : Type u_2} [CommRing S] (x : S) : natDenominator x = (denominator ℤ x).natAbs

theorem Algebra.natDenominator_dvd_iff {S : Type u_2} [CommRing S] {n : ℕ} {x : S} : natDenominator x ∣ n ↔ IsIntegral ℤ (n • x)

theorem Algebra.isIntegral_natDenominator_smul {S : Type u_2} [CommRing S] (x : S) : IsIntegral ℤ (natDenominator x • x)

theorem IsAlgebraic.denominator_ne_zero (R : Type u_1) {S : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsAlgebraic R x) : Algebra.denominator R x ≠ 0

theorem IsAlgebraic.natDenominator_ne_zero {S : Type u_2} [CommRing S] {x : S} (hx : IsAlgebraic ℤ x) : Algebra.natDenominator x ≠ 0