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 ofp
-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 onPadicAlgCl 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
PadicAlgCl p
is an algebraic extension of ℚ_[p]
.
Equations
- PadicAlgCl.instCoePadic p = { coe := ⇑(algebraMap ℚ_[p] (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]
.
Equations
The norm on PadicAlgCl p
is nonarchimedean.
The norm on PadicAlgCl p
is the spectral norm induced by the p
-adic norm on ℚ_[p]
.
The norm on PadicAlgCl p
extends the p
-adic norm on ℚ_[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.
The coercion of the valuation of x : PadicAlgCl p
to ℝ
agrees with its norm.
The valuation of p : PadicAlgCl p
is 1/p
.
The valuation on PadicAlgCl p
has rank one.
Equations
- PadicAlgCl.instRankOneNNRealV p = { hom := MonoidWithZeroHom.id NNReal, strictMono' := PadicAlgCl.instRankOneNNRealV._proof_1, nontrivial' := ⋯ }
ℂ_[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
.
The valuation on ℂ_[p]
has rank one.
Equations
- PadicComplex.instRankOneNNRealV p = { hom := MonoidWithZeroHom.id NNReal, strictMono' := PadicAlgCl.instRankOneNNRealV._proof_1, nontrivial' := ⋯ }
ℂ_[p]
is a normed field, where the norm corresponds to the extension of the p
-adic
valuation.
Equations
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.