The index of an integral primitive element

An integral primitive element θ of a number field K generates a full-rank subring ℤ[θ] of the ring of integers 𝓞 K. Its index is the finite cardinality

[𝓞 K : ℤ[θ]] = #(𝓞 K / ℤ[θ]).

This file defines integral primitive elements and their index, proves that the defining quotient is finite (and hence that the index is positive), and establishes the exact invariances under translating the generator by an integer and negating it.

Main definitions

• TauCeti.NumberField.IntegralPrimitiveElement K: integral elements generating K over ℚ.
• TauCeti.NumberField.IntegralPrimitiveElement.index: the index of ℤ[θ] in 𝓞 K.
• TauCeti.NumberField.IntegralPrimitiveElement.ofAdjoinEqTop: an element generating 𝓞 K as a ℤ-algebra, as an integral primitive element.

Main results

• TauCeti.NumberField.IntegralPrimitiveElement.finrank_adjoin: ℤ[θ] has full rank in 𝓞 K.
• TauCeti.NumberField.IntegralPrimitiveElement.index_pos: the index is positive.
• TauCeti.NumberField.IntegralPrimitiveElement.index_eq_one_iff: the index is 1 exactly when ℤ[θ] is all of 𝓞 K.
• TauCeti.NumberField.adjoin_rat_eq_top_of_adjoin_int_eq_top: an element generating 𝓞 K over ℤ generates K over ℚ.
• TauCeti.NumberField.IntegralPrimitiveElement.index_addIntCast: integer translation preserves the index.
• TauCeti.NumberField.IntegralPrimitiveElement.index_neg: negation preserves the index.
• TauCeti.NumberField.IntegralPrimitiveElement.mem_adjoin_iff: the elements of ℤ[θ] are the polynomial expressions in θ.
• TauCeti.NumberField.IntegralPrimitiveElement.mkQ_eq_zero_iff: an element vanishes in 𝓞 K / ℤ[θ] exactly when it lies in ℤ[θ].

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §2.

def TauCeti.NumberField.IntegralPrimitiveElement (K : Type u_2) [Field K] [NumberField K] : Type u_2

An integral primitive element of a number field K: an element of 𝓞 K whose image in K generates K as a ℚ-algebra.

Equations

