Relating ℤ_[p] to ZMod (p ^ n), aka ℤ/p^nℤ.

In this file we establish connections between the p-adic integers ℤ_[p] and the integers modulo powers of p, ℤ/p^nℤ, implemented as ZMod (p^n).

Main declarations

We show that ℤ_[p] has a ring homomorphism to ℤ/p^nℤ for each n. The case for n = 1 is handled separately, since it is used in the general construction and we may want to use it without the ^1 getting in the way.

• PadicInt.toZMod: ring homomorphism to ℤ/pℤ, implemented as ZMod p.
• PadicInt.toZModPow: ring homomorphism to ℤ/p^nℤ, implemented as ZMod (p^n).
• PadicInt.ker_toZMod / PadicInt.ker_toZModPow: the kernels of these maps are the ideals generated by p^n
• PadicInt.residueField shows that the residue field of ℤ_[p] is isomorhic to ``ℤ/pℤ`.

We also establish the universal property of ℤ_[p] as a projective limit. Given a family of compatible ring homomorphisms f_k : R → ℤ/p^nℤ, there is a unique limit R → ℤ_[p]

• PadicInt.lift: the limit function
• PadicInt.lift_spec / PadicInt.lift_unique: the universal property

Implementation notes

The constructions of the ring homomorphisms go through an auxiliary constructor PadicInt.toZModHom, which removes some boilerplate code.

Ring homomorphisms to ZMod p and ZMod (p ^ n)

def PadicInt.modPart (p : ℕ) (r : ℚ) : ℤ

modPart p r is an integer that satisfies ‖(r - modPart p r : ℚ_[p])‖ < 1 when ‖(r : ℚ_[p])‖ ≤ 1, see PadicInt.norm_sub_modPart. It is the unique non-negative integer that is < p with this property.

(Note that this definition assumes r : ℚ. See PadicInt.zmodRepr for a version that takes values in ℕ and works for arbitrary x : ℤ_[p].)

Equations

• PadicInt.modPart p r = r.num * r.den.gcdA p % ↑p

theorem PadicInt.modPart_lt_p {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) : modPart p r < ↑p

theorem PadicInt.modPart_nonneg {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) : 0 ≤ modPart p r

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

theorem PadicInt.norm_sub_modPart_aux {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1) : ↑p ∣ r.num - r.num * r.den.gcdA p % ↑p * ↑r.den

theorem PadicInt.norm_sub_modPart {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1) : ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1

theorem PadicInt.exists_mem_range_of_norm_rat_le_one {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1) : ∃ (n : ℤ), 0 ≤ n ∧ n < ↑p ∧ ‖⟨↑r, h⟩ - ↑n‖ < 1

theorem PadicInt.zmod_congr_of_sub_mem_span_aux {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) (a b : ℤ) (ha : x - ↑a ∈ Ideal.span {↑p ^ n}) (hb : x - ↑b ∈ Ideal.span {↑p ^ n}) : ↑a = ↑b

theorem PadicInt.zmod_congr_of_sub_mem_span {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) (a b : ℕ) (ha : x - ↑a ∈ Ideal.span {↑p ^ n}) (hb : x - ↑b ∈ Ideal.span {↑p ^ n}) : ↑a = ↑b

theorem PadicInt.zmod_congr_of_sub_mem_max_ideal {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (m n : ℕ) (hm : x - ↑m ∈ IsLocalRing.maximalIdeal ℤ_[p]) (hn : x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]) : ↑m = ↑n

theorem PadicInt.exists_mem_range {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : ∃ n < p, x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]

theorem PadicInt.existsUnique_mem_range {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : ∃! n : ℕ, n < p ∧ x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]

@[deprecated PadicInt.existsUnique_mem_range (since := "2024-12-17")]

theorem PadicInt.exists_unique_mem_range {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : ∃! n : ℕ, n < p ∧ x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p]

Alias of PadicInt.existsUnique_mem_range.

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

zmodRepr x is the unique natural number smaller than p satisfying ‖(x - zmodRepr x : ℤ_[p])‖ < 1.

Equations

• x.zmodRepr = Classical.choose ⋯

theorem PadicInt.zmodRepr_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x.zmodRepr < p ∧ x - ↑x.zmodRepr ∈ IsLocalRing.maximalIdeal ℤ_[p]

theorem PadicInt.zmodRepr_unique {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (y : ℕ) (hy₁ : y < p) (hy₂ : x - ↑y ∈ IsLocalRing.maximalIdeal ℤ_[p]) : y = x.zmodRepr

theorem PadicInt.zmodRepr_lt_p {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x.zmodRepr < p

theorem PadicInt.sub_zmodRepr_mem {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x - ↑x.zmodRepr ∈ IsLocalRing.maximalIdeal ℤ_[p]

def PadicInt.toZModHom {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (v : ℕ) (f : ℤ_[p] → ℕ) (f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}) (f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b) : ℤ_[p] →+* ZMod v

toZModHom is an auxiliary constructor for creating ring homs from ℤ_[p] to ZMod v.

Equations

• PadicInt.toZModHom v f f_spec f_congr = { toFun := fun (x : ℤ_[p]) => ↑(f x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def PadicInt.toZMod {p : ℕ} [hp_prime : Fact (Nat.Prime p)] : ℤ_[p] →+* ZMod p

toZMod is a ring hom from ℤ_[p] to ZMod p, with the equality toZMod x = (zmodRepr x : ZMod p).

Equations

• PadicInt.toZMod = PadicInt.toZModHom p PadicInt.zmodRepr ⋯ ⋯

theorem PadicInt.toZMod_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x - (toZMod x).cast ∈ IsLocalRing.maximalIdeal ℤ_[p]

z - (toZMod z : ℤ_[p]) is contained in the maximal ideal of ℤ_[p], for every z : ℤ_[p].

The coercion from ZMod p to ℤ_[p] is ZMod.cast, which coerces ZMod p into arbitrary rings. This is unfortunate, but a consequence of the fact that we allow ZMod p to coerce to rings of arbitrary characteristic, instead of only rings of characteristic p. This coercion is only a ring homomorphism if it coerces into a ring whose characteristic divides p. While this is not the case here we can still make use of the coercion.

theorem PadicInt.ker_toZMod {p : ℕ} [hp_prime : Fact (Nat.Prime p)] : RingHom.ker toZMod = IsLocalRing.maximalIdeal ℤ_[p]

def PadicInt.residueField {p : ℕ} [hp_prime : Fact (Nat.Prime p)] : IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p

The equivalence between the residue field of the p-adic integers and ℤ/pℤ

Equations

• PadicInt.residueField = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

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

appr n x gives a value v : ℕ such that x and ↑v : ℤ_p are congruent mod p^n. See appr_spec.

Equations

• One or more equations did not get rendered due to their size.
• x✝.appr 0 = 0

theorem PadicInt.appr_lt {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : x.appr n < p ^ n

theorem PadicInt.appr_mono {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : Monotone x.appr

theorem PadicInt.dvd_appr_sub_appr {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : p ^ m ∣ x.appr n - x.appr m

theorem PadicInt.appr_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

def PadicInt.toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) : ℤ_[p] →+* ZMod (p ^ n)

A ring hom from ℤ_[p] to ZMod (p^n), with underlying function PadicInt.appr n.

Equations

• PadicInt.toZModPow n = PadicInt.toZModHom (p ^ n) (fun (x : ℤ_[p]) => x.appr n) ⋯ ⋯

theorem PadicInt.ker_toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) : RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}

theorem PadicInt.zmod_cast_comp_toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (m n : ℕ) (h : m ≤ n) : (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n) = toZModPow m

@[simp]

theorem PadicInt.cast_toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (m n : ℕ) (h : m ≤ n) (x : ℤ_[p]) : ((toZModPow n) x).cast = (toZModPow m) x

theorem PadicInt.denseRange_natCast {p : ℕ} [hp_prime : Fact (Nat.Prime p)] : DenseRange Nat.cast

theorem PadicInt.denseRange_intCast {p : ℕ} [hp_prime : Fact (Nat.Prime p)] : DenseRange Int.cast

Universal property as projective limit

def PadicInt.nthHom {R : Type u_1} [NonAssocSemiring R] {p : ℕ} (f : (k : ℕ) → R →+* ZMod (p ^ k)) (r : R) : ℕ → ℤ

Given a family of ring homs f : Π n : ℕ, R →+* ZMod (p ^ n), nthHom f r is an integer-valued sequence whose nth value is the unique integer k such that 0 ≤ k < p ^ n and f n r = (k : ZMod (p ^ n)).

Equations

• PadicInt.nthHom f r n = ↑((f n) r).val

@[simp]

theorem PadicInt.nthHom_zero {R : Type u_1} [NonAssocSemiring R] {p : ℕ} (f : (k : ℕ) → R →+* ZMod (p ^ k)) : nthHom f 0 = 0

theorem PadicInt.pow_dvd_nthHom_sub {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (i j : ℕ) (h : i ≤ j) : ↑p ^ i ∣ nthHom f r j - nthHom f r i

theorem PadicInt.isCauSeq_nthHom {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) : IsCauSeq (padicNorm p) fun (n : ℕ) => ↑(nthHom f r n)

def PadicInt.nthHomSeq {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) : PadicSeq p

nthHomSeq f_compat r bundles PadicInt.nthHom f r as a Cauchy sequence of rationals with respect to the p-adic norm. The nth value of the sequence is ((f n r).val : ℚ).

Equations

• PadicInt.nthHomSeq f_compat r = ⟨fun (n : ℕ) => ↑(PadicInt.nthHom f r n), ⋯⟩

theorem PadicInt.nthHomSeq_one {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) : nthHomSeq f_compat 1 ≈ 1

theorem PadicInt.nthHomSeq_add {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R) : nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s

theorem PadicInt.nthHomSeq_mul {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R) : nthHomSeq f_compat (r * s) ≈ nthHomSeq f_compat r * nthHomSeq f_compat s

def PadicInt.limNthHom {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) : ℤ_[p]

limNthHom f_compat r is the limit of a sequence f of compatible ring homs R →+* ZMod (p^k). This is itself a ring hom: see PadicInt.lift.

Equations

• PadicInt.limNthHom f_compat r = PadicInt.ofIntSeq (PadicInt.nthHom f r) ⋯

theorem PadicInt.limNthHom_spec {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

theorem PadicInt.limNthHom_zero {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) : limNthHom f_compat 0 = 0

theorem PadicInt.limNthHom_one {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) : limNthHom f_compat 1 = 1

theorem PadicInt.limNthHom_add {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R) : limNthHom f_compat (r + s) = limNthHom f_compat r + limNthHom f_compat s

theorem PadicInt.limNthHom_mul {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R) : limNthHom f_compat (r * s) = limNthHom f_compat r * limNthHom f_compat s

def PadicInt.lift {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) : R →+* ℤ_[p]

lift f_compat is the limit of a sequence f of compatible ring homs R →+* ZMod (p^k), with the equality lift f_compat r = PadicInt.limNthHom f_compat r.

Equations

• PadicInt.lift f_compat = { toFun := PadicInt.limNthHom f_compat, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem PadicInt.lift_sub_val_mem_span {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (n : ℕ) : (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

theorem PadicInt.lift_spec {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (n : ℕ) : (toZModPow n).comp (lift f_compat) = f n

One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_unique.

theorem PadicInt.lift_unique {R : Type u_1} [NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)] (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]) (hg : ∀ (n : ℕ), (toZModPow n).comp g = f n) : lift f_compat = g

One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_spec.

@[simp]

theorem PadicInt.lift_self {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (z : ℤ_[p]) : (lift ⋯) z = z

theorem PadicInt.ext_of_toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x y : ℤ_[p]} : (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) ↔ x = y

theorem PadicInt.toZModPow_eq_iff_ext {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {g g' : R →+* ℤ_[p]} : (∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g') ↔ g = g'

theorem PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub (f : ℕ → ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i) : IsCauSeq (padicNorm p) fun (x : ℕ) => ↑(f x)

theorem PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub (f : ℕ → ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i) (n : ℕ) : (toZModPow n) (ofIntSeq f ⋯) = ↑(f n)