# 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.

• padic_int.to_zmod: ring hom to zmod p
• padic_int.to_zmod_pow: ring hom to zmod (p^n)
• padic_int.ker_to_zmod / padic_int.ker_to_zmod_pow: 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$.

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

## Implementation notes #

The ring hom constructions go through an auxiliary constructor padic_int.to_zmod_hom, which removes some boilerplate code.

### Ring homomorphisms to zmod p and zmod (p ^ n)#

def padic_int.mod_part (p : ) (r : ) :

mod_part p r is an integer that satisfies ∥(r - mod_part p r : ℚ_[p])∥ < 1 when ∥(r : ℚ_[p])∥ ≤ 1, see padic_int.norm_sub_mod_part. It is the unique non-negative integer that is < p with this property.

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

Equations
theorem padic_int.mod_part_lt_p {p : } [hp_prime : fact (nat.prime p)] (r : ) :
< p
theorem padic_int.mod_part_nonneg {p : } [hp_prime : fact (nat.prime p)] (r : ) :
0
theorem padic_int.is_unit_denom {p : } [hp_prime : fact (nat.prime p)] (r : ) (h : r 1) :
theorem padic_int.norm_sub_mod_part_aux {p : } [hp_prime : fact (nat.prime p)] (r : ) (h : r 1) :
p r.num - ((r.num) * r.denom.gcd_a p % p) * (r.denom)
theorem padic_int.norm_sub_mod_part {p : } [hp_prime : fact (nat.prime p)] (r : ) (h : r 1) :
r, h⟩ - r) < 1
theorem padic_int.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 padic_int.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}) :
theorem padic_int.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}) :
theorem padic_int.zmod_congr_of_sub_mem_max_ideal {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (m n : ) (hm : x - m ) (hn : x - n ) :
theorem padic_int.exists_mem_range {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
∃ (n : ), n < p
def padic_int.zmod_repr {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
theorem padic_int.zmod_repr_spec {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
theorem padic_int.zmod_repr_lt_p {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
theorem padic_int.sub_zmod_repr_mem {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
def padic_int.to_zmod_hom {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) :

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

Equations
def padic_int.to_zmod {p : } [hp_prime : fact (nat.prime p)] :

to_zmod is a ring hom from ℤ_[p] to zmod p, with the equality to_zmod x = (zmod_repr x : zmod p).

Equations
theorem padic_int.to_zmod_spec {p : } [hp_prime : fact (nat.prime p)] (z : ℤ_[p]) :

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

The coercion from zmod p to ℤ_[p] is zmod.has_coe_t, which coerces zmod p into artibrary 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 padic_int.ker_to_zmod {p : } [hp_prime : fact (nat.prime p)] :
def padic_int.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
theorem padic_int.appr_lt {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ) :
x.appr n < p ^ n
theorem padic_int.appr_mono {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
theorem padic_int.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 padic_int.appr_spec {p : } [hp_prime : fact (nat.prime p)] (n : ) (x : ℤ_[p]) :
x - (x.appr n) ideal.span {p ^ n}
def padic_int.to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (n : ) :

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

Equations
theorem padic_int.ker_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (n : ) :
@[simp]
theorem padic_int.zmod_cast_comp_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (m n : ) (h : m n) :
(zmod (p ^ m))).comp =
@[simp]
theorem padic_int.cast_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (m n : ) (h : m n) (x : ℤ_[p]) :
x) =
theorem padic_int.dense_range_nat_cast {p : } [hp_prime : fact (nat.prime p)] :
theorem padic_int.dense_range_int_cast {p : } [hp_prime : fact (nat.prime p)] :

### Universal property as projective limit #

def padic_int.nth_hom {p : } {R : Type u_1} [comm_ring R] (f : Π (k : ), R →+* zmod (p ^ k)) (r : R) :

Given a family of ring homs f : Π n : ℕ, R →+* zmod (p ^ n), nth_hom 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
@[simp]
theorem padic_int.nth_hom_zero {p : } {R : Type u_1} [comm_ring R] (f : Π (k : ), R →+* zmod (p ^ k)) :
= 0
theorem padic_int.pow_dvd_nth_hom_sub {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) (i j : ) (h : i j) :
p ^ i j - i
theorem padic_int.is_cau_seq_nth_hom {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) :
(λ (n : ), n))
def padic_int.nth_hom_seq {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) :

nth_hom_seq f_compat r bundles padic_int.nth_hom 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
theorem padic_int.nth_hom_seq_one {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) :
theorem padic_int.nth_hom_seq_add {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r s : R) :
theorem padic_int.nth_hom_seq_mul {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r s : R) :
def padic_int.lim_nth_hom {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) :

lim_nth_hom 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 padic_int.lift.

Equations
theorem padic_int.lim_nth_hom_spec {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) (ε : ) :
0 < ε(∃ (N : ), ∀ (n : ), n Npadic_int.lim_nth_hom f_compat r - n) < ε)
theorem padic_int.lim_nth_hom_zero {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) :
theorem padic_int.lim_nth_hom_one {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) :
theorem padic_int.lim_nth_hom_add {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r s : R) :
theorem padic_int.lim_nth_hom_mul {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r s : R) :
def padic_int.lift {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (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 = padic_int.lim_nth_hom f_compat r.

Equations
theorem padic_int.lift_sub_val_mem_span {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) (n : ) :
(padic_int.lift f_compat) r - (((f n) r).val) ideal.span {p ^ n}
theorem padic_int.lift_spec {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (n : ) :

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

theorem padic_int.lift_unique {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [comm_ring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : ∀ (k1 k2 : ) (hk : k1 k2), (zmod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]) (hg : ∀ (n : ), = f n) :
One part of the universal property of ℤ_[p] as a projective limit. See also padic_int.lift_spec.