p-adic integers

This file defines the p-adic integers ℤ_[p] as the subtype of ℚ_[p] with norm ≤ 1. We show that ℤ_[p]

• is complete,
• is nonarchimedean,
• is a normed ring,
• is a local ring, and
• is a discrete valuation ring.

The relation between ℤ_[p] and ZMod p is established in another file.

Important definitions

• PadicInt : the type of p-adic integers

Notation

We introduce the notation ℤ_[p] for the p-adic integers.

Implementation notes

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [Fact p.Prime] as a type class argument.

Coercions into ℤ_[p] are set up to work with the norm_cast tactic.

References

• [F. Q. Gouvêa, p-adic numbers][gouvea1997]
• [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
• https://en.wikipedia.org/wiki/P-adic_number

Tags

p-adic, p adic, padic, p-adic integer

def PadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : Type

The p-adic integers ℤ_[p] are the p-adic numbers with norm ≤ 1.

def «termℤ_[_]» : Lean.ParserDescr

The ring of p-adic integers.

Ring structure and coercion to ℚ_[p]

@[implicit_reducible]

instance PadicInt.instCoePadic {p : ℕ} [hp : Fact (Nat.Prime p)] : Coe ℤ_[p] ℚ_[p]

theorem PadicInt.ext {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]} : ↑x = ↑y → x = y

def PadicInt.subring (p : ℕ) [hp : Fact (Nat.Prime p)] : Subring ℚ_[p]

The p-adic integers as a subring of ℚ_[p].

@[simp]

theorem PadicInt.mem_subring_iff (p : ℕ) [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} : x ∈ subring p ↔ ‖x‖ ≤ 1

@[implicit_reducible]

noncomputable instance PadicInt.instCommRing {p : ℕ} [hp : Fact (Nat.Prime p)] : CommRing ℤ_[p]

@[implicit_reducible]

noncomputable instance PadicInt.instInhabited {p : ℕ} [hp : Fact (Nat.Prime p)] : Inhabited ℤ_[p]

@[simp]

theorem PadicInt.mk_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ‖0‖ ≤ 1} : ⟨0, h⟩ = 0

@[simp]

theorem PadicInt.coe_add {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]) : ↑(z1 + z2) = ↑z1 + ↑z2

@[simp]

theorem PadicInt.coe_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]) : ↑(z1 * z2) = ↑z1 * ↑z2

@[simp]

theorem PadicInt.coe_neg {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 : ℤ_[p]) : ↑(-z1) = -↑z1

@[simp]

theorem PadicInt.coe_sub {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ_[p]) : ↑(z1 - z2) = ↑z1 - ↑z2

@[simp]

theorem PadicInt.coe_one {p : ℕ} [hp : Fact (Nat.Prime p)] : ↑1 = 1

@[simp]

theorem PadicInt.coe_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : ↑0 = 0

@[simp]

theorem PadicInt.coe_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} : ↑x = 0 ↔ x = 0

theorem PadicInt.coe_ne_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} : ↑x ≠ 0 ↔ x ≠ 0

@[simp]

