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 tozmod p
padic_int.to_zmod_pow
: ring hom tozmod (p^n)
padic_int.ker_to_zmod
/padic_int.ker_to_zmod_pow
: the kernels of these maps are the ideals generated byp^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 functionpadic_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.
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]
.)
to_zmod_hom
is an auxiliary constructor for creating ring homs from ℤ_[p]
to zmod v
.
to_zmod
is a ring hom from ℤ_[p]
to zmod p
,
with the equality to_zmod x = (zmod_repr x : zmod p)
.
Equations
- padic_int.to_zmod = padic_int.to_zmod_hom p padic_int.zmod_repr padic_int.to_zmod._proof_1 padic_int.to_zmod._proof_2
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.
appr n x
gives a value v : ℕ
such that x
and ↑v : ℤ_p
are congruent mod p^n
.
See appr_spec
.
A ring hom from ℤ_[p]
to zmod (p^n)
, with underlying function padic_int.appr n
.
Equations
- padic_int.to_zmod_pow n = padic_int.to_zmod_hom (p ^ n) (λ (x : ℤ_[p]), x.appr n) _ _
Universal property as projective limit #
Given a family of ring homs f : Π n : ℕ, R →+* zmod (p ^ n)
,
nth_hom f r
is an integer-valued sequence
whose n
th value is the unique integer k
such that 0 ≤ k < p ^ n
and f n r = (k : zmod (p ^ n))
.
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 n
th value of the sequence is ((f n r).val : ℚ)
.
Equations
- padic_int.nth_hom_seq f_compat r = ⟨λ (n : ℕ), ↑(padic_int.nth_hom f r n), _⟩
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
- padic_int.lim_nth_hom f_compat r = padic_int.of_int_seq (padic_int.nth_hom f r) _
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
- padic_int.lift f_compat = {to_fun := padic_int.lim_nth_hom f_compat, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
One part of the universal property of ℤ_[p]
as a projective limit.
See also padic_int.lift_unique
.
One part of the universal property of ℤ_[p]
as a projective limit.
See also padic_int.lift_spec
.