• TauCeti.NumberField.IntegralPrimitiveElement K = { θ : NumberField.RingOfIntegers K // ℚ[↑θ] = ⊤ }

theorem TauCeti.NumberField.adjoin_rat_eq_top_of_adjoin_int_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (h : ℤ[θ] = ⊤) : ℚ[↑θ] = ⊤

An element whose order ℤ[θ] is all of 𝓞 K generates K over ℚ.

@[instance_reducible]

instance TauCeti.NumberField.IntegralPrimitiveElement.instCoeRingOfIntegers {K : Type u_1} [Field K] [NumberField K] : Coe (IntegralPrimitiveElement K) (NumberField.RingOfIntegers K)

Equations

• TauCeti.NumberField.IntegralPrimitiveElement.instCoeRingOfIntegers = { coe := Subtype.val }

def TauCeti.NumberField.IntegralPrimitiveElement.adjoin {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : Subalgebra ℤ (NumberField.RingOfIntegers K)

The ℤ-subalgebra of 𝓞 K generated by an integral primitive element.

Equations

• θ.adjoin = ℤ[↑θ]

theorem TauCeti.NumberField.IntegralPrimitiveElement.adjoin_def {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : θ.adjoin = ℤ[↑θ]

The generated order is the ℤ-subalgebra generated by the underlying ring integer.

theorem TauCeti.NumberField.IntegralPrimitiveElement.mem_adjoin_iff {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (x : NumberField.RingOfIntegers K) : x ∈ θ.adjoin ↔ ∃ (G : Polynomial ℤ), (Polynomial.aeval ↑θ) G = x

The elements of ℤ[θ] are the polynomial expressions in θ.

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.aeval_mem_adjoin {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (G : Polynomial ℤ) : (Polynomial.aeval ↑θ) G ∈ θ.adjoin

Every polynomial expression in θ lies in ℤ[θ].

@[reducible, inline]

abbrev TauCeti.NumberField.IntegralPrimitiveElement.Quotient {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : Type u_1

The additive quotient of 𝓞 K by the order ℤ[θ].

Equations

• θ.Quotient = (NumberField.RingOfIntegers K ⧸ Subalgebra.toSubmodule θ.adjoin)

noncomputable def TauCeti.NumberField.IntegralPrimitiveElement.index {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : ℕ

The index [𝓞 K : ℤ[θ]], defined as the cardinality of the additive quotient.

Equations

• θ.index = (Subalgebra.toSubmodule θ.adjoin).cardQuot

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_def {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : θ.index = Nat.card (NumberField.RingOfIntegers K ⧸ Subalgebra.toSubmodule θ.adjoin)

The index is the cardinality of the additive quotient by the generated order.

theorem TauCeti.NumberField.IntegralPrimitiveElement.mkQ_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (b : NumberField.RingOfIntegers K) : (Subalgebra.toSubmodule θ.adjoin).mkQ b = 0 ↔ b ∈ θ.adjoin

An element vanishes in the quotient 𝓞 K / ℤ[θ] exactly when it lies in the order ℤ[θ].

theorem TauCeti.NumberField.IntegralPrimitiveElement.nsmul_mkQ_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (n : ℕ) (b : NumberField.RingOfIntegers K) : n • (Subalgebra.toSubmodule θ.adjoin).mkQ b = 0 ↔ ↑n * b ∈ θ.adjoin

A multiple n • b vanishes in the quotient 𝓞 K / ℤ[θ] exactly when n * b lies in the order ℤ[θ].

theorem TauCeti.NumberField.IntegralPrimitiveElement.finrank_adjoin {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : Module.finrank ℤ ↥θ.adjoin = Module.finrank ℤ (NumberField.RingOfIntegers K)

The order ℤ[θ] generated by an integral primitive element has full rank in 𝓞 K.

instance TauCeti.NumberField.IntegralPrimitiveElement.finite_quotient {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : Finite θ.Quotient

The quotient 𝓞 K / ℤ[θ] is finite.

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_pos {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : 0 < θ.index

The index of an integral primitive element is positive.

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : θ.index = 1 ↔ θ.adjoin = ⊤

The index of an integral primitive element θ is 1 exactly when the order ℤ[θ] is all of 𝓞 K.

def TauCeti.NumberField.IntegralPrimitiveElement.ofAdjoinEqTop {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (h : ℤ[θ] = ⊤) : IntegralPrimitiveElement K

An element generating 𝓞 K as a ℤ-algebra, as an integral primitive element.

Equations

• TauCeti.NumberField.IntegralPrimitiveElement.ofAdjoinEqTop h = ⟨θ, ⋯⟩

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.coe_ofAdjoinEqTop {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (h : ℤ[θ] = ⊤) : ↑(ofAdjoinEqTop h) = θ

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.adjoin_ofAdjoinEqTop {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (h : ℤ[θ] = ⊤) : (ofAdjoinEqTop h).adjoin = ⊤

The order generated by ofAdjoinEqTop h is all of 𝓞 K, by construction.

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_ofAdjoinEqTop {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (h : ℤ[θ] = ⊤) : (ofAdjoinEqTop h).index = 1

An element generating 𝓞 K as a ℤ-algebra has index 1.

Changing the generator

def TauCeti.NumberField.IntegralPrimitiveElement.addIntCast {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (n : ℤ) : IntegralPrimitiveElement K

Translating an integral primitive element by an integer gives another integral primitive element.

Equations

• θ.addIntCast n = ⟨↑θ + (algebraMap ℤ (NumberField.RingOfIntegers K)) n, ⋯⟩

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.coe_addIntCast {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (n : ℤ) : ↑(θ.addIntCast n) = ↑θ + (algebraMap ℤ (NumberField.RingOfIntegers K)) n

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.adjoin_addIntCast {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (n : ℤ) : (θ.addIntCast n).adjoin = θ.adjoin

Integer translation does not change the generated ℤ-subalgebra.

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_addIntCast {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) (n : ℤ) : (θ.addIntCast n).index = θ.index

Translating an integral primitive element by an integer preserves its index.

def TauCeti.NumberField.IntegralPrimitiveElement.neg {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : IntegralPrimitiveElement K

Negating an integral primitive element gives another integral primitive element.

Equations

• θ.neg = ⟨-↑θ, ⋯⟩

@[instance_reducible]

instance TauCeti.NumberField.IntegralPrimitiveElement.instNeg {K : Type u_1} [Field K] [NumberField K] : Neg (IntegralPrimitiveElement K)

Equations

• TauCeti.NumberField.IntegralPrimitiveElement.instNeg = { neg := TauCeti.NumberField.IntegralPrimitiveElement.neg }

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.coe_neg {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : ↑(-θ) = -↑θ

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.adjoin_neg {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : (-θ).adjoin = θ.adjoin

Negation does not change the generated ℤ-subalgebra.

@[simp]

theorem TauCeti.NumberField.IntegralPrimitiveElement.index_neg {K : Type u_1} [Field K] [NumberField K] (θ : IntegralPrimitiveElement K) : (-θ).index = θ.index

Negating an integral primitive element preserves its index.