PadicInt.zmod_cast_comp_toZModPow
theorem PadicInt.zmod_cast_comp_toZModPow :
∀ {p : ℕ} [hp_prime : Fact p.Prime] (m n : ℕ) (h : m ≤ n),
(ZMod.castHom ⋯ (ZMod (p ^ m))).comp (PadicInt.toZModPow n) = PadicInt.toZModPow m
This theorem states that for any natural number `p` that is prime and any two natural numbers `m` and `n` such that `m` is less than or equal to `n`, the composition of the ring homomorphism from `ZMod n` to `ZMod (p ^ m)` with the ring homomorphism from `ℤ_[p]` to `ZMod (p^n)` is equal to the ring homomorphism from `ℤ_[p]` to `ZMod (p^m)`. In other words, it ensures the compatibility of reducing a p-adic integer modulo `p^n` before or after reducing modulo `p^m` for `m ≤ n`.
More concisely: For any prime number p and natural numbers m and n with m <= n, the ring homomorphism from Z_[p] to ZMod (p^m) commutes with the ring homomorphism from ZMod n to ZMod (p^m).
|
PadicInt.zmod_congr_of_sub_mem_span
theorem PadicInt.zmod_congr_of_sub_mem_span :
∀ {p : ℕ} [hp_prime : Fact p.Prime] (n : ℕ) (x : ℤ_[p]) (a b : ℕ),
x - ↑a ∈ Ideal.span {↑p ^ n} → x - ↑b ∈ Ideal.span {↑p ^ n} → ↑a = ↑b
The theorem `PadicInt.zmod_congr_of_sub_mem_span` states that for any natural number `p` which is a prime number, any natural number `n`, any p-adic integer `x`, and any two natural numbers `a` and `b`, if the difference of `x` and the integer representation of `a` belongs to the ideal generated by the set containing `p` raised to the power `n`, and similarly, the difference of `x` and the integer representation of `b` also belongs to the same ideal, then `a` and `b` are equal. In other words, if the differences between a p-adic integer and two natural numbers fall into the same ideal generated by a prime number to a certain power, these two numbers must be the same.
More concisely: If two natural numbers `a` and `b` differ by an integer multiple of `p^n`, where `p` is a prime number and `n` is a natural number, then `a` and `b` are equal. (In the context of p-adic integers, the difference of `x` and the integer representation of `a` and `b` belong to the ideal generated by `p` raised to the power `n`.)
|
PadicInt.toZMod_spec
theorem PadicInt.toZMod_spec :
∀ {p : ℕ} [hp_prime : Fact p.Prime] (x : ℤ_[p]), x - (PadicInt.toZMod x).cast ∈ LocalRing.maximalIdeal ℤ_[p] := by
sorry
This theorem states that for any prime number `p` and any integer `x` in the ring of `p`-adic integers (`ℤ_[p]`), the difference `x - (PadicInt.toZMod x).cast` is contained in the maximal ideal of the `p`-adic integers ring.
Here, `PadicInt.toZMod x` is a ring homomorphism from `ℤ_[p]` to `ZMod p`, which maps `x` to its representative modulo `p`. The `.cast` operation then coerces this representative back into the ring of `p`-adic integers.
The theorem tells us about the relationship between integer values in the `p`-adic integers ring, their modulo `p` representations, and the maximal ideal of the `p`-adic integers ring, which consists of non-unit elements.
More concisely: For any prime number `p` and `x` in the `p`-adic integers ring `ℤ_[p]`, the difference between `x` and the reduction of `x` modulo `p` lies in the maximal ideal of `ℤ_[p]`.
|
PadicInt.appr_spec
theorem PadicInt.appr_spec :
∀ {p : ℕ} [hp_prime : Fact p.Prime] (n : ℕ) (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
The theorem `PadicInt.appr_spec` states that for every natural number `p` which is a prime number, for every natural number `n`, and for every p-adic integer `x`, the difference between `x` and the approximation of `x` at `n` belongs to the ideal generated by the set containing `p` to the power of `n`. In other words, if we subtract the `n`th approximation of a p-adic integer `x` from `x` itself, the result will be a member of the ideal whose generators are the powers of the prime `p` up to the `n`th power.
More concisely: For every prime number p, natural number n, and p-adic integer x, the difference between x and its n-th approximation belongs to the ideal generated by {p^i | i <= n}.
|
PadicInt.lift_unique
theorem PadicInt.lift_unique :
∀ {p : ℕ} [hp_prime : Fact p.Prime] {R : Type u_1} [inst : NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)}
(f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]),
(∀ (n : ℕ), (PadicInt.toZModPow n).comp g = f n) → PadicInt.lift f_compat = g
This theorem is part of the universal property of the p-adic integers (`ℤ_[p]`) viewed as a projective limit. Given a prime number `p`, a non-associative semiring `R`, and a sequence of ring homomorphisms `f` from `R` to Z modulo `p` to the power of `k` (`ZMod (p ^ k)`) that are compatible in the sense that for every two natural numbers `k1` and `k2` with `k1` less than or equal to `k2`, the composition of `ZMod.castHom` and `f k2` is equal to `f k1`. If we also have a ring homomorphism `g` from `R` to `ℤ_[p]` such that for every natural number `n`, the composition of `PadicInt.toZModPow n` and `g` is equal to `f n`, then the PadicInt.lift of `f_compat` (another ring homomorphism) is equal to `g`. This theorem essentially provides a uniqueness aspect for the `PadicInt.lift` function under these conditions.
More concisely: Given a prime number `p`, a non-associative semiring `R`, a sequence `f` of compatible ring homomorphisms from `R` to `ZMod (p ^ k)`, and a ring homomorphism `g` from `R` to `ℤ_[p]` such that `PadicInt.toZModPow n . g = f n` for all natural numbers `n`, the `PadicInt.lift` of `f` is equal to `g`.
|
PadicInt.lift_spec
theorem PadicInt.lift_spec :
∀ {p : ℕ} [hp_prime : Fact p.Prime] {R : Type u_1} [inst : NonAssocSemiring R] {f : (k : ℕ) → R →+* ZMod (p ^ k)}
(f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (n : ℕ),
(PadicInt.toZModPow n).comp (PadicInt.lift f_compat) = f n
This theorem, `PadicInt.lift_spec`, is a part of the universal property of the ring of p-adic integers `ℤ_[p]` as a projective limit. It states that for any natural number `p` that is prime, any type `R` that forms a non-associative semiring, and any sequence `f` of ring homomorphisms from `R` to `ZMod (p ^ k)` for each natural number `k`, that are compatible in the sense defined by `f_compat`, the composition of `PadicInt.toZModPow n` and `PadicInt.lift f_compat` is equal to `f n` for each natural number `n`. This means that the lifting operation used in the construction of the projective limit of the system of `ZMod (p ^ k)`s over `ℤ_[p]` behaves correctly with respect to the maps `f` that define the system.
More concisely: For any prime number p, any non-associative semiring R and compatible sequence of ring homomorphisms f from R to ZMod (p^k), the composition of PadicInt.toZModPow and PadicInt.lift(f) equals f for all natural numbers n.
|