Congruence and continuity properties of the truncations of a p-adic integer

Mathlib's PadicInt.appr x n is the natural number below p ^ n congruent to x modulo p ^ n, and PadicInt.toZModPow n is the induced ring homomorphism to ZMod (p ^ n). This file records the arithmetic dictionary between the two, the congruences that make appr behave like a ring homomorphism modulo p ^ n, and the continuity of toZModPow.

The congruences are exactly what is needed to raise an element of p-power order in a monoid to a p-adic exponent: g ^ x.appr n does not change when n grows past the order of g (PadicInt.pow_appr_eq_pow_appr), so such powers assemble into a well-defined action of ℤ_[p].

Main results

• PadicInt.val_toZModPow_eq_appr: appr computes the ZMod (p ^ n)-value of toZModPow.
• PadicInt.continuous_toZModPow, PadicInt.continuous_toZMod: truncation modulo p ^ n and reduction modulo p are continuous, ZMod (p ^ n) and ZMod p carrying the discrete topology.
• PadicInt.toZMod_eq_zero_iff_dvd, PadicInt.toZModPow_eq_zero_iff_dvd: the kernels of reduction and truncation, as divisibility statements.
• PadicInt.cast_toZModPow_eq_toZMod: reducing the truncation modulo p ^ n further modulo p recovers toZMod.
• PadicInt.dvd_sub_appr: x - appr x n is divisible by p ^ n in ℤ_[p].
• PadicInt.appr_modEq, PadicInt.appr_add_modEq, PadicInt.appr_mul_modEq, PadicInt.appr_natCast_modEq: the truncations are compatible with each other and with the ring operations, modulo p ^ n.
• PadicInt.appr_natCast_pow_of_le: the truncation of p ^ m modulo p ^ n is 0 for n ≤ m.
• PadicInt.pow_appr_eq_pow_appr: raising an element of p-power order to the truncated exponent is independent of the truncation level, once that level is large enough.
• PadicInt.quotientSpanPowEquivZMod: toZModPow n identifies ℤ_[p] ⧸ (p ^ n) with ZMod (p ^ n).
• PadicInt.span_singleton_eq_span_pow_valuation, PadicInt.quotientSpanEquivZMod, PadicInt.natCard_quotient_span, PadicInt.isAddCyclic_quotient_span: a nonzero x generates the same ideal as p ^ v for v its valuation, so ℤ_[p] ⧸ (x) is ZMod (p ^ v), a finite ring of cardinality p ^ v whose additive group is cyclic.
• PadicInt.valuation_natCast, PadicInt.valuation_eq_zero_of_isUnit, PadicInt.one_le_valuation_of_dvd: the valuation of a natural number is its p-adic valuation, units have valuation 0, and a nonzero multiple of p has valuation at least 1.
• PadicInt.quotientSpanToZMod, PadicInt.quotientSpanToZModPow: for p ∣ q, respectively p ^ n ∣ q, reduction modulo p, respectively truncation modulo p ^ n, descends to a continuous ring homomorphism out of ℤ_[p] ⧸ (q).
• PadicInt.surjective_units_map_toZModPow: every unit of ZMod (p ^ n) lifts to a unit of ℤ_[p].
• PadicInt.unitsToZModPow: truncation modulo p ^ n on the units of ℤ_[p], as a continuous homomorphism to the units of ZMod (p ^ n).
• PadicInt.finite_residueField, PadicInt.card_residueField: the residue field of ℤ_[p] is finite of cardinality p.

instance PadicInt.finite_residueField {p : ℕ} [hp : Fact (Nat.Prime p)] : Finite (IsLocalRing.ResidueField ℤ_[p])

The residue field of ℤ_p is finite, being ℤ/pℤ.

theorem PadicInt.card_residueField (p : ℕ) [hp : Fact (Nat.Prime p)] : Nat.card (IsLocalRing.ResidueField ℤ_[p]) = p

The residue field of ℤ_p has p elements.

