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]

Tags

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

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

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

Equations

• ℤ_[p] = { x : ℚ_[p] // ‖x‖ ≤ 1 }

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

The ring of p-adic integers.

Equations

• One or more equations did not get rendered due to their size.

Ring structure and coercion to ℚ_[p]

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

Equations

• PadicInt.instCoePadicIntPadic = { coe := Subtype.val }

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

instance PadicInt.instAddPadicInt {p : ℕ} [Fact (Nat.Prime p)] : Add ℤ_[p]

Addition on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instAddPadicInt = inferInstance

instance PadicInt.instMulPadicInt {p : ℕ} [Fact (Nat.Prime p)] : Mul ℤ_[p]

Multiplication on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instMulPadicInt = inferInstance

instance PadicInt.instNegPadicInt {p : ℕ} [Fact (Nat.Prime p)] : Neg ℤ_[p]

Negation on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instNegPadicInt = inferInstance

instance PadicInt.instSubPadicInt {p : ℕ} [Fact (Nat.Prime p)] : Sub ℤ_[p]

Subtraction on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instSubPadicInt = inferInstance

instance PadicInt.instZeroPadicInt {p : ℕ} [Fact (Nat.Prime p)] : Zero ℤ_[p]

Zero on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instZeroPadicInt = inferInstance

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

Equations

• PadicInt.instInhabitedPadicInt = { default := 0 }

instance PadicInt.instOnePadicInt {p : ℕ} [Fact (Nat.Prime p)] : One ℤ_[p]

One on ℤ_[p] is inherited from ℚ_[p].

Equations

• PadicInt.instOnePadicInt = { one := { val := 1, property := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

instance PadicInt.instAddCommGroupPadicInt {p : ℕ} [Fact (Nat.Prime p)] : AddCommGroup ℤ_[p]

Equations

• PadicInt.instAddCommGroupPadicInt = inferInstance

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

Equations

• PadicInt.instCommRing = inferInstance

@[simp]

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

@[simp]

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

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

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

Equations

• PadicInt.Coe.ringHom = Subring.subtype (PadicInt.subring p)

@[simp]

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

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

def PadicInt.inv {p : ℕ} [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.

Equations

• PadicInt.inv x = match x with | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := ⋯ } else 0

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

Equations

• ⋯ = ⋯

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

def PadicInt.ofIntSeq {p : ℕ} [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.

Equations

• PadicInt.ofIntSeq seq h = { val := ⟦{ val := fun (n : ℕ) => ↑(seq n), property := h }⟧, property := ⋯ }

Instances

We now show that ℤ_[p] is a

• complete metric space
• normed ring
• integral domain

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

Equations

• PadicInt.instMetricSpacePadicInt p = Subtype.metricSpace

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

Equations

• ⋯ = ⋯

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

Equations

• PadicInt.instNormPadicInt p = { norm := fun (z : ℤ_[p]) => ‖↑z‖ }

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

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

Equations

• PadicInt.instNormedCommRingPadicInt p = let __src := PadicInt.instCommRing; NormedCommRing.mk ⋯

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

Equations

• ⋯ = ⋯

instance PadicInt.isAbsoluteValue (p : ℕ) [Fact (Nat.Prime p)] : IsAbsoluteValue fun (z : ℤ_[p]) => ‖z‖

Equations

• ⋯ = ⋯

instance PadicInt.instIsDomainPadicIntToSemiringToCommSemiringInstCommRing {p : ℕ} [Fact (Nat.Prime p)] : IsDomain ℤ_[p]

Equations

• ⋯ = ⋯

Norm

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

@[simp]

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

@[simp]

theorem PadicInt.norm_pow {p : ℕ} [Fact (Nat.Prime p)] (z : ℤ_[p]) (n : ℕ) : ‖z ^ n‖ = ‖z‖ ^ n

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

Valuation on ℤ_[p]

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

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

Equations

• PadicInt.valuation x = Padic.valuation ↑x

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

Units of ℤ_[p]

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

theorem PadicInt.inv_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} (hz : ‖z‖ = 1) : PadicInt.inv z * 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 : ℤ_[p]} {z2 : ℤ_[p]} (hz1 : ‖z1‖ < 1) (hz2 : ‖z2‖ < 1) : ‖z1 + z2‖ < 1

theorem PadicInt.norm_lt_one_mul {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 : ℤ_[p]} {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

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].

Equations

• PadicInt.mkUnits h = let z := { val := u, property := ⋯ }; { val := z, inv := PadicInt.inv z, val_inv := ⋯, inv_val := ⋯ }

@[simp]

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

@[simp]

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

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.

Equations

• PadicInt.unitCoeff hx = let u := ↑x * ↑p ^ (-PadicInt.valuation x); let_fun hu := ⋯; PadicInt.mkUnits hu

@[simp]

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

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

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 ≤ PadicInt.valuation x

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 ≤ PadicInt.valuation x

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.instLocalRingPadicIntToSemiringToCommSemiringInstCommRing {p : ℕ} [hp : Fact (Nat.Prime p)] : LocalRing ℤ_[p]

Equations

• ⋯ = ⋯

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

theorem PadicInt.maximalIdeal_eq_span_p {p : ℕ} [hp : Fact (Nat.Prime p)] : LocalRing.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.instDiscreteValuationRingPadicIntInstCommRingInstIsDomainPadicIntToSemiringToCommSemiringInstCommRing {p : ℕ} [hp : Fact (Nat.Prime p)] : DiscreteValuationRing ℤ_[p]

Equations

• ⋯ = ⋯

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.instIsAdicCompletePadicIntInstCommRingMaximalIdealToCommSemiringInstLocalRingPadicIntToSemiringToCommSemiringInstCommRingInstAddCommGroupPadicIntToModuleToSemiring {p : ℕ} [hp : Fact (Nat.Prime p)] : IsAdicComplete (LocalRing.maximalIdeal ℤ_[p]) ℤ_[p]

Equations

• ⋯ = ⋯

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

Equations

• PadicInt.algebra = Algebra.ofSubring (PadicInt.subring 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]

Equations

• ⋯ = ⋯