# 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
• = r.num * r.den.gcdA p % p
Instances For
theorem PadicInt.modPart_lt_p {p : } [hp_prime : Fact p.Prime] (r : ) :
< p
theorem PadicInt.modPart_nonneg {p : } [hp_prime : Fact p.Prime] (r : ) :
0
theorem PadicInt.isUnit_den {p : } [hp_prime : Fact p.Prime] (r : ) (h : r 1) :
IsUnit r.den
theorem PadicInt.norm_sub_modPart_aux {p : } [hp_prime : Fact p.Prime] (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 p.Prime] (r : ) (h : r 1) :
r, h - () < 1
theorem PadicInt.exists_mem_range_of_norm_rat_le_one {p : } [hp_prime : Fact p.Prime] (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 p.Prime] (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 p.Prime] (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 p.Prime] (x : ℤ_[p]) (m : ) (n : ) (hm : x - m ) (hn : x - n ) :
m = n
theorem PadicInt.exists_mem_range {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
n < p, x - n
def PadicInt.zmodRepr {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :

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

Equations
• x.zmodRepr =
Instances For
theorem PadicInt.zmodRepr_spec {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
x.zmodRepr < p x - x.zmodRepr
theorem PadicInt.zmodRepr_lt_p {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
x.zmodRepr < p
theorem PadicInt.sub_zmodRepr_mem {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
x - x.zmodRepr
def PadicInt.toZModHom {p : } [hp_prime : Fact p.Prime] (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) :

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' := }
Instances For
def PadicInt.toZMod {p : } [hp_prime : Fact p.Prime] :

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

Equations
Instances For
theorem PadicInt.toZMod_spec {p : } [hp_prime : Fact p.Prime] (x : ℤ_[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 p.Prime] :
noncomputable def PadicInt.appr {p : } [hp_prime : Fact p.Prime] :
ℤ_[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
Instances For
theorem PadicInt.appr_lt {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) (n : ) :
x.appr n < p ^ n
theorem PadicInt.appr_mono {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
Monotone x.appr
theorem PadicInt.dvd_appr_sub_appr {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) (m : ) (n : ) (h : m n) :
p ^ m x.appr n - x.appr m
theorem PadicInt.appr_spec {p : } [hp_prime : Fact p.Prime] (n : ) (x : ℤ_[p]) :
x - (x.appr n) Ideal.span {p ^ n}
def PadicInt.toZModPow {p : } [hp_prime : Fact p.Prime] (n : ) :

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

Equations
Instances For
theorem PadicInt.ker_toZModPow {p : } [hp_prime : Fact p.Prime] (n : ) :
= Ideal.span {p ^ n}
theorem PadicInt.zmod_cast_comp_toZModPow {p : } [hp_prime : Fact p.Prime] (m : ) (n : ) (h : m n) :
(ZMod.castHom (ZMod (p ^ m))).comp =
@[simp]
theorem PadicInt.cast_toZModPow {p : } [hp_prime : Fact p.Prime] (m : ) (n : ) (h : m n) (x : ℤ_[p]) :
( x).cast = x
theorem PadicInt.denseRange_natCast {p : } [hp_prime : Fact p.Prime] :
DenseRange Nat.cast
theorem PadicInt.denseRange_nat_cast {p : } [hp_prime : Fact p.Prime] :
DenseRange Nat.cast

Alias of PadicInt.denseRange_natCast.

theorem PadicInt.denseRange_intCast {p : } [hp_prime : Fact p.Prime] :
DenseRange Int.cast
theorem PadicInt.denseRange_int_cast {p : } [hp_prime : Fact p.Prime] :
DenseRange Int.cast

Alias of PadicInt.denseRange_intCast.

### Universal property as projective limit #

def PadicInt.nthHom {p : } {R : Type u_1} [] (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
• = ((f n) r).val
Instances For
@[simp]
theorem PadicInt.nthHom_zero {p : } {R : Type u_1} [] (f : (k : ) → R →+* ZMod (p ^ k)) :
= 0
theorem PadicInt.pow_dvd_nthHom_sub {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (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 -
theorem PadicInt.isCauSeq_nthHom {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) :
IsCauSeq () fun (n : ) => ()
def PadicInt.nthHomSeq {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) :

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
Instances For
theorem PadicInt.nthHomSeq_one {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) :
theorem PadicInt.nthHomSeq_add {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (s : R) :
theorem PadicInt.nthHomSeq_mul {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (s : R) :
def PadicInt.limNthHom {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) :

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
Instances For
theorem PadicInt.limNthHom_spec {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (ε : ) :
0 < ε∃ (N : ), nN, PadicInt.limNthHom f_compat r - () < ε
theorem PadicInt.limNthHom_zero {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) :
theorem PadicInt.limNthHom_one {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) :
theorem PadicInt.limNthHom_add {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (s : R) :
theorem PadicInt.limNthHom_mul {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (s : R) :
def PadicInt.lift {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) :

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
Instances For
theorem PadicInt.lift_sub_val_mem_span {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (r : R) (n : ) :
(PadicInt.lift f_compat) r - ((f n) r).val Ideal.span {p ^ n}
theorem PadicInt.lift_spec {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (n : ) :
.comp (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 p.Prime] {R : Type u_1} [] {f : (k : ) → R →+* ZMod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (ZMod.castHom (ZMod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]) (hg : ∀ (n : ), .comp g = f n) :
One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_spec.