Units of the p-adic integers

Complements to Mathlib's PadicInt API on the units of ℤ_p: 1 + x is a unit whenever p ∣ x, because ℤ_p is a local ring whose maximal ideal is pℤ_p. This is the criterion that makes 1 + p^f ℤ_p a subgroup of ℤ_pˣ.

The unit group ℤ_pˣ is a profinite group: it is the closed unit sphere of the compact totally disconnected space ℤ_p, and the topology of the units is the subspace topology because ℤ_p is a complete normed ring. The instances CompactSpace ℤ_[p]ˣ and TotallyDisconnectedSpace ℤ_[p]ˣ are recorded here.

Two consequences of the ultrametric divisibility in ℤ_p are recorded as well: an element divides every element of no larger norm, so that a finite family of p-adic integers is a common multiple q • w of a family w with a coordinate equal to 1, namely at an index of maximal norm. This is the shape in which the exponent vector of a relator of a free pro-p group is read.

Main results

• PadicInt.isUnit_one_add_of_dvd: 1 + x is a unit of ℤ_[p] whenever p ∣ x.
• PadicInt.isUnit_two: 2 is a unit of ℤ_[p] for odd p.
• PadicInt.pow_p_dvd_natCast_iff: p ^ n divides a natural number in ℤ_[p] exactly when it does in ℕ.
• PadicInt.dvd_of_norm_le: in ℤ_[p], y ∣ x whenever ‖x‖ ≤ ‖y‖.
• PadicInt.exists_apply_eq_one_and_eq_smul: a finite family in ℤ_[p] is q • w with w i₀ = 1 at some index i₀.
• PadicInt.units_neg_one_ne_one: -1 ≠ 1 in ℤ_[p]ˣ.
• PadicInt.range_units_val: the units of ℤ_[p] are the elements of norm 1.
• Padic.exists_eq_zpow_valuation_mul: every nonzero x : ℚ_[p] is p ^ v(x) times a unit of ℤ_[p].
• PadicInt.compactSpace_units, PadicInt.totallyDisconnectedSpace_units: ℤ_[p]ˣ is a profinite group.

theorem PadicInt.isUnit_one_add_of_dvd {p : ℕ} [Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : ↑p ∣ x) : IsUnit (1 + x)

In ℤ_p, 1 + x is a unit whenever p ∣ x.

theorem PadicInt.isUnit_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) : IsUnit 2

2 is a unit in ℤ_p for every odd prime p.

@[simp]

theorem PadicInt.pow_p_dvd_natCast_iff {p : ℕ} [Fact (Nat.Prime p)] (n a : ℕ) : ↑p ^ n ∣ ↑a ↔ p ^ n ∣ a

p ^ n divides a natural number in ℤ_p exactly when it divides it in ℕ: the natural number version of PadicInt.pow_p_dvd_int_iff.

theorem PadicInt.units_neg_one_ne_one {p : ℕ} [Fact (Nat.Prime p)] : -1 ≠ 1

-1 ≠ 1 in ℤ_pˣ: the unit group has an element of order two.

theorem PadicInt.range_units_val {p : ℕ} [Fact (Nat.Prime p)] : Set.range Units.val = {x : ℤ_[p] | ‖x‖ = 1}

The units of ℤ_p are the elements of norm 1.

instance PadicInt.compactSpace_units {p : ℕ} [Fact (Nat.Prime p)] : CompactSpace ℤ_[p]ˣ

ℤ_pˣ is compact: it is the closed unit sphere of the compact space ℤ_p, and the topology on the units of the complete normed ring ℤ_p is the subspace topology.

instance PadicInt.totallyDisconnectedSpace_units {p : ℕ} [Fact (Nat.Prime p)] : TotallyDisconnectedSpace ℤ_[p]ˣ

ℤ_pˣ is totally disconnected, as a subspace of the ultrametric space ℤ_p.

theorem PadicInt.dvd_of_norm_le {p : ℕ} [Fact (Nat.Prime p)] {x y : ℤ_[p]} (h : ‖x‖ ≤ ‖y‖) : y ∣ x

Divisibility from the norm: in ℤ_p, y divides every x with ‖x‖ ≤ ‖y‖, because x then lies in the ideal p^{v_p(y)} ℤ_p = y ℤ_p when y ≠ 0, and vanishes when y = 0.

theorem PadicInt.exists_apply_eq_one_and_eq_smul {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} [Finite ι] [Nonempty ι] (v : ι → ℤ_[p]) : ∃ (i₀ : ι) (q : ℤ_[p]) (w : ι → ℤ_[p]), w i₀ = 1 ∧ v = q • w

A finite family of p-adic integers is a multiple of a family with a coordinate 1: for v : ι → ℤ_p with ι finite and nonempty there are an index i₀, a scalar q and a family w with w i₀ = 1 and v = q • w. One may take i₀ of maximal norm and q = v i₀, which then divides every coordinate.

theorem Padic.exists_eq_zpow_valuation_mul {p : ℕ} [Fact (Nat.Prime p)] {x : ℚ_[p]} (hx : x ≠ 0) : ∃ (u : ℤ_[p]ˣ), x = ↑p ^ x.valuation * ↑↑u

Every nonzero p-adic number is p ^ v(x) times a unit of ℤ_[p].