Documentation

Mathlib.NumberTheory.Padics.PadicNumbers

p-adic numbers #

This file defines the p-adic numbers (rationals) ℚ_[p] as the completion of with respect to the p-adic norm. We show that the p-adic norm on extends to ℚ_[p], that is embedded in ℚ_[p], and that ℚ_[p] is Cauchy complete.

Important definitions #

Notation #

We introduce the notation ℚ_[p] for the p-adic numbers.

Implementation notes #

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [Fact p.Prime] as a type class argument.

We use the same concrete Cauchy sequence construction that is used to construct . ℚ_[p] inherits a field structure from this construction. The extension of the norm on to ℚ_[p] is not analogous to extending the absolute value to and hence the proof that ℚ_[p] is complete is different from the proof that ℝ is complete.

A small special-purpose simplification tactic, padic_index_simp, is used to manipulate sequence indices in the proof that the norm extends.

padicNormE is the rational-valued p-adic norm on ℚ_[p]. To instantiate ℚ_[p] as a normed field, we must cast this into an -valued norm. The -valued norm, using notation ‖ ‖ from normed spaces, is the canonical representation of this norm.

simp prefers padicNorm to padicNormE when possible. Since padicNormE and ‖ ‖ have different types, simp does not rewrite one to the other.

Coercions from to ℚ_[p] are set up to work with the norm_cast tactic.

References #

Tags #

p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion

@[reducible, inline]
abbrev PadicSeq (p : ) :

The type of Cauchy sequences of rationals with respect to the p-adic norm.

