The disc decomposition of ℤ_p

For h : ℕ, the residue classes a ∈ ZMod (p ^ h) cut ℤ_p into the discs a + pʰℤ_p, where a is represented by its natural representative a.val < pʰ. On the disc of a the coordinate w = (x - a.val) / pʰ runs through ℤ_p.

Main definitions

• PadicInt.discHomeomorph p h: the homeomorphism ZMod (pʰ) × ℤ_p ≃ₜ ℤ_p, (a, w) ↦ a.val + pʰ w.

Main results

• PadicInt.toZModPow_natCast_val_add_mul: the point a.val + pʰ w reduces to a modulo pʰ.
• PadicInt.fst_discHomeomorph_symm: the disc of x is its residue class modulo pʰ.
• PadicInt.natCast_val_toZModPow_add_mul_snd_discHomeomorph_symm: x is the natural representative of its residue class plus pʰ times its disc coordinate.
• PadicInt.discHomeomorph_symm_natCast_val_add_mul: the inverse decomposition of a.val + pʰ w is (a, w).
• PadicInt.discHomeomorph_symm_cast_add_mul: the same statement in simp normal form.

theorem PadicInt.toZModPow_natCast_val_add_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (a : ZMod (p ^ h)) (w : ℤ_[p]) : (toZModPow h) (↑a.val + ↑p ^ h * w) = a

The point a.val + pʰ w of the disc of a reduces to a modulo pʰ.

noncomputable def PadicInt.discHomeomorph (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) : ZMod (p ^ h) × ℤ_[p] ≃ₜ ℤ_[p]

The decomposition of ℤ_p into the discs a + pʰℤ_p, a ∈ ZMod (pʰ): the homeomorphism ZMod (pʰ) × ℤ_p ≃ₜ ℤ_p sending (a, w) to a.val + pʰ w, where a.val < pʰ is the natural representative of a. Its inverse sends x to its residue class modulo pʰ and to the disc coordinate w = (x - a.val) / pʰ.

@[simp]

theorem PadicInt.discHomeomorph_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (y : ZMod (p ^ h) × ℤ_[p]) : (discHomeomorph p h) y = ↑y.1.val + ↑p ^ h * y.2

@[simp]

theorem PadicInt.fst_discHomeomorph_symm {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (x : ℤ_[p]) : ((discHomeomorph p h).symm x).1 = (toZModPow h) x

The first component of the inverse disc decomposition is reduction modulo pʰ.

theorem PadicInt.natCast_val_toZModPow_add_mul_snd_discHomeomorph_symm {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (x : ℤ_[p]) : ↑((toZModPow h) x).val + ↑p ^ h * ((discHomeomorph p h).symm x).2 = x

The second component of the inverse disc decomposition is the disc coordinate: x is the natural representative of its residue class modulo pʰ plus pʰ times it.

theorem PadicInt.discHomeomorph_symm_natCast_val_add_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (a : ZMod (p ^ h)) (w : ℤ_[p]) : (discHomeomorph p h).symm (↑a.val + ↑p ^ h * w) = (a, w)

The inverse disc decomposition of a.val + pʰ w is (a, w).

@[simp]

theorem PadicInt.discHomeomorph_symm_cast_add_mul {p : ℕ} [hp : Fact (Nat.Prime p)] (h : ℕ) (a : ZMod (p ^ h)) (w : ℤ_[p]) : (discHomeomorph p h).symm (a.cast + ↑p ^ h * w) = (a, w)

The inverse disc decomposition of a + pʰ w is (a, w), with a cast to ℤ_p through its natural representative. This is the simp normal form of discHomeomorph_symm_natCast_val_add_mul, since ZMod.natCast_val rewrites a.val to a.cast.