Documentation

Mathlib.NumberTheory.Padics.PadicIntegers

p-adic integers #

This file defines the p-adic integers ℤ_[p] as the subtype of ℚ_[p] with norm ≤ 1. We show that ℤ_[p]

The relation between ℤ_[p] and ZMod p is established in another file.

Important definitions #

Notation #

We introduce the notation ℤ_[p] for the p-adic integers.

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.

Coercions into ℤ_[p] are set up to work with the norm_cast tactic.

References #

Tags #

p-adic, p adic, padic, p-adic integer

def PadicInt (p : ) [Fact (Nat.Prime p)] :

The p-adic integers ℤ_[p] are the p-adic numbers with norm ≤ 1.

Equations
Instances For

    The ring of p-adic integers.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Ring structure and coercion to ℚ_[p] #

      Equations
      • PadicInt.instCoePadic = { coe := Subtype.val }
      theorem PadicInt.ext {p : } [Fact (Nat.Prime p)] {x : ℤ_[p]} {y : ℤ_[p]} :
      x = yx = y

      The p-adic integers as a subring of ℚ_[p].

      Equations
      Instances For
        instance PadicInt.instAdd {p : } [Fact (Nat.Prime p)] :

        Addition on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instAdd = inferInstance
        instance PadicInt.instMul {p : } [Fact (Nat.Prime p)] :

        Multiplication on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instMul = inferInstance
        instance PadicInt.instNeg {p : } [Fact (Nat.Prime p)] :

        Negation on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instNeg = inferInstance
        instance PadicInt.instSub {p : } [Fact (Nat.Prime p)] :

        Subtraction on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instSub = inferInstance

        Zero on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instZero = inferInstance
        Equations
        • PadicInt.instInhabited = { default := 0 }
        instance PadicInt.instOne {p : } [Fact (Nat.Prime p)] :

        One on ℤ_[p] is inherited from ℚ_[p].

        Equations
        • PadicInt.instOne = { one := 1, }
        @[simp]
        theorem PadicInt.mk_zero {p : } [Fact (Nat.Prime p)] {h : 0 1} :
        0, h = 0
        @[simp]
        theorem PadicInt.coe_add {p : } [Fact (Nat.Prime p)] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
        (z1 + z2) = z1 + z2
        @[simp]
        theorem PadicInt.coe_mul {p : } [Fact (Nat.Prime p)] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
        (z1 * z2) = z1 * z2
        @[simp]
        theorem PadicInt.coe_neg {p : } [Fact (Nat.Prime p)] (z1 : ℤ_[p]) :
        (-z1) = -z1
        @[simp]
        theorem PadicInt.coe_sub {p : } [Fact (Nat.Prime p)] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
        (z1 - z2) = z1 - z2
        @[simp]
        theorem PadicInt.coe_one {p : } [Fact (Nat.Prime p)] :
        1 = 1
        @[simp]
        theorem PadicInt.coe_zero {p : } [Fact (Nat.Prime p)] :
        0 = 0
        theorem PadicInt.coe_eq_zero {p : } [Fact (Nat.Prime p)] (z : ℤ_[p]) :
        z = 0 z = 0
        theorem PadicInt.coe_ne_zero {p : } [Fact (Nat.Prime p)] (z : ℤ_[p]) :
        z 0 z 0
        Equations
        • PadicInt.instAddCommGroup = inferInstance
        Equations
        • PadicInt.instCommRing = inferInstance
        @[simp]
        theorem PadicInt.coe_natCast {p : } [Fact (Nat.Prime p)] (n : ) :
        n = n
        @[deprecated PadicInt.coe_natCast]
        theorem PadicInt.coe_nat_cast {p : } [Fact (Nat.Prime p)] (n : ) :
        n = n

        Alias of PadicInt.coe_natCast.

        @[simp]
        theorem PadicInt.coe_intCast {p : } [Fact (Nat.Prime p)] (z : ) :
        z = z
        @[deprecated PadicInt.coe_intCast]
        theorem PadicInt.coe_int_cast {p : } [Fact (Nat.Prime p)] (z : ) :
        z = z

        Alias of PadicInt.coe_intCast.

        The coercion from ℤ_[p] to ℚ_[p] as a ring homomorphism.

        Equations
        Instances For
          @[simp]
          theorem PadicInt.coe_pow {p : } [Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ) :
          (x ^ n) = x ^ n
          theorem PadicInt.mk_coe {p : } [Fact (Nat.Prime p)] (k : ℤ_[p]) :
          k, = k
          def PadicInt.inv {p : } [Fact (Nat.Prime p)] :

          The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the inverse is defined to be 0.

          Equations
          • x.inv = match x with | k, property => if h : k = 1 then k⁻¹, else 0
          Instances For
            Equations
            • =
            theorem PadicInt.intCast_eq {p : } [Fact (Nat.Prime p)] (z1 : ) (z2 : ) :
            z1 = z2 z1 = z2
            @[deprecated PadicInt.intCast_eq]
            theorem PadicInt.coe_int_eq {p : } [Fact (Nat.Prime p)] (z1 : ) (z2 : ) :
            z1 = z2 z1 = z2

            Alias of PadicInt.intCast_eq.

            def PadicInt.ofIntSeq {p : } [Fact (Nat.Prime p)] (seq : ) (h : IsCauSeq (padicNorm p) fun (n : ) => (seq n)) :

            A sequence of integers that is Cauchy with respect to the p-adic norm converges to a p-adic integer.

            Equations
            Instances For

              Instances #

              We now show that ℤ_[p] is a

              Equations
              Equations
              • =
              Equations
              theorem PadicInt.norm_def {p : } [Fact (Nat.Prime p)] {z : ℤ_[p]} :
              Equations
              Equations
              • =
              Equations
              • =
              Equations
              • =

              Norm #

              @[simp]
              theorem PadicInt.norm_mul {p : } [Fact (Nat.Prime p)] (z1 : ℤ_[p]) (z2 : ℤ_[p]) :
              z1 * z2 = z1 * z2
              @[simp]
              theorem PadicInt.norm_pow {p : } [Fact (Nat.Prime p)] (z : ℤ_[p]) (n : ) :
              z ^ n = z ^ n
              theorem PadicInt.norm_eq_of_norm_add_lt_right {p : } [Fact (Nat.Prime p)] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (h : z1 + z2 < z2) :
              theorem PadicInt.norm_eq_of_norm_add_lt_left {p : } [Fact (Nat.Prime p)] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (h : z1 + z2 < z1) :
              @[deprecated PadicInt.norm_intCast_eq_padic_norm]

              Alias of PadicInt.norm_intCast_eq_padic_norm.

              @[simp]
              theorem PadicInt.norm_eq_padic_norm {p : } [Fact (Nat.Prime p)] {q : ℚ_[p]} (hq : q 1) :
              q, hq = q
              @[simp]
              theorem PadicInt.norm_p {p : } [Fact (Nat.Prime p)] :
              p = (p)⁻¹
              theorem PadicInt.norm_p_pow {p : } [Fact (Nat.Prime p)] (n : ) :
              p ^ n = p ^ (-n)
              Equations
              • =
              theorem PadicInt.exists_pow_neg_lt (p : ) [hp : Fact (Nat.Prime p)] {ε : } (hε : 0 < ε) :
              ∃ (k : ), p ^ (-k) < ε
              theorem PadicInt.exists_pow_neg_lt_rat (p : ) [hp : Fact (Nat.Prime p)] {ε : } (hε : 0 < ε) :
              ∃ (k : ), p ^ (-k) < ε
              theorem PadicInt.norm_int_lt_one_iff_dvd {p : } [hp : Fact (Nat.Prime p)] (k : ) :
              k < 1 p k
              theorem PadicInt.norm_int_le_pow_iff_dvd {p : } [hp : Fact (Nat.Prime p)] {k : } {n : } :
              k p ^ (-n) p ^ n k

              Valuation on ℤ_[p] #

              def PadicInt.valuation {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) :

              PadicInt.valuation lifts the p-adic valuation on to ℤ_[p].

              Equations
              • x.valuation = (x).valuation
              Instances For
                theorem PadicInt.norm_eq_pow_val {p : } [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x 0) :
                x = p ^ (-x.valuation)
                @[simp]
                @[simp]
                @[simp]
                theorem PadicInt.valuation_p {p : } [hp : Fact (Nat.Prime p)] :
                (p).valuation = 1
                theorem PadicInt.valuation_nonneg {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) :
                0 x.valuation
                @[simp]
                theorem PadicInt.valuation_p_pow_mul {p : } [hp : Fact (Nat.Prime p)] (n : ) (c : ℤ_[p]) (hc : c 0) :
                (p ^ n * c).valuation = n + c.valuation

                Units of ℤ_[p] #

                theorem PadicInt.mul_inv {p : } [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} :
                z = 1z * z.inv = 1
                theorem PadicInt.inv_mul {p : } [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} (hz : z = 1) :
                z.inv * z = 1
                theorem PadicInt.isUnit_iff {p : } [hp : Fact (Nat.Prime p)] {z : ℤ_[p]} :
                theorem PadicInt.norm_lt_one_add {p : } [hp : Fact (Nat.Prime p)] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (hz1 : z1 < 1) (hz2 : z2 < 1) :
                z1 + z2 < 1
                theorem PadicInt.norm_lt_one_mul {p : } [hp : Fact (Nat.Prime p)] {z1 : ℤ_[p]} {z2 : ℤ_[p]} (hz2 : z2 < 1) :
                z1 * z2 < 1
                def PadicInt.mkUnits {p : } [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : u = 1) :

                A p-adic number u with ‖u‖ = 1 is a unit of ℤ_[p].

                Equations
                • PadicInt.mkUnits h = let z := u, ; { val := z, inv := z.inv, val_inv := , inv_val := }
                Instances For
                  @[simp]
                  theorem PadicInt.mkUnits_eq {p : } [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : u = 1) :
                  (PadicInt.mkUnits h) = u
                  @[simp]
                  theorem PadicInt.norm_units {p : } [hp : Fact (Nat.Prime p)] (u : ℤ_[p]ˣ) :
                  u = 1
                  def PadicInt.unitCoeff {p : } [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x 0) :

                  unitCoeff hx is the unit u in the unique representation x = u * p ^ n. See unitCoeff_spec.

                  Equations
                  Instances For
                    @[simp]
                    theorem PadicInt.unitCoeff_coe {p : } [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x 0) :
                    (PadicInt.unitCoeff hx) = x * p ^ (-x.valuation)
                    theorem PadicInt.unitCoeff_spec {p : } [hp : Fact (Nat.Prime p)] {x : ℤ_[p]} (hx : x 0) :
                    x = (PadicInt.unitCoeff hx) * p ^ x.valuation.natAbs

                    Various characterizations of open unit balls #

                    theorem PadicInt.norm_le_pow_iff_le_valuation {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x 0) (n : ) :
                    x p ^ (-n) n x.valuation
                    theorem PadicInt.mem_span_pow_iff_le_valuation {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (hx : x 0) (n : ) :
                    x Ideal.span {p ^ n} n x.valuation
                    theorem PadicInt.norm_le_pow_iff_mem_span_pow {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ) :
                    x p ^ (-n) x Ideal.span {p ^ n}
                    theorem PadicInt.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 PadicInt.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 PadicInt.norm_lt_one_iff_dvd {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) :
                    x < 1 p x
                    @[simp]
                    theorem PadicInt.pow_p_dvd_int_iff {p : } [hp : Fact (Nat.Prime p)] (n : ) (a : ) :
                    p ^ n a p ^ n a

                    Discrete valuation ring #

                    Equations
                    • =
                    theorem PadicInt.prime_p {p : } [hp : Fact (Nat.Prime p)] :
                    Prime p
                    theorem PadicInt.ideal_eq_span_pow_p {p : } [hp : Fact (Nat.Prime p)] {s : Ideal ℤ_[p]} (hs : s ) :
                    ∃ (n : ), s = Ideal.span {p ^ n}
                    instance PadicInt.algebra {p : } [hp : Fact (Nat.Prime p)] :
                    Equations
                    @[simp]
                    theorem PadicInt.algebraMap_apply {p : } [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) :
                    Equations
                    • =