Equations
Instances For
    theorem PadicSeq.stationary {p : } [Fact (Nat.Prime p)] {f : CauSeq (padicNorm p)} (hf : ¬f 0) :
    ∃ (N : ), ∀ (m n : ), N mN npadicNorm p (f n) = padicNorm p (f m)

    The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually constant.

    def PadicSeq.stationaryPoint {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) :

    For all n ≥ stationaryPoint f hf, the p-adic norm of f n is the same.

    Equations
    Instances For
      theorem PadicSeq.stationaryPoint_spec {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) {m : } {n : } :
      def PadicSeq.norm {p : } [Fact (Nat.Prime p)] (f : PadicSeq p) :

      Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm to sequences.

      Equations
      Instances For
        theorem PadicSeq.norm_zero_iff {p : } [Fact (Nat.Prime p)] (f : PadicSeq p) :
        f.norm = 0 f 0
        theorem PadicSeq.equiv_zero_of_val_eq_of_equiv_zero {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (h : ∀ (k : ), padicNorm p (f k) = padicNorm p (g k)) (hf : f 0) :
        g 0
        theorem PadicSeq.norm_nonzero_of_not_equiv_zero {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) :
        f.norm 0
        theorem PadicSeq.norm_eq_norm_app_of_nonzero {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) :
        ∃ (k : ), f.norm = padicNorm p k k 0
        theorem PadicSeq.not_limZero_const_of_nonzero {p : } [Fact (Nat.Prime p)] {q : } (hq : q 0) :
        ¬(CauSeq.const (padicNorm p) q).LimZero
        theorem PadicSeq.norm_nonneg {p : } [Fact (Nat.Prime p)] (f : PadicSeq p) :
        0 f.norm
        theorem PadicSeq.lift_index_left_left {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) (v2 : ) (v3 : ) :

        An auxiliary lemma for manipulating sequence indices.

        theorem PadicSeq.lift_index_left {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) (v1 : ) (v3 : ) :

        An auxiliary lemma for manipulating sequence indices.

        theorem PadicSeq.lift_index_right {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) (v1 : ) (v2 : ) :

        An auxiliary lemma for manipulating sequence indices.

        Valuation on PadicSeq #

        def PadicSeq.valuation {p : } [Fact (Nat.Prime p)] (f : PadicSeq p) :

        The p-adic valuation on lifts to PadicSeq p. Valuation f is defined to be the valuation of the (-valued) stationary point of f.

        Equations
        Instances For
          theorem PadicSeq.norm_eq_pow_val {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} (hf : ¬f 0) :
          f.norm = p ^ (-f.valuation)
          theorem PadicSeq.val_eq_iff_norm_eq {p : } [Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (hf : ¬f 0) (hg : ¬g 0) :
          f.valuation = g.valuation f.norm = g.norm
          theorem PadicSeq.norm_mul {p : } [hp : Fact (Nat.Prime p)] (f : PadicSeq p) (g : PadicSeq p) :
          (f * g).norm = f.norm * g.norm
          theorem PadicSeq.norm_values_discrete {p : } [hp : Fact (Nat.Prime p)] (a : PadicSeq p) (ha : ¬a 0) :
          ∃ (z : ), a.norm = p ^ (-z)
          theorem PadicSeq.norm_equiv {p : } [hp : Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (hfg : f g) :
          f.norm = g.norm
          theorem PadicSeq.norm_nonarchimedean {p : } [hp : Fact (Nat.Prime p)] (f : PadicSeq p) (g : PadicSeq p) :
          (f + g).norm max f.norm g.norm
          theorem PadicSeq.norm_eq {p : } [hp : Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (h : ∀ (k : ), padicNorm p (f k) = padicNorm p (g k)) :
          f.norm = g.norm
          theorem PadicSeq.norm_neg {p : } [hp : Fact (Nat.Prime p)] (a : PadicSeq p) :
          (-a).norm = a.norm
          theorem PadicSeq.norm_eq_of_add_equiv_zero {p : } [hp : Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (h : f + g 0) :
          f.norm = g.norm
          theorem PadicSeq.add_eq_max_of_ne {p : } [hp : Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} (hfgne : f.norm g.norm) :
          (f + g).norm = max f.norm g.norm
          def Padic (p : ) [Fact (Nat.Prime p)] :

          The p-adic numbers ℚ_[p] are the Cauchy completion of with respect to the p-adic norm.

          Equations
          Instances For

            notation for p-padic rationals

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance Padic.field {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.field = CauSeq.Completion.Cauchy.field
              Equations
              • Padic.instInhabited = { default := 0 }
              Equations
              • Padic.instCommRing = CauSeq.Completion.Cauchy.commRing
              instance Padic.instRing {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instRing = CauSeq.Completion.Cauchy.ring
              instance Padic.instZero {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instZero = inferInstance
              instance Padic.instOne {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instOne = inferInstance
              instance Padic.instAdd {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instAdd = inferInstance
              instance Padic.instMul {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instMul = inferInstance
              instance Padic.instSub {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instSub = inferInstance
              instance Padic.instNeg {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instNeg = inferInstance
              instance Padic.instDiv {p : } [Fact (Nat.Prime p)] :
              Equations
              • Padic.instDiv = inferInstance
              Equations
              • Padic.instAddCommGroup = inferInstance
              def Padic.mk {p : } [Fact (Nat.Prime p)] :

              Builds the equivalence class of a Cauchy sequence of rationals.

              Equations
              • Padic.mk = Quotient.mk'
              Instances For
                theorem Padic.zero_def (p : ) [Fact (Nat.Prime p)] :
                0 = 0
                theorem Padic.mk_eq (p : ) [Fact (Nat.Prime p)] {f : PadicSeq p} {g : PadicSeq p} :
                theorem Padic.coe_inj (p : ) [Fact (Nat.Prime p)] {q : } {r : } :
                q = r q = r
                Equations
                • =
                theorem Padic.coe_add (p : ) [Fact (Nat.Prime p)] {x : } {y : } :
                (x + y) = x + y
                theorem Padic.coe_neg (p : ) [Fact (Nat.Prime p)] {x : } :
                (-x) = -x
                theorem Padic.coe_mul (p : ) [Fact (Nat.Prime p)] {x : } {y : } :
                (x * y) = x * y
                theorem Padic.coe_sub (p : ) [Fact (Nat.Prime p)] {x : } {y : } :
                (x - y) = x - y
                theorem Padic.coe_div (p : ) [Fact (Nat.Prime p)] {x : } {y : } :
                (x / y) = x / y
                theorem Padic.coe_one (p : ) [Fact (Nat.Prime p)] :
                1 = 1
                theorem Padic.coe_zero (p : ) [Fact (Nat.Prime p)] :
                0 = 0

                The rational-valued p-adic norm on ℚ_[p] is lifted from the norm on Cauchy sequences. The canonical form of this function is the normed space instance, with notation ‖ ‖.

                Equations
                • padicNormE = { toFun := Quotient.lift PadicSeq.norm , map_mul' := , nonneg' := , eq_zero' := , add_le' := }
                Instances For
                  theorem padicNormE.defn {p : } [Fact (Nat.Prime p)] (f : PadicSeq p) {ε : } (hε : 0 < ε) :
                  ∃ (N : ), iN, padicNormE (Padic.mk f - (f i)) < ε
                  theorem padicNormE.nonarchimedean' {p : } [Fact (Nat.Prime p)] (q : ℚ_[p]) (r : ℚ_[p]) :
                  padicNormE (q + r) max (padicNormE q) (padicNormE r)

                  Theorems about padicNormE are named with a ' so the names do not conflict with the equivalent theorems about norm (‖ ‖).

                  theorem padicNormE.add_eq_max_of_ne' {p : } [Fact (Nat.Prime p)] {q : ℚ_[p]} {r : ℚ_[p]} :
                  padicNormE q padicNormE rpadicNormE (q + r) = max (padicNormE q) (padicNormE r)

                  Theorems about padicNormE are named with a ' so the names do not conflict with the equivalent theorems about norm (‖ ‖).

                  @[simp]
                  theorem padicNormE.eq_padic_norm' {p : } [Fact (Nat.Prime p)] (q : ) :
                  padicNormE q = padicNorm p q
                  theorem padicNormE.image' {p : } [Fact (Nat.Prime p)] {q : ℚ_[p]} :
                  q 0∃ (n : ), padicNormE q = p ^ (-n)
                  theorem Padic.rat_dense' {p : } [Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : } (hε : 0 < ε) :
                  ∃ (r : ), padicNormE (q - r) < ε
                  def Padic.limSeq {p : } [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] padicNormE) :

                  limSeq f, for f a Cauchy sequence of p-adic numbers, is a sequence of rationals with the same limit point as f.

                  Equations
                  Instances For
                    theorem Padic.exi_rat_seq_conv {p : } [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] padicNormE) {ε : } (hε : 0 < ε) :
                    ∃ (N : ), iN, padicNormE (f i - (Padic.limSeq f i)) < ε
                    theorem Padic.complete' {p : } [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] padicNormE) :
                    ∃ (q : ℚ_[p]), ε > 0, ∃ (N : ), iN, padicNormE (q - f i) < ε
                    theorem Padic.complete'' {p : } [Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] padicNormE) :
                    ∃ (q : ℚ_[p]), ε > 0, ∃ (N : ), iN, padicNormE (f i - q) < ε
                    instance Padic.instDist (p : ) [Fact (Nat.Prime p)] :
                    Equations
                    instance Padic.instNorm (p : ) [Fact (Nat.Prime p)] :
                    Equations
                    Equations
                    instance Padic.isAbsoluteValue (p : ) [Fact (Nat.Prime p)] :
                    Equations
                    • =
                    theorem Padic.rat_dense (p : ) [Fact (Nat.Prime p)] (q : ℚ_[p]) {ε : } (hε : 0 < ε) :
                    ∃ (r : ), q - r < ε
                    @[simp]
                    theorem padicNormE.mul {p : } [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) (r : ℚ_[p]) :
                    theorem padicNormE.is_norm {p : } [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) :
                    (padicNormE q) = q
                    theorem padicNormE.nonarchimedean {p : } [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) (r : ℚ_[p]) :
                    theorem padicNormE.add_eq_max_of_ne {p : } [hp : Fact (Nat.Prime p)] {q : ℚ_[p]} {r : ℚ_[p]} (h : q r) :
                    @[simp]
                    theorem padicNormE.eq_padicNorm {p : } [hp : Fact (Nat.Prime p)] (q : ) :
                    q = (padicNorm p q)
                    @[simp]
                    theorem padicNormE.norm_p {p : } [hp : Fact (Nat.Prime p)] :
                    p = (p)⁻¹
                    theorem padicNormE.norm_p_lt_one {p : } [hp : Fact (Nat.Prime p)] :
                    p < 1
                    @[simp]
                    theorem padicNormE.norm_p_zpow {p : } [hp : Fact (Nat.Prime p)] (n : ) :
                    p ^ n = p ^ (-n)
                    @[simp]
                    theorem padicNormE.norm_p_pow {p : } [hp : Fact (Nat.Prime p)] (n : ) :
                    p ^ n = p ^ (-n)
                    Equations
                    theorem padicNormE.image {p : } [hp : Fact (Nat.Prime p)] {q : ℚ_[p]} :
                    q 0∃ (n : ), q = (p ^ (-n))
                    theorem padicNormE.is_rat {p : } [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) :
                    ∃ (q' : ), q = q'
                    def padicNormE.ratNorm {p : } [hp : Fact (Nat.Prime p)] (q : ℚ_[p]) :

                    ratNorm q, for a p-adic number q is the p-adic norm of q, as rational number.

                    The lemma padicNormE.eq_ratNorm asserts ‖q‖ = ratNorm q.

                    Equations
                    Instances For
                      theorem padicNormE.norm_rat_le_one {p : } [hp : Fact (Nat.Prime p)] {q : } :
                      ¬p q.denq 1
                      theorem padicNormE.norm_int_le_one {p : } [hp : Fact (Nat.Prime p)] (z : ) :
                      z 1
                      theorem padicNormE.norm_int_lt_one_iff_dvd {p : } [hp : Fact (Nat.Prime p)] (k : ) :
                      k < 1 p k
                      theorem padicNormE.norm_int_le_pow_iff_dvd {p : } [hp : Fact (Nat.Prime p)] (k : ) (n : ) :
                      k p ^ (-n) p ^ n k
                      theorem padicNormE.eq_of_norm_add_lt_right {p : } [hp : Fact (Nat.Prime p)] {z1 : ℚ_[p]} {z2 : ℚ_[p]} (h : z1 + z2 < z2) :
                      theorem padicNormE.eq_of_norm_add_lt_left {p : } [hp : Fact (Nat.Prime p)] {z1 : ℚ_[p]} {z2 : ℚ_[p]} (h : z1 + z2 < z1) :
                      instance Padic.complete {p : } [hp : Fact (Nat.Prime p)] :
                      Equations
                      • =
                      theorem Padic.padicNormE_lim_le {p : } [hp : Fact (Nat.Prime p)] {f : CauSeq ℚ_[p] norm} {a : } (ha : 0 < a) (hf : ∀ (i : ), f i a) :
                      f.lim a
                      Equations
                      • =

                      Valuation on ℚ_[p] #

                      def Padic.valuation {p : } [hp : Fact (Nat.Prime p)] :
                      ℚ_[p]

                      Padic.valuation lifts the p-adic valuation on rationals to ℚ_[p].

                      Equations
                      Instances For
                        @[simp]
                        theorem Padic.valuation_zero {p : } [hp : Fact (Nat.Prime p)] :
                        @[simp]
                        theorem Padic.valuation_one {p : } [hp : Fact (Nat.Prime p)] :
                        theorem Padic.norm_eq_pow_val {p : } [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} :
                        x 0x = p ^ (-x.valuation)
                        @[simp]
                        theorem Padic.valuation_p {p : } [hp : Fact (Nat.Prime p)] :
                        (p).valuation = 1
                        theorem Padic.valuation_map_add {p : } [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} {y : ℚ_[p]} (hxy : x + y 0) :
                        min x.valuation y.valuation (x + y).valuation
                        @[simp]
                        theorem Padic.valuation_map_mul {p : } [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} {y : ℚ_[p]} (hx : x 0) (hy : y 0) :
                        (x * y).valuation = x.valuation + y.valuation

                        The additive p-adic valuation on ℚ_[p], with values in WithTop.

                        Equations
                        • x.addValuationDef = if x = 0 then else x.valuation
                        Instances For
                          theorem Padic.AddValuation.map_mul {p : } [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (y : ℚ_[p]) :
                          (x * y).addValuationDef = x.addValuationDef + y.addValuationDef
                          theorem Padic.AddValuation.map_add {p : } [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (y : ℚ_[p]) :
                          min x.addValuationDef y.addValuationDef (x + y).addValuationDef

                          The additive p-adic valuation on ℚ_[p], as an addValuation.

                          Equations
                          Instances For
                            @[simp]
                            theorem Padic.addValuation.apply {p : } [hp : Fact (Nat.Prime p)] {x : ℚ_[p]} (hx : x 0) :
                            Padic.addValuation x = x.valuation

                            Various characterizations of open unit balls #

                            theorem Padic.norm_le_pow_iff_norm_lt_pow_add_one {p : } [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ) :
                            x p ^ n x < p ^ (n + 1)
                            theorem Padic.norm_lt_pow_iff_norm_le_pow_sub_one {p : } [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) (n : ) :
                            x < p ^ n x p ^ (n - 1)
                            theorem Padic.norm_le_one_iff_val_nonneg {p : } [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) :
                            x 1 0 x.valuation