Units of a number field #

We prove results about the group (𝓞 K)ˣ of units of the ring of integers 𝓞 K of a number field K.

Main results #

isUnit_iff_norm: an algebraic integer x : 𝓞 K is a unit if and only if |norm ℚ x| = 1.
mem_torsion: a unit x : (𝓞 K)ˣ is torsion iff w x = 1 for all infinite places of K.

Tags #

number field, units

source

theorem Rat.RingOfIntegers.isUnit_iff {x : { x // x ∈ NumberField.ringOfIntegers ℚ }} :

IsUnit x ↔ ↑x = 1 ∨ ↑x = -1

source

theorem isUnit_iff_norm {K : Type u_1} [Field K] [NumberField K] {x : { x // x ∈ NumberField.ringOfIntegers K }} :

IsUnit x ↔ |↑(↑(RingOfIntegers.norm ℚ) x)| = 1

source

theorem NumberField.Units.coe_injective (K : Type u_1) [Field K] :

Function.Injective fun x => ↑↑x

source

theorem NumberField.Units.coe_mul {K : Type u_1} [Field K] (x : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (y : { x // x ∈ NumberField.ringOfIntegers K }ˣ) :

↑↑(x * y) = ↑↑x * ↑↑y

source

theorem NumberField.Units.coe_pow {K : Type u_1} [Field K] (x : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (n : ℕ) :

↑↑(x ^ n) = ↑↑x ^ n

source

theorem NumberField.Units.coe_zpow {K : Type u_1} [Field K] (x : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (n : ℤ) :

↑↑(x ^ n) = ↑↑x ^ n

source

theorem NumberField.Units.coe_one {K : Type u_1} [Field K] :

↑↑1 = 1

source

theorem NumberField.Units.coe_neg_one {K : Type u_1} [Field K] :

↑↑(-1) = -1

source

theorem NumberField.Units.coe_ne_zero {K : Type u_1} [Field K] (x : { x // x ∈ NumberField.ringOfIntegers K }ˣ) :

↑↑x ≠ 0

source

def NumberField.Units.torsion (K : Type u_1) [Field K] :

Subgroup { x // x ∈ NumberField.ringOfIntegers K }ˣ

The torsion subgroup of the group of units.

Instances For

source

theorem NumberField.Units.mem_torsion (K : Type u_1) [Field K] {x : { x // x ∈ NumberField.ringOfIntegers K }ˣ} [NumberField K] :

x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), ↑w ↑↑x = 1

source

instance NumberField.Units.instNonemptySubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupUnitsInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] :

Nonempty { x // x ∈ NumberField.Units.torsion K }

Shortcut instance because Lean tends to time out before finding the general instance.

source

instance NumberField.Units.instFintypeSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupUnitsInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] :

Fintype { x // x ∈ NumberField.Units.torsion K }

The torsion subgroup is finite.

source

instance NumberField.Units.instFiniteSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupUnitsInstSetLikeSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] :

Finite { x // x ∈ NumberField.Units.torsion K }

source

instance NumberField.Units.instIsCyclicSubtypeUnitsMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringSubgroupInstGroupUnitsInstSetLikeSubgroupTorsionToGroup (K : Type u_1) [Field K] [NumberField K] :

IsCyclic { x // x ∈ NumberField.Units.torsion K }

The torsion subgroup is cylic.

source

def NumberField.Units.torsionOrder (K : Type u_1) [Field K] [NumberField K] :

ℕ+

The order of the torsion subgroup as positive integer.

Instances For

source

theorem NumberField.Units.rootsOfUnity_eq_one (K : Type u_1) [Field K] {ζ : { x // x ∈ NumberField.ringOfIntegers K }ˣ} [NumberField K] {k : ℕ+} (hc : Nat.Coprime ↑k ↑(NumberField.Units.torsionOrder K)) :

ζ ∈ rootsOfUnity k { x // x ∈ NumberField.ringOfIntegers K } ↔ ζ = 1

If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.

source

theorem NumberField.Units.rootsOfUnity_eq_torsion (K : Type u_1) [Field K] [NumberField K] :

rootsOfUnity (NumberField.Units.torsionOrder K) { x // x ∈ NumberField.ringOfIntegers K } = NumberField.Units.torsion K

The group of roots of unity of order dividing torsionOrder is equal to the torsion group.