Relating ℤ_[p] to ZMod (p ^ n)

In this file we establish connections between the p-adic integers $\mathbb{Z}_p$ and the integers modulo powers of p, $\mathbb{Z}/p^n\mathbb{Z}$.

Main declarations

We show that $\mathbb{Z}_p$ has a ring hom to $\mathbb{Z}/p^n\mathbb{Z}$ 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 hom to ZMod p
• PadicInt.toZModPow: ring hom to ZMod (p^n)
• PadicInt.ker_toZMod / PadicInt.ker_toZModPow: the kernels of these maps are the ideals generated by p^n

We also establish the universal property of $\mathbb{Z}_p$ as a projective limit. Given a family of compatible ring homs $f_k : R \to \mathbb{Z}/p^n\mathbb{Z}$, there is a unique limit $R \to \mathbb{Z}_p$.

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

Implementation notes

The ring hom constructions 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 * Nat.gcdA r.den p % ↑p

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

theorem PadicInt.modPart_nonneg {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) : 0 ≤ PadicInt.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 * Nat.gcdA r.den p % ↑p * ↑r.den

theorem PadicInt.norm_sub_modPart {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1) : ‖{ val := ↑r, property := h } - ↑(PadicInt.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 ∧ ‖{ val := ↑r, property := 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 ∈ LocalRing.maximalIdeal ℤ_[p]) (hn : x - ↑n ∈ LocalRing.maximalIdeal ℤ_[p]) : ↑m = ↑n

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

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

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

Equations

• PadicInt.zmodRepr x = Classical.choose (_ : ∃ n < p, x - ↑n ∈ LocalRing.maximalIdeal ℤ_[p])

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

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

theorem PadicInt.sub_zmodRepr_mem {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x - ↑(PadicInt.zmodRepr x) ∈ LocalRing.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

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

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

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

theorem PadicInt.toZMod_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) : x - ZMod.cast (PadicInt.toZMod x) ∈ LocalRing.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 PadicInt.toZMod = LocalRing.maximalIdeal ℤ_[p]

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.
• PadicInt.appr x 0 = 0

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

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

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

theorem PadicInt.appr_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : x - ↑(PadicInt.appr x 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

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

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

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

@[simp]

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

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

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

Universal property as projective limit

def PadicInt.nthHom {p : ℕ} {R : Type u_1} [NonAssocSemiring R] (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 = ↑(ZMod.val ((f n) r))

@[simp]

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

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

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

def PadicInt.nthHomSeq {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (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

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

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

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

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

def PadicInt.limNthHom {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (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) (_ : IsCauSeq (padicNorm p) fun (n : ℕ) => ↑(PadicInt.nthHom (fun (k2 : ℕ) => f k2) r n))

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

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

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

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

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

def PadicInt.lift {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (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

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

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

theorem PadicInt.lift_spec {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1) (n : ℕ) : RingHom.comp (PadicInt.toZModPow n) (PadicInt.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 {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {R : Type u_1} [NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1) (g : R →+* ℤ_[p]) (hg : ∀ (n : ℕ), RingHom.comp (PadicInt.toZModPow n) g = f n) : PadicInt.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]) : (PadicInt.lift (_ : ∀ (m n : ℕ) (h : m ≤ n), RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (PadicInt.toZModPow n) = PadicInt.toZModPow m)) z = z

theorem PadicInt.ext_of_toZModPow {p : ℕ} [hp_prime : Fact (Nat.Prime p)] {x : ℤ_[p]} {y : ℤ_[p]} : (∀ (n : ℕ), (PadicInt.toZModPow n) x = (PadicInt.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 : R →+* ℤ_[p]} {g' : R →+* ℤ_[p]} : (∀ (n : ℕ), RingHom.comp (PadicInt.toZModPow n) g = RingHom.comp (PadicInt.toZModPow n) g') ↔ g = g'