mathlib3 documentation

number_theory.padics.ring_homs

Relating ℤ_[p] to zmod (p ^ n) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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 : ) :
theorem padic_int.mod_part_nonneg {p : } [hp_prime : fact (nat.prime p)] (r : ) :
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) :
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.exists_mem_range {p : } [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :
noncomputable 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_lt_p {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
noncomputable 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

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.

@[irreducible]
noncomputable def padic_int.appr {p : } [hp_prime : fact (nat.prime 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}
noncomputable 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
@[simp]
theorem padic_int.zmod_cast_comp_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (m n : ) (h : m n) :
@[simp]
theorem padic_int.cast_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] (m n : ) (h : m n) (x : ℤ_[p]) :

Universal property as projective limit #

def padic_int.nth_hom {p : } {R : Type u_1} [non_assoc_semiring 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} [non_assoc_semiring R] (f : Π (k : ), R →+* zmod (p ^ k)) :
theorem padic_int.pow_dvd_nth_hom_sub {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) (i j : ) (h : i j) :
theorem padic_int.is_cau_seq_nth_hom {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) :
def padic_int.nth_hom_seq {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (zmod (p ^ k1))).comp (f k2) = f k1) (r : R) (ε : ) :
0 < ε ( (N : ), (n : ), n N padic_int.lim_nth_hom f_compat r - (padic_int.nth_hom f r n) < ε)
theorem padic_int.lim_nth_hom_zero {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (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} [non_assoc_semiring R] {f : Π (k : ), R →+* zmod (p ^ k)} (f_compat : (k1 k2 : ) (hk : k1 k2), (zmod.cast_hom _ (zmod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]) (hg : (n : ), (padic_int.to_zmod_pow n).comp g = f n) :
padic_int.lift f_compat = g

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

theorem padic_int.ext_of_to_zmod_pow {p : } [hp_prime : fact (nat.prime p)] {x y : ℤ_[p]} :
theorem padic_int.to_zmod_pow_eq_iff_ext {p : } [hp_prime : fact (nat.prime p)] {R : Type u_1} [non_assoc_semiring R] {g g' : R →+* ℤ_[p]} :