theorem PadicInt.toZModPow_eq_natCast_appr {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : (toZModPow n) x = ↑(x.appr n)

The truncation toZModPow n x is the class of the natural number x.appr n.

theorem PadicInt.val_toZModPow_eq_appr {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ((toZModPow n) x).val = x.appr n

The ZMod (p ^ n)-value of the truncation toZModPow n x is x.appr n.

This is the p ^ n analogue of PadicInt.val_toZMod_eq_zmodRepr.

theorem PadicInt.continuous_toZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : Continuous ⇑(toZModPow n)

Truncation modulo p ^ n is continuous: its fibres are the closed balls of radius p ^ (-n), which are open because the p-adic distance is ultrametric.

theorem PadicInt.continuous_toZMod {p : ℕ} [hp : Fact (Nat.Prime p)] : Continuous ⇑toZMod

Reduction modulo p is continuous: its fibres are those of the truncation toZModPow 1, both kernels being the maximal ideal (p).

theorem PadicInt.toZMod_eq_zero_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : toZMod x = 0 ↔ ↑p ∣ x

A p-adic integer reduces to 0 modulo p exactly when p divides it.

theorem PadicInt.toZModPow_eq_zero_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : (toZModPow n) x = 0 ↔ ↑p ^ n ∣ x

A p-adic integer truncates to 0 modulo p ^ n exactly when p ^ n divides it.

@[simp]

theorem PadicInt.cast_toZModPow_eq_toZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : n ≠ 0) (x : ℤ_[p]) : ((toZModPow n) x).cast = toZMod x

Reducing the truncation x mod p ^ n further modulo p gives x mod p.

@[simp]

theorem PadicInt.dvd_sub_appr {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ↑p ^ n ∣ x - ↑(x.appr n)

The truncation appr x n agrees with x modulo p ^ n: the divisibility form of PadicInt.appr_spec.

theorem PadicInt.appr_modEq {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) {m n : ℕ} (h : m ≤ n) : x.appr n ≡ x.appr m [MOD p ^ m]

A coarser truncation of x is a finer truncation of x read modulo the coarser modulus.

theorem PadicInt.appr_add_modEq {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℤ_[p]) (n : ℕ) : (x + y).appr n ≡ x.appr n + y.appr n [MOD p ^ n]

Truncation is additive modulo p ^ n.

theorem PadicInt.appr_mul_modEq {p : ℕ} [hp : Fact (Nat.Prime p)] (x y : ℤ_[p]) (n : ℕ) : (x * y).appr n ≡ x.appr n * y.appr n [MOD p ^ n]

Truncation is multiplicative modulo p ^ n.

theorem PadicInt.appr_natCast_modEq {p : ℕ} [hp : Fact (Nat.Prime p)] (k n : ℕ) : (↑k).appr n ≡ k [MOD p ^ n]

Truncation fixes a natural number modulo p ^ n.

@[simp]

theorem PadicInt.appr_natCast_pow_of_le {p : ℕ} [hp : Fact (Nat.Prime p)] {m n : ℕ} (h : n ≤ m) : (↑p ^ m).appr n = 0

The truncation of p ^ m modulo p ^ n vanishes when n ≤ m.

noncomputable def PadicInt.quotientSpanPowEquivZMod {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : ℤ_[p] ⧸ Ideal.span {↑p ^ n} ≃+* ZMod (p ^ n)

The truncation toZModPow n identifies the quotient of ℤ_[p] by the ideal (p ^ n) with ZMod (p ^ n). This is the p ^ n analogue of PadicInt.residueField.

Equations

• PadicInt.quotientSpanPowEquivZMod n = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

@[simp]

theorem PadicInt.quotientSpanPowEquivZMod_mk {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (x : ℤ_[p]) : (quotientSpanPowEquivZMod n) ((Ideal.Quotient.mk (Ideal.span {↑p ^ n})) x) = (toZModPow n) x

theorem PadicInt.span_singleton_eq_span_pow_valuation {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : Ideal.span {x} = Ideal.span {↑p ^ x.valuation}

A nonzero p-adic integer x generates the same ideal as p ^ x.valuation, since it is a unit times that power of p.

noncomputable def PadicInt.quotientSpanEquivZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : ℤ_[p] ⧸ Ideal.span {x} ≃+* ZMod (p ^ x.valuation)

The quotient of ℤ_[p] by the ideal generated by a nonzero element x is ZMod (p ^ v), where v is the valuation of x: the ideal (x) is (p ^ v), and toZModPow v identifies the quotient with ZMod (p ^ v).

Equations

• PadicInt.quotientSpanEquivZMod hx = (Ideal.quotEquivOfEq ⋯).trans (PadicInt.quotientSpanPowEquivZMod x.valuation)

@[simp]

theorem PadicInt.quotientSpanEquivZMod_mk {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) (y : ℤ_[p]) : (quotientSpanEquivZMod hx) ((Ideal.Quotient.mk (Ideal.span {x})) y) = (toZModPow x.valuation) y

theorem PadicInt.finite_quotient_span {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : Finite (ℤ_[p] ⧸ Ideal.span {x})

The quotient of ℤ_[p] by the ideal generated by a nonzero element is finite.

theorem PadicInt.natCard_quotient_span {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : Nat.card (ℤ_[p] ⧸ Ideal.span {x}) = p ^ x.valuation

The quotient of ℤ_[p] by the ideal generated by a nonzero element x has p ^ v elements, where v is the valuation of x.

theorem PadicInt.isAddCyclic_quotient_span {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) : IsAddCyclic (ℤ_[p] ⧸ Ideal.span {x})

The additive group of the quotient of ℤ_[p] by the ideal generated by a nonzero element is cyclic, being that of ZMod (p ^ v).

@[simp]

theorem PadicInt.valuation_natCast {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : (↑n).valuation = padicValNat p n

The valuation of a natural number in ℤ_[p] is its p-adic valuation.

theorem PadicInt.valuation_eq_zero_of_isUnit {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : IsUnit x) : x.valuation = 0

A unit of ℤ_[p] has valuation 0.

theorem PadicInt.one_le_valuation_of_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x ≠ 0) (h : ↑p ∣ x) : 1 ≤ x.valuation

A nonzero p-adic integer divisible by p has valuation at least 1.

noncomputable def PadicInt.quotientSpanToZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℤ_[p]} (hq : ↑p ∣ q) : ℤ_[p] ⧸ Ideal.span {q} →+* ZMod p

Reduction modulo p of ℤ_[p] ⧸ (q), for p ∣ q: the ring homomorphism induced by toZMod, whose kernel (p) contains (q).

Equations

• PadicInt.quotientSpanToZMod hq = Ideal.Quotient.lift (Ideal.span {q}) PadicInt.toZMod ⋯

@[simp]

theorem PadicInt.quotientSpanToZMod_mk {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℤ_[p]} (hq : ↑p ∣ q) (x : ℤ_[p]) : (quotientSpanToZMod hq) ((Ideal.Quotient.mk (Ideal.span {q})) x) = toZMod x

Reduction modulo p of the class of x in ℤ_[p] ⧸ (q) is x mod p.

theorem PadicInt.continuous_quotientSpanToZMod {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℤ_[p]} (hq : ↑p ∣ q) : Continuous ⇑(quotientSpanToZMod hq)

Reduction modulo p of ℤ_[p] ⧸ (q) is continuous for the quotient topology.

noncomputable def PadicInt.quotientSpanToZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) {q : ℤ_[p]} (hq : ↑p ^ n ∣ q) : ℤ_[p] ⧸ Ideal.span {q} →+* ZMod (p ^ n)

Truncation modulo p ^ n of ℤ_[p] ⧸ (q), for p ^ n ∣ q: the ring homomorphism induced by toZModPow n, whose kernel (p ^ n) contains (q).

Equations

• PadicInt.quotientSpanToZModPow n hq = Ideal.Quotient.lift (Ideal.span {q}) (PadicInt.toZModPow n) ⋯

@[simp]

theorem PadicInt.quotientSpanToZModPow_mk {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) {q : ℤ_[p]} (hq : ↑p ^ n ∣ q) (x : ℤ_[p]) : (quotientSpanToZModPow n hq) ((Ideal.Quotient.mk (Ideal.span {q})) x) = (toZModPow n) x

Truncation modulo p ^ n of the class of x in ℤ_[p] ⧸ (q) is x mod p ^ n.

theorem PadicInt.continuous_quotientSpanToZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) {q : ℤ_[p]} (hq : ↑p ^ n ∣ q) : Continuous ⇑(quotientSpanToZModPow n hq)

Truncation modulo p ^ n of ℤ_[p] ⧸ (q) is continuous for the quotient topology.

theorem PadicInt.surjective_units_map_toZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : Function.Surjective ⇑(Units.map ↑(toZModPow n))

Every unit of ZMod (p ^ n) lifts to a unit of ℤ_[p]. For n > 0 this holds because truncation is a surjective local homomorphism out of the local ring ℤ_[p]; for n = 0 the target ZMod 1 is the trivial ring, so there is nothing to lift.

noncomputable def PadicInt.unitsToZModPow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : ℤ_[p]ˣ →ₜ* (ZMod (p ^ n))ˣ

Truncation modulo p ^ n on the units of ℤ_[p], as a continuous homomorphism to the units of ZMod (p ^ n).

Equations

• PadicInt.unitsToZModPow n = { toMonoidHom := Units.map ↑(PadicInt.toZModPow n), continuous_toFun := ⋯ }

@[simp]

theorem PadicInt.coe_unitsToZModPow_apply {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (u : ℤ_[p]ˣ) : ↑((unitsToZModPow n) u) = (toZModPow n) ↑u

theorem PadicInt.pow_appr_eq_pow_appr {p : ℕ} [hp : Fact (Nat.Prime p)] {M : Type u_1} [Monoid M] {g : M} {n : ℕ} (x : ℤ_[p]) {m : ℕ} (hg : g ^ p ^ m = 1) (hmn : m ≤ n) : g ^ x.appr n = g ^ x.appr m

Raising an element killed by p ^ m to the exponent x.appr n gives the same value for every truncation level n ≥ m. This is what makes the p-adic power well defined.