Units of a number field

We prove some basic results on the group (𝓞 K)ˣ of units of the ring of integers 𝓞 K of a number field K and its torsion subgroup.

Main definition

• NumberField.Units.torsion: the torsion subgroup of a number field.

Main results

• NumberField.isUnit_iff_norm: an algebraic integer x : 𝓞 K is a unit if and only if |norm ℚ x| = 1.

• NumberField.Units.mem_torsion: a unit x : (𝓞 K)ˣ is torsion iff w x = 1 for all infinite places w of K.

Tags

number field, units

theorem Rat.RingOfIntegers.isUnit_iff {x : NumberField.RingOfIntegers ℚ} : IsUnit x ↔ ↑x = 1 ∨ ↑x = -1

theorem NumberField.isUnit_iff_norm {K : Type u_1} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} : IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1

instance NumberField.Units.instCoeHTCUnitsRingOfIntegers (K : Type u_1) [Field K] : CoeHTC (NumberField.RingOfIntegers K)ˣ K

Equations

• NumberField.Units.instCoeHTCUnitsRingOfIntegers K = { coe := fun (x : (NumberField.RingOfIntegers K)ˣ) => (algebraMap (NumberField.RingOfIntegers K) K) ↑x }

theorem NumberField.Units.coe_injective (K : Type u_1) [Field K] : Function.Injective fun (x : (NumberField.RingOfIntegers K)ˣ) => (algebraMap (NumberField.RingOfIntegers K) K) ↑x

theorem NumberField.Units.coe_coe {K : Type u_1} [Field K] (u : (NumberField.RingOfIntegers K)ˣ) : ↑↑u = (algebraMap (NumberField.RingOfIntegers K) K) ↑u

theorem NumberField.Units.coe_mul {K : Type u_1} [Field K] (x : (NumberField.RingOfIntegers K)ˣ) (y : (NumberField.RingOfIntegers K)ˣ) : (algebraMap (NumberField.RingOfIntegers K) K) ↑(x * y) = (algebraMap (NumberField.RingOfIntegers K) K) ↑x * (algebraMap (NumberField.RingOfIntegers K) K) ↑y

theorem NumberField.Units.coe_pow {K : Type u_1} [Field K] (x : (NumberField.RingOfIntegers K)ˣ) (n : ℕ) : (algebraMap (NumberField.RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (NumberField.RingOfIntegers K) K) ↑x ^ n

theorem NumberField.Units.coe_zpow {K : Type u_1} [Field K] (x : (NumberField.RingOfIntegers K)ˣ) (n : ℤ) : (algebraMap (NumberField.RingOfIntegers K) K) ↑(x ^ n) = (algebraMap (NumberField.RingOfIntegers K) K) ↑x ^ n

theorem NumberField.Units.coe_one {K : Type u_1} [Field K] : (algebraMap (NumberField.RingOfIntegers K) K) ↑1 = 1

theorem NumberField.Units.coe_neg_one {K : Type u_1} [Field K] : (algebraMap (NumberField.RingOfIntegers K) K) ↑(-1) = -1

theorem NumberField.Units.coe_ne_zero {K : Type u_1} [Field K] (x : (NumberField.RingOfIntegers K)ˣ) : (algebraMap (NumberField.RingOfIntegers K) K) ↑x ≠ 0

@[simp]

theorem NumberField.Units.norm (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : |(Algebra.norm ℚ) ((algebraMap (NumberField.RingOfIntegers K) K) ↑x)| = 1

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

The torsion subgroup of the group of units.

Equations

• NumberField.Units.torsion K = CommGroup.torsion (NumberField.RingOfIntegers K)ˣ

theorem NumberField.Units.mem_torsion (K : Type u_1) [Field K] {x : (NumberField.RingOfIntegers K)ˣ} [NumberField K] : x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1

instance NumberField.Units.instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] : Fintype ↥(NumberField.Units.torsion K)

The torsion subgroup is finite.

Equations

• NumberField.Units.instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion K = Fintype.ofFinite ↥(NumberField.Units.torsion K)

instance NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion (K : Type u_1) [Field K] : Nonempty ↥(NumberField.Units.torsion K)

Equations

• ⋯ = ⋯

instance NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] : IsCyclic ↥(NumberField.Units.torsion K)

The torsion subgroup is cylic.

Equations

• ⋯ = ⋯

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

The order of the torsion subgroup as a positive integer.

Equations

• NumberField.Units.torsionOrder K = ⟨Fintype.card ↥(NumberField.Units.torsion K), ⋯⟩

theorem NumberField.Units.rootsOfUnity_eq_one (K : Type u_1) [Field K] [NumberField K] {k : ℕ+} (hc : (↑k).Coprime ↑(NumberField.Units.torsionOrder K)) {ζ : (NumberField.RingOfIntegers K)ˣ} : ζ ∈ rootsOfUnity k (NumberField.RingOfIntegers K) ↔ ζ = 1

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

theorem NumberField.Units.rootsOfUnity_eq_torsion (K : Type u_1) [Field K] [NumberField K] : rootsOfUnity (NumberField.Units.torsionOrder K) (NumberField.RingOfIntegers K) = NumberField.Units.torsion K

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