The height one spectrum of a polynomial ring over a field

A polynomial ring k[X] over a field is a principal ideal domain, so each of its height-one primes is generated by a single polynomial; normalizing that generator to be monic pins it down uniquely: every height-one prime of k[X] has a unique monic irreducible generator. This is what attaches a monic irreducible polynomial to each finite place of the rational function field (Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.2.1(a)).

Main definitions

• IsDedekindDomain.HeightOneSpectrum.ofIrreducible: the height-one prime generated by an irreducible polynomial.
• IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv: the resulting bijection between the monic irreducible polynomials and the height-one primes of k[X].

Main results

• IsDedekindDomain.HeightOneSpectrum.existsUnique_monic_irreducible_span: a height-one prime of k[X] is generated by a unique monic irreducible polynomial.

References

• Mathlib/RingTheory/Ideal/MonicSpan.lean by Nailin Guan, whose Polynomial.exists_monic_span supplies the monic generator used here.

theorem IsDedekindDomain.HeightOneSpectrum.existsUnique_monic_irreducible_span {k : Type u_1} [Field k] (p : HeightOneSpectrum (Polynomial k)) : ∃! q : Polynomial k, q.Monic ∧ Irreducible q ∧ p.asIdeal = Ideal.span {q}

Each height-one prime of k[X] is generated by a unique monic irreducible polynomial.

noncomputable def IsDedekindDomain.HeightOneSpectrum.ofIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : HeightOneSpectrum (Polynomial k)

The height-one prime of k[X] generated by an irreducible polynomial. This generalizes Mathlib's Polynomial.idealX, the prime generated by X.

Equations

• IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq = IsDedekindDomain.HeightOneSpectrum.ofPrime ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ofIrreducible_asIdeal {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) : (ofIrreducible hq).asIdeal = Ideal.span {q}

noncomputable def IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv {k : Type u_1} [Field k] : { q : Polynomial k // q.Monic ∧ Irreducible q } ≃ HeightOneSpectrum (Polynomial k)

The height-one primes of k[X] are the monic irreducible polynomials: the prime generated by a monic irreducible polynomial determines it, by IsDedekindDomain.HeightOneSpectrum.existsUnique_monic_irreducible_span.

Equations

• IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv = Equiv.ofBijective (fun (q : { q : Polynomial k // q.Monic ∧ Irreducible q }) => IsDedekindDomain.HeightOneSpectrum.ofIrreducible ⋯) ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.monicIrreducibleEquiv_apply {k : Type u_1} [Field k] (q : { q : Polynomial k // q.Monic ∧ Irreducible q }) : monicIrreducibleEquiv q = ofIrreducible ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.span_monicIrreducibleEquiv_symm {k : Type u_1} [Field k] (p : HeightOneSpectrum (Polynomial k)) : Ideal.span {↑(monicIrreducibleEquiv.symm p)} = p.asIdeal