theorem PadicInt.coe_natCast {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem PadicInt.coe_intCast {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ) : ↑↑z = ↑z

noncomputable def PadicInt.Coe.ringHom {p : ℕ} [hp : Fact (Nat.Prime p)] : ℤ_[p] →+* ℚ_[p]

The coercion from ℤ_[p] to ℚ_[p] as a ring homomorphism.

@[simp]

theorem PadicInt.Coe.ringHom_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (self : ↥(subring p)) : ringHom self = ↑self

@[simp]

theorem PadicInt.coe_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem PadicInt.mk_coe {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ_[p]) : ⟨↑k, ⋯⟩ = k

@[simp]

theorem PadicInt.coe_sum {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} (s : Finset α) (f : α → ℤ_[p]) : ↑(∑ z ∈ s, f z) = ∑ z ∈ s, ↑(f z)

theorem PadicInt.isOpenEmbedding_coe {p : ℕ} [hp : Fact (Nat.Prime p)] : Topology.IsOpenEmbedding Subtype.val

noncomputable def PadicInt.inv {p : ℕ} [hp : Fact (Nat.Prime p)] : ℤ_[p] → ℤ_[p]

The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the inverse is defined to be 0.

instance PadicInt.instCharZero {p : ℕ} [hp : Fact (Nat.Prime p)] : CharZero ℤ_[p]

theorem PadicInt.intCast_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (z1 z2 : ℤ) : ↑z1 = ↑z2 ↔ z1 = z2

def PadicInt.ofIntSeq {p : ℕ} [hp : Fact (Nat.Prime p)] (seq : ℕ → ℤ) (h : IsCauSeq (padicNorm p) fun (n : ℕ) => ↑(seq n)) : ℤ_[p]

A sequence of integers that is Cauchy with respect to the p-adic norm converges to a p-adic integer.

Instances

We now show that ℤ_[p] is a

• complete metric space
• normed ring
• integral domain

@[implicit_reducible]

noncomputable instance PadicInt.instMetricSpace (p : ℕ) [hp : Fact (Nat.Prime p)] : MetricSpace ℤ_[p]

instance PadicInt.instIsUltrametricDist (p : ℕ) [hp : Fact (Nat.Prime p)] : IsUltrametricDist ℤ_[p]

instance PadicInt.completeSpace (p : ℕ) [hp : Fact (Nat.Prime p)] : CompleteSpace ℤ_[p]

@[implicit_reducible]

noncomputable instance PadicInt.instNorm (p : ℕ) [hp : Fact (Nat.Prime p)] : Norm ℤ_[p]

theorem PadicInt.norm_def {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : ‖z‖ = ‖↑z‖

@[implicit_reducible]

noncomputable instance PadicInt.instNormedCommRing (p : ℕ) [hp : Fact (Nat.Prime p)] : NormedCommRing ℤ_[p]

instance PadicInt.instNormOneClass (p : ℕ) [hp : Fact (Nat.Prime p)] : NormOneClass ℤ_[p]

instance PadicInt.instNormMulClass (p : ℕ) [hp : Fact (Nat.Prime p)] : NormMulClass ℤ_[p]

instance PadicInt.instIsDomain (p : ℕ) [hp : Fact (Nat.Prime p)] : IsDomain ℤ_[p]

Norm

theorem PadicInt.norm_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ_[p]) : ‖z‖ ≤ 1

theorem PadicInt.nonarchimedean {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℤ_[p]) : ‖q + r‖ ≤ max ‖q‖ ‖r‖

theorem PadicInt.norm_add_eq_max_of_ne {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℤ_[p]} : ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖

theorem PadicInt.norm_eq_of_norm_add_lt_right {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖

theorem PadicInt.norm_eq_of_norm_add_lt_left {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖

@[simp]

theorem PadicInt.padic_norm_e_of_padicInt {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ_[p]) : ‖↑z‖ = ‖z‖

theorem PadicInt.norm_intCast_eq_padic_norm {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ) : ‖↑z‖ = ‖↑z‖

@[simp]

theorem PadicInt.norm_eq_padic_norm {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ_[p]} (hq : ‖q‖ ≤ 1) : ‖⟨q, hq⟩‖ = ‖q‖

@[simp]

theorem PadicInt.norm_p {p : ℕ} [hp : Fact (Nat.Prime p)] : ‖↑p‖ = (↑p)⁻¹

theorem PadicInt.norm_p_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : ‖↑p ^ n‖ = ↑p ^ (-↑n)

@[simp]

theorem PadicInt.one_le_norm_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} : 1 ≤ ‖x‖ ↔ ‖x‖ = 1

@[simp]

theorem PadicInt.norm_natCast_p_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] : ‖↑(p - 1)‖ = 1

instance PadicInt.complete (p : ℕ) [hp : Fact (Nat.Prime p)] : CauSeq.IsComplete ℤ_[p] norm

theorem PadicInt.exists_pow_neg_lt (p : ℕ) [hp : Fact (Nat.Prime p)] {ε : ℝ} (hε : 0 < ε) : ∃ (k : ℕ), ↑p ^ (-↑k) < ε

theorem PadicInt.exists_pow_neg_lt_rat (p : ℕ) [hp : Fact (Nat.Prime p)] {ε : ℚ} (hε : 0 < ε) : ∃ (k : ℕ), ↑p ^ (-↑k) < ε

theorem PadicInt.norm_int_lt_one_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) : ‖↑k‖ < 1 ↔ ↑p ∣ k

theorem PadicInt.norm_int_le_pow_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℤ} {n : ℕ} : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

@[simp]

theorem PadicInt.norm_natCast_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : ‖↑n‖ = 1 ↔ p.Coprime n

@[simp]

theorem PadicInt.norm_natCast_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : ‖↑n‖ < 1 ↔ p ∣ n

@[simp]

theorem PadicInt.norm_intCast_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} : ‖↑z‖ = 1 ↔ IsCoprime z ↑p

@[simp]

theorem PadicInt.norm_intCast_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} : ‖↑z‖ < 1 ↔ ↑p ∣ z

Valuation on ℤ_[p]

theorem PadicInt.valuation_coe_nonneg {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} : 0 ≤ (↑x).valuation

noncomputable def PadicInt.valuation {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ℕ

PadicInt.valuation lifts the p-adic valuation on ℚ to ℤ_[p].

@[simp]

theorem PadicInt.valuation_coe {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : (↑x).valuation = ↑x.valuation

@[simp]

theorem PadicInt.valuation_zero {p : ℕ} [hp : Fact (Nat.Prime p)] : valuation 0 = 0

@[simp]

theorem PadicInt.valuation_one {p : ℕ} [hp : Fact (Nat.Prime p)] : valuation 1 = 0

@[simp]

theorem PadicInt.valuation_p {p : ℕ} [hp : Fact (Nat.Prime p)] : (↑p).valuation = 1

theorem PadicInt.le_valuation_add {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]} (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation

@[simp]

theorem PadicInt.valuation_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℤ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).valuation = x.valuation + y.valuation

@[simp]

theorem PadicInt.valuation_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : (x ^ n).valuation = n * x.valuation

theorem PadicInt.norm_eq_zpow_neg_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = ↑p ^ (-↑x.valuation)

@[simp]

theorem PadicInt.valuation_p_pow_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) : (↑p ^ n * c).valuation = n + c.valuation

