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

• PadicAlgCl p : the algebraic closure of ℚ_[p].
• PadicComplex p : the type of p-adic complex numbers, denoted by ℂ_[p].
• PadicComplexInt p : the ring of integers of ℂ_[p].

Main Results

• PadicComplex.norm_extends : the norm on ℂ_[p] extends the norm on PadicAlgCl p, and hence the norm on ℚ_[p].
• PadicComplex.isNonarchimedean : The norm on ℂ_[p] is nonarchimedean.

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)] : Type

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

theorem PadicAlgCl.isAlgebraic (p : ℕ) [hp : Fact (Nat.Prime p)] : Algebra.IsAlgebraic ℚ_[p] (PadicAlgCl p)

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

instance PadicAlgCl.instCoePadic (p : ℕ) [hp : Fact (Nat.Prime p)] : Coe ℚ_[p] (PadicAlgCl p)

theorem PadicAlgCl.coe_eq (p : ℕ) [hp : Fact (Nat.Prime p)] : Coe.coe = ⇑(algebraMap ℚ_[p] (PadicAlgCl p))

instance PadicAlgCl.normedField (p : ℕ) [hp : Fact (Nat.Prime p)] : NormedField (PadicAlgCl 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].

theorem PadicAlgCl.isNonarchimedean (p : ℕ) [hp : Fact (Nat.Prime p)] : IsNonarchimedean norm

The norm on PadicAlgCl p is nonarchimedean.

@[simp]

theorem PadicAlgCl.spectralNorm_eq (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : spectralNorm ℚ_[p] (PadicAlgCl p) x = ‖x‖

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

@[simp]

theorem PadicAlgCl.norm_extends (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℚ_[p]) : ‖(algebraMap ℚ_[p] (PadicAlgCl p)) x‖ = ‖x‖

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

instance PadicAlgCl.instIsUltrametricDist (p : ℕ) [hp : Fact (Nat.Prime p)] : IsUltrametricDist (PadicAlgCl p)

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

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

theorem PadicAlgCl.valuation_def (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : Valued.v x = ‖x‖₊

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.

instance PadicAlgCl.instRankOneNNRealV (p : ℕ) [hp : Fact (Nat.Prime p)] : Valued.v.RankOne

The valuation on PadicAlgCl p has rank one.

instance PadicAlgCl.instUniformContinuousConstSMulPadic (p : ℕ) [hp : Fact (Nat.Prime p)] : UniformContinuousConstSMul ℚ_[p] (PadicAlgCl p)

@[reducible, inline]

abbrev PadicComplex (p : ℕ) [hp : Fact (Nat.Prime p)] : Type

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

def «termℂ_[_]» : Lean.ParserDescr

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

instance PadicComplex.valued (p : ℕ) [hp : Fact (Nat.Prime p)] : Valued ℂ_[p] NNReal

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

theorem PadicComplex.valuation_extends (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : Valued.v ↑x = Valued.v x

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

theorem PadicComplex.coe_eq (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : ↑x = (algebraMap (PadicAlgCl p) ℂ_[p]) x

@[simp]

theorem PadicComplex.coe_zero (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑0 = 0

instance PadicComplex.instAlgebraPadic (p : ℕ) [hp : Fact (Nat.Prime p)] : Algebra ℚ_[p] ℂ_[p]

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

instance PadicComplex.instIsScalarTowerPadicPadicAlgCl (p : ℕ) [hp : Fact (Nat.Prime p)] : IsScalarTower ℚ_[p] (PadicAlgCl p) ℂ_[p]

@[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.

instance PadicComplex.instRankOneNNRealV (p : ℕ) [hp : Fact (Nat.Prime p)] : Valued.v.RankOne

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

theorem PadicComplex.rankOne_hom_eq (p : ℕ) [hp : Fact (Nat.Prime p)] : Valuation.RankOne.hom Valued.v = Valuation.RankOne.hom Valued.v

instance PadicComplex.instNormedField (p : ℕ) [hp : Fact (Nat.Prime p)] : NormedField ℂ_[p]

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

theorem PadicComplex.norm_def (p : ℕ) [hp : Fact (Nat.Prime p)] : norm = Valued.norm

theorem PadicComplex.norm_extends (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : ‖↑x‖ = ‖x‖

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

theorem PadicComplex.nnnorm_extends (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p) : ‖↑x‖₊ = ‖x‖₊

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

theorem PadicComplex.isNonarchimedean (p : ℕ) [hp : Fact (Nat.Prime p)] : IsNonarchimedean norm

The norm on ℂ_[p] is nonarchimedean.

def PadicComplexInt (p : ℕ) [hp : Fact (Nat.Prime p)] : ValuationSubring ℂ_[p]

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

def «term𝓞_ℂ_[_]» : Lean.ParserDescr

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

theorem PadicComplexInt.integers (p : ℕ) [hp : Fact (Nat.Prime p)] : Valued.v.Integers ↥𝓞_ℂ_[p]

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