Documentation

Mathlib.NumberTheory.Padics.Complex

The field ℂ_[p] of p-adic complex numbers. #

In this file we define the field ℂ_[p] of p-adic complex numbers as the p-adic completion of an algebraic closure of ℚ_[p]. We endow ℂ_[p] with both a normed field and a valued field structure, induced by the unique extension of the p-adic norm to ℂ_[p].

Main Definitions #

Main Results #

Notation #

We introduce the notation ℂ_[p] for the p-adic complex numbers, and 𝓞_ℂ_[p] for its ring of integers.

Tags #

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

@[reducible, inline]
abbrev PadicAlgCl (p : ) [hp : Fact (Nat.Prime p)] :

PadicAlgCl p is a fixed algebraic closure of ℚ_[p].

Equations
Instances For

    PadicAlgCl p is an algebraic extension of ℚ_[p].

    PadicAlgCl p is a normed field, where the norm is the p-adic norm, that is, the spectral norm induced by the p-adic norm on ℚ_[p].

    Equations

    The norm on PadicAlgCl p is nonarchimedean.

    @[simp]

    The norm on PadicAlgCl p is the spectral norm induced by the p-adic norm on ℚ_[p].

    @[simp]

    The norm on PadicAlgCl p extends the p-adic norm on ℚ_[p].

    instance PadicAlgCl.valued (p : ) [hp : Fact (Nat.Prime p)] :

    PadicAlgCl p is a valued field, with the valuation corresponding to the p-adic norm.

    Equations

    The valuation of x : PadicAlgCl p agrees with its ℝ≥0-valued norm.

    @[simp]
    theorem PadicAlgCl.valuation_coe (p : ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) :
    (Valued.v x) = x

    The coercion of the valuation of x : PadicAlgCl p to agrees with its norm.

    theorem PadicAlgCl.valuation_p (p : ) [Fact (Nat.Prime p)] :
    Valued.v p = 1 / p

    The valuation of p : PadicAlgCl p is 1/p.

    The valuation on PadicAlgCl p has rank one.

    Equations
    @[reducible, inline]
    abbrev PadicComplex (p : ) [hp : Fact (Nat.Prime p)] :

    ℂ_[p] is the field of p-adic complex numbers, that is, the completion of PadicAlgCl p with respect to the p-adic norm.

    Equations
    Instances For

      ℂ_[p] is the field of p-adic complex numbers.

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

        ℂ_[p] is a valued field, where the valuation is the one extending that on PadicAlgCl p.

        Equations

        The valuation on ℂ_[p] extends the valuation on PadicAlgCl p.

        theorem PadicComplex.coe_eq (p : ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) :
        @[simp]
        theorem PadicComplex.coe_zero (p : ) [hp : Fact (Nat.Prime p)] :
        0 = 0

        ℂ_[p] is an algebra over ℚ_[p].

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem PadicComplex.coe_natCast (p : ) [hp : Fact (Nat.Prime p)] (n : ) :
        n = n
        theorem PadicComplex.valuation_p (p : ) [hp : Fact (Nat.Prime p)] :
        Valued.v p = 1 / p

        The valuation of p : ℂ_[p] is 1/p.

        The valuation on ℂ_[p] has rank one.

        Equations

        ℂ_[p] is a normed field, where the norm corresponds to the extension of the p-adic valuation.

        Equations
        theorem PadicComplex.norm_extends (p : ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) :

        The norm on ℂ_[p] extends the norm on PadicAlgCl p.

        The ℝ≥0-valued norm on ℂ_[p] extends that on PadicAlgCl p.

        The norm on ℂ_[p] is nonarchimedean.

        We define 𝓞_ℂ_[p] as the valuation subring of of ℂ_[p], consisting of those elements with valuation ≤ 1.

        Equations
        Instances For

          We define 𝓞_ℂ_[p] as the subring of elements of ℂ_[p] with valuation ≤ 1.

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

            𝓞_ℂ_[p] is the ring of integers of ℂ_[p].