Units of a number field

Basic facts about the units of the ring of integers of a number field K, beyond Mathlib's Mathlib.NumberTheory.NumberField.Units.Basic.

The norm of a unit is ±1, so the constant coefficient of its minimal polynomial over ℤ is ±1. The units of ℤ are ±1, so a unit of 𝓞 K whose image in K is rational is a root of unity: its absolute value is the same at every infinite place, and the product formula forces that value to be 1. Read the other way, a non-torsion unit lies outside the base field ℚ, which is what field-generation and primitive-element arguments about units need, for instance to see that a non-torsion unit of a field of prime degree generates the field.

Main results

• TauCeti.NumberField.Units.coeff_zero_minpoly_eq_one_or_neg_one: the constant coefficient of the minimal polynomial of a unit is ±1.
• TauCeti.NumberField.Units.mem_torsion_of_mem_bot: a unit whose image in K lies in the base field ℚ is torsion.
• Units.prod_norm_embedding_eq_one: the absolute values of the conjugates of a unit have product |N(u)| = 1.
• NumberField.InfinitePlace.exists_torsion_mul_embedding_eq_abs: a torsion sign makes a unit's real embedding equal its absolute value at a real place.

theorem NumberField.InfinitePlace.exists_torsion_mul_embedding_eq_abs {K : Type u_1} [Field K] (w : InfinitePlace K) (hw : w.IsReal) (v : (RingOfIntegers K)ˣ) : ∃ (ε : ↥(Units.torsion K)), (embedding_of_isReal hw) ((algebraMap (RingOfIntegers K) K) ↑(↑ε * v)) = w ((algebraMap (RingOfIntegers K) K) ↑v)

At a real place, multiply a unit by a torsion unit so that its real embedding is its (positive) absolute value.

@[simp]

theorem Units.prod_norm_embedding_eq_one {K : Type u_1} [Field K] [NumberField K] (u : (NumberField.RingOfIntegers K)ˣ) : ∏ σ : K →+* ℂ, ‖σ ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)‖ = 1

The absolute values of the conjugates of a unit u have product |N(u)| = 1.

instance TauCeti.NumberField.Units.instTendstoCofiniteUnitsRingOfIntegersCoeRingHomAlgebraMapVal_tauCeti {K : Type u_1} [Field K] : Filter.TendstoCofinite fun (u : (NumberField.RingOfIntegers K)ˣ) => (algebraMap (NumberField.RingOfIntegers K) K) ↑u

The coercion from units of the ring of integers to the number field has finite fibers.

theorem TauCeti.NumberField.Units.coeff_zero_minpoly_eq_one_or_neg_one {K : Type u_1} [Field K] [NumberField K] (v : (NumberField.RingOfIntegers K)ˣ) : (minpoly ℤ ↑v).coeff 0 = 1 ∨ (minpoly ℤ ↑v).coeff 0 = -1

The constant coefficient of the minimal polynomial of a unit is ±1.

theorem TauCeti.NumberField.Units.mem_torsion_of_mem_bot {K : Type u_1} [Field K] [NumberField K] {v : (NumberField.RingOfIntegers K)ˣ} (hv : (algebraMap (NumberField.RingOfIntegers K) K) ↑v ∈ ⊥) : v ∈ NumberField.Units.torsion K

A unit whose image in K lies in the base field ℚ is torsion.