Documentation

Mathlib.NumberTheory.Padics.PadicIntegers

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 : ℕ) [Fact (Nat.Prime p)] :

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

Equations

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

Instances For

def «termℤ_[_]» :

Lean.ParserDescr

The ring of p-adic integers.

Equations

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

Instances For

Ring structure and coercion to `ℚ_[p]` #

instance PadicInt.instCoePadic {p : ℕ} [Fact (Nat.Prime p)] :

Coe ℤ_[p] ℚ_[p]

Equations

PadicInt.instCoePadic = { 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

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

Instances For

@[simp]

theorem PadicInt.mem_subring_iff (p : ℕ) [Fact (Nat.Prime p)] {x : ℚ_[p]} :

x ∈ PadicInt.subring p ↔ ‖x‖ ≤ 1

instance PadicInt.instAdd {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

PadicInt.instAdd = inferInstance

instance PadicInt.instMul {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

PadicInt.instMul = inferInstance

instance PadicInt.instNeg {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

PadicInt.instNeg = inferInstance

instance PadicInt.instSub {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

PadicInt.instSub = inferInstance

instance PadicInt.instZero {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

PadicInt.instZero = inferInstance

instance PadicInt.instInhabited {p : ℕ} [Fact (Nat.Prime p)] :

Inhabited ℤ_[p]

Equations

PadicInt.instInhabited = { default := 0 }

instance PadicInt.instOne {p : ℕ} [Fact (Nat.Prime p)] :

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

Equations

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

@[simp]

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

⟨0, 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.instAddCommGroup {p : ℕ} [Fact (Nat.Prime p)] :

AddCommGroup ℤ_[p]

Equations

PadicInt.instAddCommGroup = inferInstance

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

CommRing ℤ_[p]

Equations

PadicInt.instCommRing = inferInstance

@[simp]

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

↑↑n = ↑n

@[deprecated PadicInt.coe_natCast]

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

↑↑n = ↑n

Alias of PadicInt.coe_natCast.

@[simp]

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

↑↑z = ↑z

@[deprecated PadicInt.coe_intCast]

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

↑↑z = ↑z

Alias of PadicInt.coe_intCast.

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 = (PadicInt.subring p).subtype

Instances For

@[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]) :

⟨↑k, ⋯⟩ = 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

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

Instances For

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

CharZero ℤ_[p]

Equations

⋯ = ⋯

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

↑z1 = ↑z2 ↔ z1 = z2

@[deprecated PadicInt.intCast_eq]

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

↑z1 = ↑z2 ↔ z1 = z2

Alias of PadicInt.intCast_eq.

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

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 For

Instances #

We now show that ℤ_[p] is a

complete metric space
normed ring
integral domain

instance PadicInt.instMetricSpace (p : ℕ) [Fact (Nat.Prime p)] :

MetricSpace ℤ_[p]

Equations

PadicInt.instMetricSpace p = Subtype.metricSpace

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

CompleteSpace ℤ_[p]

Equations

⋯ = ⋯

instance PadicInt.instNorm (p : ℕ) [Fact (Nat.Prime p)] :

Equations

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

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

‖z‖ = ‖↑z‖

instance PadicInt.instNormedCommRing (p : ℕ) [Fact (Nat.Prime p)] :

NormedCommRing ℤ_[p]

Equations

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

instance PadicInt.instNormOneClass (p : ℕ) [Fact (Nat.Prime p)] :

NormOneClass ℤ_[p]

Equations

⋯ = ⋯

instance PadicInt.isAbsoluteValue (p : ℕ) [Fact (Nat.Prime p)] :

IsAbsoluteValue fun (z : ℤ_[p]) => ‖z‖

Equations

⋯ = ⋯

instance PadicInt.instIsDomain {p : ℕ} [Fact (Nat.Prime p)] :

IsDomain ℤ_[p]

Equations

⋯ = ⋯

Norm #

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

@[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_intCast_eq_padic_norm {p : ℕ} [Fact (Nat.Prime p)] (z : ℤ) :

‖↑z‖ = ‖↑z‖

@[deprecated PadicInt.norm_intCast_eq_padic_norm]

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

‖↑z‖ = ‖↑z‖

Alias of PadicInt.norm_intCast_eq_padic_norm.

@[simp]

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

‖⟨q, 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

x.valuation = (↑x).valuation

Instances For

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

‖x‖ = ↑p ^ (-x.valuation)

@[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)] :

(↑p).valuation = 1

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

0 ≤ 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 : ℤ_[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) :

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 := ⋯ }

Instances For

@[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) :

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

Instances For

@[simp]

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

↑↑(PadicInt.unitCoeff hx) = ↑x * ↑p ^ (-x.valuation)

theorem PadicInt.unitCoeff_spec {p : ℕ} [hp : Fact (Nat.Prime p)] {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 (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.instLocalRing {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.instDiscreteValuationRing {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.instIsAdicCompleteMaximalIdeal {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

⋯ = ⋯