Units of ℤ_[p]

theorem PadicInt.mul_inv {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : ‖z‖ = 1 → z * z.inv = 1

theorem PadicInt.inv_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} (hz : ‖z‖ = 1) : z.inv * z = 1

theorem PadicInt.isUnit_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : IsUnit z ↔ ‖z‖ = 1

theorem PadicInt.norm_lt_one_add {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]} (hz1 : ‖z1‖ < 1) (hz2 : ‖z2‖ < 1) : ‖z1 + z2‖ < 1

theorem PadicInt.norm_lt_one_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℤ_[p]} (hz2 : ‖z2‖ < 1) : ‖z1 * z2‖ < 1

theorem PadicInt.mem_nonunits {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1

theorem PadicInt.not_isUnit_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} : ¬IsUnit z ↔ ‖z‖ < 1

noncomputable def PadicInt.mkUnits {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1) : ℤ_[p]ˣ

A p-adic number u with ‖u‖ = 1 is a unit of ℤ_[p].

@[simp]

theorem PadicInt.val_mkUnits {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1) : ↑(mkUnits h) = ⟨u, ⋯⟩

theorem PadicInt.mkUnits_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1) : ↑↑(mkUnits h) = u

@[simp]

theorem PadicInt.norm_units {p : ℕ} [hp : Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) : ‖↑u‖ = 1

noncomputable def PadicInt.unitCoeff {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : ℤ_[p]ˣ

unitCoeff hx is the unit u in the unique representation x = u * p ^ n. See unitCoeff_spec.

@[simp]

theorem PadicInt.unitCoeff_coe {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : ↑↑(unitCoeff hx) = ↑x * ↑p ^ (-↑x.valuation)

theorem PadicInt.unitCoeff_spec {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : x = ↑(unitCoeff hx) * ↑p ^ x.valuation

theorem PadicInt.isUnit_den {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1) : IsUnit ↑r.den

Various characterizations of open unit balls

theorem PadicInt.norm_le_pow_iff_le_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation

theorem PadicInt.mem_span_pow_iff_le_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : x ∈ Ideal.span {↑p ^ n} ↔ n ≤ x.valuation

theorem PadicInt.norm_le_pow_iff_mem_span_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

theorem PadicInt.norm_le_pow_iff_norm_lt_pow_add_one {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ) : ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

theorem PadicInt.norm_lt_pow_iff_norm_le_pow_sub_one {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℤ) : ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

theorem PadicInt.norm_lt_one_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ‖x‖ < 1 ↔ ↑p ∣ x

@[simp]

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

Discrete valuation ring

instance PadicInt.instIsLocalRing {p : ℕ} [hp : Fact (Nat.Prime p)] : IsLocalRing ℤ_[p]

theorem PadicInt.p_nonunit {p : ℕ} [hp : Fact (Nat.Prime p)] : ↑p ∈ nonunits ℤ_[p]

theorem PadicInt.maximalIdeal_eq_span_p {p : ℕ} [hp : Fact (Nat.Prime p)] : IsLocalRing.maximalIdeal ℤ_[p] = Ideal.span {↑p}

theorem PadicInt.prime_p {p : ℕ} [hp : Fact (Nat.Prime p)] : Prime ↑p

theorem PadicInt.irreducible_p {p : ℕ} [hp : Fact (Nat.Prime p)] : Irreducible ↑p

instance PadicInt.instIsDiscreteValuationRing {p : ℕ} [hp : Fact (Nat.Prime p)] : IsDiscreteValuationRing ℤ_[p]

theorem PadicInt.ideal_eq_span_pow_p {p : ℕ} [hp : Fact (Nat.Prime p)] {s : Ideal ℤ_[p]} (hs : s ≠ ⊥) : ∃ (n : ℕ), s = Ideal.span {↑p ^ n}

instance PadicInt.instIsAdicCompleteMaximalIdeal {p : ℕ} [hp : Fact (Nat.Prime p)] : IsAdicComplete (IsLocalRing.maximalIdeal ℤ_[p]) ℤ_[p]

@[implicit_reducible]

noncomputable instance PadicInt.algebra {p : ℕ} [hp : Fact (Nat.Prime p)] : Algebra ℤ_[p] ℚ_[p]

@[simp]

theorem PadicInt.algebraMap_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : (algebraMap ℤ_[p] ℚ_[p]) x = ↑x

instance PadicInt.isFractionRing {p : ℕ} [hp : Fact (Nat.Prime p)] : IsFractionRing ℤ_[p] ℚ_[p]