Gauss's Lemma for Dedekind Domains #
This file contains Gauss's Lemma for Dedekind Domains, which states that the content ideal of a
polynomial is the whole ring if and only if the v-adic Gauss norms of the polynomial are equal to
1 for all v.
theorem
Polynomial.gaussNorm_intAdicAbv_le_one
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
(v : IsDedekindDomain.HeightOneSpectrum R)
{b : NNReal}
(hb : 1 < b)
(p : Polynomial R)
:
theorem
Polynomial.gaussNorm_lt_one_iff_contentIdeal_le
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
(v : IsDedekindDomain.HeightOneSpectrum R)
{b : NNReal}
(hb : 1 < b)
(p : Polynomial R)
:
Given a polynomial p in R[X], the v-adic Gauss norm of p is smaller than 1 if and only
if the content ideal of p is contained in the prime ideal corresponding to v.
theorem
Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
{b : NNReal}
(hb : 1 < b)
(p : Polynomial R)
(hR : ¬IsField R)
:
p.contentIdeal = ⊤ ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), gaussNorm (v.intAdicAbv hb) 1 p = 1
Gauss's Lemma: given a polynomial p in R[X], the content ideal of p is the whole ring
if and only if the v-adic Gauss norms of p are equal to 1 for all v.
theorem
Polynomial.isPrimitive_iff_forall_gaussNorm_eq_one
{R : Type u_2}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
(hR : ¬IsField R)
{b : NNReal}
(hb : 1 < b)
(p : Polynomial R)
:
In case R is PID, given a polynomial p in R[X], p is primitive if and only if the
v-adic Gauss norms of p are equal to 1 for all v.