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 : RingOfIntegers K} : IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1

instance NumberField.Units.instCoeHTCUnitsRingOfIntegers (K : Type u_1) [Field K] : CoeHTC (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 : (RingOfIntegers K)ˣ) => (algebraMap (RingOfIntegers K) K) ↑x

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

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

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

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

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

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

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

def NumberField.Units.complexEmbedding {K : Type u_1} [Field K] (φ : K →+* ℂ) : (RingOfIntegers K)ˣ →* ℂˣ

The group homomorphism (𝓞 K)ˣ →* ℂˣ induced by a complex embedding of K.

Equations

• NumberField.Units.complexEmbedding φ = (Units.map ↑φ).comp (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K))

@[simp]

theorem NumberField.Units.complexEmbedding_apply {K : Type u_1} [Field K] (φ : K →+* ℂ) (u : (RingOfIntegers K)ˣ) : ↑((Units.complexEmbedding φ) u) = φ ((algebraMap (RingOfIntegers K) K) ↑u)

theorem NumberField.Units.complexEmbedding_injective {K : Type u_1} [Field K] (φ : K →+* ℂ) : Function.Injective ⇑(Units.complexEmbedding φ)

@[simp]

theorem NumberField.Units.complexEmbedding_inj {K : Type u_1} [Field K] (φ : K →+* ℂ) (u v : (RingOfIntegers K)ˣ) : (Units.complexEmbedding φ) u = (Units.complexEmbedding φ) v ↔ u = v

@[simp]

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

theorem NumberField.Units.pos_at_place {K : Type u_1} [Field K] (x : (RingOfIntegers K)ˣ) (w : InfinitePlace K) : 0 < w ((algebraMap (RingOfIntegers K) K) ↑x)

theorem NumberField.Units.sum_mult_mul_log {K : Type u_1} [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) : ∑ w : InfinitePlace K, ↑w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) ↑x)) = 0

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

The torsion subgroup of the group of units.

Equations

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

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

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

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

The torsion subgroup is finite.

Equations

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

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

The torsion subgroup is cyclic.

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

The order of the torsion subgroup.

Equations

• NumberField.Units.torsionOrder K = Fintype.card ↥(NumberField.Units.torsion K)

instance NumberField.Units.instNeZeroNatTorsionOrder (K : Type u_1) [Field K] [NumberField K] : NeZero (torsionOrder K)

theorem NumberField.Units.torsionOrder_ne_zero (K : Type u_1) [Field K] [NumberField K] : torsionOrder K ≠ 0

theorem NumberField.Units.torsionOrder_pos (K : Type u_1) [Field K] [NumberField K] : 0 < torsionOrder K

theorem NumberField.Units.rootsOfUnity_eq_one (K : Type u_1) [Field K] [NumberField K] {k : ℕ+} (hc : (↑k).Coprime (torsionOrder K)) {ζ : (RingOfIntegers K)ˣ} : ζ ∈ rootsOfUnity (↑k) (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 (torsionOrder K) (RingOfIntegers K) = torsion K

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

theorem NumberField.Units.map_complexEmbedding_torsion (K : Type u_1) [Field K] [NumberField K] (φ : K →+* ℂ) : Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ

The image of torsion K by a complex embedding is the group of complex roots of unity of order torsionOrder K.

theorem NumberField.Units.even_torsionOrder (K : Type u_1) [Field K] [NumberField K] : Even (torsionOrder K)

theorem NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank {K : Type u_1} [Field K] [NumberField K] (h : Odd (Module.finrank ℚ K)) (x : ↥(torsion K)) : ↑x = 1 ∨ ↑x = -1

theorem NumberField.Units.torsionOrder_eq_two_of_odd_finrank {K : Type u_1} [Field K] [NumberField K] (h : Odd (Module.finrank ℚ K)) : torsionOrder K = 2