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.
padic_int.to_zmod: ring hom tozmod ppadic_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 nth 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 nth 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.