Documentation

TauCeti.NumberTheory.NumberField.Monogenic

Monogenic number fields #

A number field K is monogenic when its ring of integers admits a power integral basis, that is 𝓞 K = ℤ[θ] for a single algebraic integer θ. This file defines the predicate, gives the two standard criteria for it — one in terms of the conductor exponent, one in terms of the index [𝓞 K : ℤ[θ]] — and records the classical monogenic families.

The predicate lives in the TauCeti.NumberField namespace rather than the root namespace, where a bare IsMonogenic would collide with the ring-theoretic notion of a monogenic algebra.

Main definitions #

Main results #

Dedekind's cubic field, the standard example of a field that is not monogenic, is not treated here: its non-monogenicity is witnessed by a common index divisor, a prime dividing the index of every generator.

References #

source
def TauCeti.NumberField.IsMonogenic (K : Type u_2) [Field K] :
Prop

A field K is monogenic when its ring of integers is generated by a single algebraic integer as a ℤ-algebra, that is 𝓞 K = ℤ[θ].

Only [Field K] is assumed, because 𝓞 K needs no more than that; the intended case, and the one every result below is about, is a number field.

Equations
Instances For
    source
    theorem TauCeti.NumberField.isMonogenic_def {K : Type u_1} [Field K] :
    IsMonogenic K ↔ ∃ (θ : NumberField.RingOfIntegers K), ℤ[θ] = ⊤

    The defining condition of monogenicity, for introducing and eliminating the predicate.

    source
    theorem TauCeti.NumberField.isMonogenic_iff_exists_exponent_eq_one {K : Type u_1} [Field K] :
    IsMonogenic K ↔ ∃ (θ : NumberField.RingOfIntegers K), RingOfIntegers.exponent θ = 1

    Monogenicity via the conductor exponent. K is monogenic exactly when some algebraic integer of K has conductor exponent 1.

    source
    theorem TauCeti.NumberField.isMonogenic_iff_exists_index_eq_one {K : Type u_1} [Field K] [NumberField K] :
    IsMonogenic K ↔ ∃ (θ : IntegralPrimitiveElement K), θ.index = 1

    Monogenicity via the index. K is monogenic exactly when some integral primitive element has index 1, so the two ways of saying 𝓞 K = ℤ[θ] agree.

    source
    theorem TauCeti.NumberField.isMonogenic_of_isCyclotomicExtension {K : Type u_1} [Field K] [CharZero K] (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] :
    IsMonogenic K

    Cyclotomic fields are monogenic: a primitive n-th root of unity generates the ring of integers, 𝓞 K = ℤ[ζ]. The root is produced internally, so no generator need be supplied.

    source
    theorem TauCeti.NumberField.isMonogenic_cyclotomicField_four :
    IsMonogenic (CyclotomicField 4 ℚ)

    ℚ(i) is monogenic: the fourth cyclotomic field has 𝓞 ℚ(i) = ℤ[i], generated by a primitive fourth root of unity.

    source
    theorem TauCeti.NumberField.isMonogenic_of_mod_four_ne_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 ≠ 1) :
    IsMonogenic K

    Quadratic fields with d % 4 ≠ 1 are monogenic, generated by θ itself.

    source
    theorem TauCeti.NumberField.isMonogenic_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 = 1) :
    IsMonogenic K

    Quadratic fields with d % 4 = 1 are monogenic, generated by (1 + θ) / 2.

    source
    theorem TauCeti.NumberField.isMonogenic_of_quadratic {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) :
    IsMonogenic K

    Quadratic fields are monogenic. Either θ or (1 + θ) / 2 generates the ring of integers, according to the class of d modulo 4.

    source
    @[simp]
    theorem TauCeti.NumberField.isMonogenic_rat :
    IsMonogenic ℚ

    ℚ is monogenic: its ring of integers is ℤ, generated by 1.