Documentation

Mathlib.NumberTheory.Padics.RingHoms

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.

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$.

Implementation notes #

The ring hom constructions go through an auxiliary constructor PadicInt.toZModHom, which removes some boilerplate code.

Ring homomorphisms to ZMod p and ZMod (p ^ n) #

def PadicInt.modPart (p : ) (r : ) :

modPart p r is an integer that satisfies ‖(r - modPart p r : ℚ_[p])‖ < 1 when ‖(r : ℚ_[p])‖ ≤ 1, see PadicInt.norm_sub_modPart. It is the unique non-negative integer that is < p with this property.

(Note that this definition assumes r : ℚ. See PadicInt.zmodRepr for a version that takes values in and works for arbitrary x : ℤ_[p].)

Equations
Instances For
    theorem PadicInt.modPart_lt_p {p : } [hp_prime : Fact p.Prime] (r : ) :
    theorem PadicInt.modPart_nonneg {p : } [hp_prime : Fact p.Prime] (r : ) :
    theorem PadicInt.isUnit_den {p : } [hp_prime : Fact p.Prime] (r : ) (h : r 1) :
    IsUnit r.den
    theorem PadicInt.norm_sub_modPart_aux {p : } [hp_prime : Fact p.Prime] (r : ) (h : r 1) :
    p r.num - r.num * r.den.gcdA p % p * r.den
    theorem PadicInt.norm_sub_modPart {p : } [hp_prime : Fact p.Prime] (r : ) (h : r 1) :
    r, h - (PadicInt.modPart p r) < 1
    theorem PadicInt.exists_mem_range_of_norm_rat_le_one {p : } [hp_prime : Fact p.Prime] (r : ) (h : r 1) :
    ∃ (n : ), 0 n n < p r, h - n < 1
    theorem PadicInt.zmod_congr_of_sub_mem_span_aux {p : } [hp_prime : Fact p.Prime] (n : ) (x : ℤ_[p]) (a : ) (b : ) (ha : x - a Ideal.span {p ^ n}) (hb : x - b Ideal.span {p ^ n}) :
    a = b
    theorem PadicInt.zmod_congr_of_sub_mem_span {p : } [hp_prime : Fact p.Prime] (n : ) (x : ℤ_[p]) (a : ) (b : ) (ha : x - a Ideal.span {p ^ n}) (hb : x - b Ideal.span {p ^ n}) :
    a = b
    theorem PadicInt.zmod_congr_of_sub_mem_max_ideal {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) (m : ) (n : ) (hm : x - m LocalRing.maximalIdeal ℤ_[p]) (hn : x - n LocalRing.maximalIdeal ℤ_[p]) :
    m = n
    theorem PadicInt.exists_mem_range {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
    n < p, x - n LocalRing.maximalIdeal ℤ_[p]
    def PadicInt.zmodRepr {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :

    zmod_repr x is the unique natural number smaller than p satisfying ‖(x - zmod_repr x : ℤ_[p])‖ < 1.

    Equations
    Instances For
      theorem PadicInt.zmodRepr_spec {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
      x.zmodRepr < p x - x.zmodRepr LocalRing.maximalIdeal ℤ_[p]
      theorem PadicInt.zmodRepr_lt_p {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
      x.zmodRepr < p
      theorem PadicInt.sub_zmodRepr_mem {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
      def PadicInt.toZModHom {p : } [hp_prime : Fact p.Prime] (v : ) (f : ℤ_[p]) (f_spec : ∀ (x : ℤ_[p]), x - (f x) Ideal.span {v}) (f_congr : ∀ (x : ℤ_[p]) (a b : ), x - a Ideal.span {v}x - b Ideal.span {v}a = b) :

      toZModHom is an auxiliary constructor for creating ring homs from ℤ_[p] to ZMod v.

      Equations
      • PadicInt.toZModHom v f f_spec f_congr = { toFun := fun (x : ℤ_[p]) => (f x), map_one' := , map_mul' := , map_zero' := , map_add' := }
      Instances For
        def PadicInt.toZMod {p : } [hp_prime : Fact p.Prime] :

        toZMod is a ring hom from ℤ_[p] to ZMod p, with the equality toZMod x = (zmodRepr x : ZMod p).

        Equations
        Instances For
          theorem PadicInt.toZMod_spec {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
          x - (PadicInt.toZMod x).cast LocalRing.maximalIdeal ℤ_[p]

          z - (toZMod z : ℤ_[p]) is contained in the maximal ideal of ℤ_[p], for every z : ℤ_[p].

          The coercion from ZMod p to ℤ_[p] is ZMod.cast, which coerces ZMod p into arbitrary 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.

          theorem PadicInt.ker_toZMod {p : } [hp_prime : Fact p.Prime] :
          noncomputable def PadicInt.appr {p : } [hp_prime : Fact p.Prime] :
          ℤ_[p]

          appr n x gives a value v : ℕ such that x and ↑v : ℤ_p are congruent mod p^n. See appr_spec.

          Equations
          • One or more equations did not get rendered due to their size.
          • x.appr 0 = 0
          Instances For
            theorem PadicInt.appr_lt {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) (n : ) :
            x.appr n < p ^ n
            theorem PadicInt.appr_mono {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) :
            Monotone x.appr
            theorem PadicInt.dvd_appr_sub_appr {p : } [hp_prime : Fact p.Prime] (x : ℤ_[p]) (m : ) (n : ) (h : m n) :
            p ^ m x.appr n - x.appr m
            theorem PadicInt.appr_spec {p : } [hp_prime : Fact p.Prime] (n : ) (x : ℤ_[p]) :
            x - (x.appr n) Ideal.span {p ^ n}
            def PadicInt.toZModPow {p : } [hp_prime : Fact p.Prime] (n : ) :

            A ring hom from ℤ_[p] to ZMod (p^n), with underlying function PadicInt.appr n.

            Equations
            Instances For
              theorem PadicInt.ker_toZModPow {p : } [hp_prime : Fact p.Prime] (n : ) :
              theorem PadicInt.zmod_cast_comp_toZModPow {p : } [hp_prime : Fact p.Prime] (m : ) (n : ) (h : m n) :
              @[simp]
              theorem PadicInt.cast_toZModPow {p : } [hp_prime : Fact p.Prime] (m : ) (n : ) (h : m n) (x : ℤ_[p]) :
              theorem PadicInt.denseRange_natCast {p : } [hp_prime : Fact p.Prime] :
              DenseRange Nat.cast
              @[deprecated PadicInt.denseRange_natCast]
              theorem PadicInt.denseRange_nat_cast {p : } [hp_prime : Fact p.Prime] :
              DenseRange Nat.cast

              Alias of PadicInt.denseRange_natCast.

              theorem PadicInt.denseRange_intCast {p : } [hp_prime : Fact p.Prime] :
              DenseRange Int.cast
              @[deprecated PadicInt.denseRange_intCast]
              theorem PadicInt.denseRange_int_cast {p : } [hp_prime : Fact p.Prime] :
              DenseRange Int.cast

              Alias of PadicInt.denseRange_intCast.

              Universal property as projective limit #

              def PadicInt.nthHom {p : } {R : Type u_1} [NonAssocSemiring R] (f : (k : ) → R →+* ZMod (p ^ k)) (r : R) :

              Given a family of ring homs f : Π n : ℕ, R →+* ZMod (p ^ n), nthHom 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)).

              Equations
              Instances For
                @[simp]
                theorem PadicInt.nthHom_zero {p : } {R : Type u_1} [NonAssocSemiring R] (f : (k : ) → R →+* ZMod (p ^ k)) :
                theorem PadicInt.pow_dvd_nthHom_sub {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (i : ) (j : ) (h : i j) :
                theorem PadicInt.isCauSeq_nthHom {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) :
                IsCauSeq (padicNorm p) fun (n : ) => (PadicInt.nthHom f r n)
                def PadicInt.nthHomSeq {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) :

                nthHomSeq f_compat r bundles PadicInt.nthHom 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
                Instances For
                  theorem PadicInt.nthHomSeq_one {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) :
                  PadicInt.nthHomSeq f_compat 1 1
                  theorem PadicInt.nthHomSeq_add {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (s : R) :
                  PadicInt.nthHomSeq f_compat (r + s) PadicInt.nthHomSeq f_compat r + PadicInt.nthHomSeq f_compat s
                  theorem PadicInt.nthHomSeq_mul {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (s : R) :
                  PadicInt.nthHomSeq f_compat (r * s) PadicInt.nthHomSeq f_compat r * PadicInt.nthHomSeq f_compat s
                  def PadicInt.limNthHom {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) :

                  limNthHom 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 PadicInt.lift.

                  Equations
                  Instances For
                    theorem PadicInt.limNthHom_spec {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (ε : ) :
                    0 < ε∃ (N : ), nN, PadicInt.limNthHom f_compat r - (PadicInt.nthHom f r n) < ε
                    theorem PadicInt.limNthHom_zero {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) :
                    PadicInt.limNthHom f_compat 0 = 0
                    theorem PadicInt.limNthHom_one {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) :
                    PadicInt.limNthHom f_compat 1 = 1
                    theorem PadicInt.limNthHom_add {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (s : R) :
                    PadicInt.limNthHom f_compat (r + s) = PadicInt.limNthHom f_compat r + PadicInt.limNthHom f_compat s
                    theorem PadicInt.limNthHom_mul {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (s : R) :
                    PadicInt.limNthHom f_compat (r * s) = PadicInt.limNthHom f_compat r * PadicInt.limNthHom f_compat s
                    def PadicInt.lift {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) :

                    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 = PadicInt.limNthHom f_compat r.

                    Equations
                    Instances For
                      theorem PadicInt.lift_sub_val_mem_span {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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) (r : R) (n : ) :
                      (PadicInt.lift f_compat) r - ((f n) r).val Ideal.span {p ^ n}
                      theorem PadicInt.lift_spec {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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

                      One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_unique.

                      theorem PadicInt.lift_unique {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [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]) (hg : ∀ (n : ), (PadicInt.toZModPow n).comp g = f n) :
                      PadicInt.lift f_compat = g

                      One part of the universal property of ℤ_[p] as a projective limit. See also PadicInt.lift_spec.

                      @[simp]
                      theorem PadicInt.lift_self {p : } [hp_prime : Fact p.Prime] (z : ℤ_[p]) :
                      (PadicInt.lift ) z = z
                      theorem PadicInt.ext_of_toZModPow {p : } [hp_prime : Fact p.Prime] {x : ℤ_[p]} {y : ℤ_[p]} :
                      (∀ (n : ), (PadicInt.toZModPow n) x = (PadicInt.toZModPow n) y) x = y
                      theorem PadicInt.toZModPow_eq_iff_ext {p : } [hp_prime : Fact p.Prime] {R : Type u_1} [NonAssocSemiring R] {g : R →+* ℤ_[p]} {g' : R →+* ℤ_[p]} :
                      (∀ (n : ), (PadicInt.toZModPow n).comp g = (PadicInt.toZModPow n).comp g') g = g'