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 p.Prime] : 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.instCoePadic {p : ℕ} [Fact p.Prime] : Coe ℤ_[p] ℚ_[p]

Equations

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

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

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

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

Equations

• PadicInt.subring p = { carrier := {x : ℚ_[p] | ‖x‖ ≤ 1}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

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

instance PadicInt.instAdd {p : ℕ} [Fact p.Prime] : Add ℤ_[p]

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

Equations

• PadicInt.instAdd = inferInstance

instance PadicInt.instMul {p : ℕ} [Fact p.Prime] : Mul ℤ_[p]

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

Equations

• PadicInt.instMul = inferInstance

instance PadicInt.instNeg {p : ℕ} [Fact p.Prime] : Neg ℤ_[p]

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

Equations

• PadicInt.instNeg = inferInstance

instance PadicInt.instSub {p : ℕ} [Fact p.Prime] : Sub ℤ_[p]

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

Equations

• PadicInt.instSub = inferInstance

instance PadicInt.instZero {p : ℕ} [Fact p.Prime] : Zero ℤ_[p]

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

Equations

• PadicInt.instZero = inferInstance

instance PadicInt.instInhabited {p : ℕ} [Fact p.Prime] : Inhabited ℤ_[p]

Equations

• PadicInt.instInhabited = { default := 0 }

instance PadicInt.instOne {p : ℕ} [Fact p.Prime] : One ℤ_[p]

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

Equations

• PadicInt.instOne = { one := ⟨1, ⋯⟩ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

instance PadicInt.instAddCommGroup {p : ℕ} [Fact p.Prime] : AddCommGroup ℤ_[p]

Equations

• PadicInt.instAddCommGroup = inferInstance

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

Equations

• PadicInt.instCommRing = inferInstance

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

def PadicInt.inv {p : ℕ} [Fact p.Prime] : ℤ_[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

• x.inv = match x with | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0

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

Equations

• ⋯ = ⋯

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

@[deprecated PadicInt.intCast_eq]

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

Alias of PadicInt.intCast_eq.

def PadicInt.ofIntSeq {p : ℕ} [Fact p.Prime] (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 = ⟨⟦⟨fun (n : ℕ) => ↑(seq n), h⟩⟧, ⋯⟩

Instances

We now show that ℤ_[p] is a

• complete metric space
• normed ring
• integral domain

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

Equations

• PadicInt.instMetricSpace p = Subtype.metricSpace

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

Equations

• ⋯ = ⋯

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

Equations

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

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance PadicInt.instIsDomain {p : ℕ} [Fact p.Prime] : IsDomain ℤ_[p]

Equations

• ⋯ = ⋯

Norm

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

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

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

Valuation on ℤ_[p]

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

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

Equations

• x.valuation = (↑x).valuation

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

Units of ℤ_[p]

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

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

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

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

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

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

def PadicInt.mkUnits {p : ℕ} [hp : Fact p.Prime] {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 := ⟨u, ⋯⟩; { val := z, inv := z.inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

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

@[simp]

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

def PadicInt.unitCoeff {p : ℕ} [hp : Fact p.Prime] {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 ^ (-x.valuation); let_fun hu := ⋯; PadicInt.mkUnits hu

@[simp]

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

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

Various characterizations of open unit balls

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

theorem PadicInt.mem_span_pow_iff_le_valuation {p : ℕ} [hp : Fact p.Prime] (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 p.Prime] (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 p.Prime] (x : ℤ_[p]) (n : ℤ) : ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

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

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

@[simp]

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

Discrete valuation ring

instance PadicInt.instLocalRing {p : ℕ} [hp : Fact p.Prime] : LocalRing ℤ_[p]

Equations

• ⋯ = ⋯

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

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

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

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

instance PadicInt.instDiscreteValuationRing {p : ℕ} [hp : Fact p.Prime] : DiscreteValuationRing ℤ_[p]

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• PadicInt.algebra = Algebra.ofSubring (PadicInt.subring p)

@[simp]

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

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

Equations

• ⋯ = ⋯