ℂ_p is separable

The field ℂ_[p] of p-adic complex numbers is the completion of an algebraic closure of ℚ_[p]. It contains the countable set of algebraic numbers, the elements algebraic over ℚ, as a dense subset. Indeed the image of the algebraic closure of ℚ_[p] is dense, and each of its elements is a limit of algebraic numbers: approximate its minimal polynomial over ℚ_[p] by one over ℚ and take a nearby root (IsAlgebraic.mem_closure_setOf_isAlgebraic).

Separability is what makes ℂ_p fail to be spherically complete, so that the closed unit disc over ℂ_p has points of type (4).

The file also compares the valuation with the norm, records ‖p‖ = p⁻¹ < 1 and the residue characteristic, and provides the integral coefficient inclusion and topological nilpotence of ζ - 1 for p-th roots of unity.

Main results

• PadicComplex.valuation_coe: the real value of the valuation is the norm.
• PadicComplex.residueFieldCharP: the residue field of 𝓞_ℂ_[p] has characteristic p.
• PadicComplex.instIsLinearTopologyInt, PadicComplex.instCompleteSpaceInt: the integers of ℂ_p are complete and linearly topologized.
• PadicComplex.integralCoefficientMap: the continuous, injective inclusion ℤ_[p] →+* 𝓞_ℂ_[p].
• PadicComplex.isTopologicallyNilpotent_sub_one: ζ - 1 is topologically nilpotent if ζ ^ p = 1.
• PadicComplex.norm_p: ‖p‖ = p⁻¹ in ℂ_[p].
• PadicComplex.norm_p_lt_one: ‖p‖ < 1 in ℂ_[p].
• PadicComplex.dense_setOf_isAlgebraic: the algebraic numbers are dense in ℂ_[p].
• PadicComplex.separableSpace: ℂ_[p] is a separable space.

References

• A. M. Robert, A Course in p-adic Analysis, Graduate Texts in Mathematics 198, Springer, 2000, Chapter 3, for the density of the algebraic numbers in ℂ_p and the separability of ℂ_p.

theorem PadicComplex.valuation_coe (p : ℕ) [Fact (Nat.Prime p)] (x : ℂ_[p]) : ↑(Valued.v x) = ‖x‖

The real value of the valuation on ℂ_[p] is its norm.

@[simp]

theorem PadicComplex.norm_p (p : ℕ) [Fact (Nat.Prime p)] : ‖↑p‖ = (↑p)⁻¹

The norm of p in ℂ_[p] is p⁻¹.

theorem PadicComplex.norm_p_lt_one (p : ℕ) [Fact (Nat.Prime p)] : ‖↑p‖ < 1

‖p‖ < 1 in ℂ_[p].

instance PadicComplex.instIsLinearTopologyInt (p : ℕ) [Fact (Nat.Prime p)] : IsLinearTopology ↥𝓞_ℂ_[p] ↥𝓞_ℂ_[p]

The integers of ℂ_p have a linear topology.

instance PadicComplex.instCompleteSpaceInt (p : ℕ) [Fact (Nat.Prime p)] : CompleteSpace ↥𝓞_ℂ_[p]

The integers of ℂ_p are complete for the induced uniformity.

instance PadicComplex.residueFieldCharP (p : ℕ) [Fact (Nat.Prime p)] : CharP (IsLocalRing.ResidueField ↥𝓞_ℂ_[p]) p

The residue field of the integers of ℂ_p has characteristic p.

noncomputable def PadicComplex.integralCoefficientMap (p : ℕ) [Fact (Nat.Prime p)] : ℤ_[p] →+* ↥𝓞_ℂ_[p]

The coefficient inclusion from the p-adic integers into the integers of ℂ_p.

@[simp]

theorem PadicComplex.integralCoefficientMap_coe (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : ↑((integralCoefficientMap p) x) = (algebraMap ℚ_[p] ℂ_[p]) ↑x

theorem PadicComplex.continuous_integralCoefficientMap (p : ℕ) [Fact (Nat.Prime p)] : Continuous ⇑(integralCoefficientMap p)

The integral coefficient inclusion is continuous for the induced p-adic topologies.

theorem PadicComplex.integralCoefficientMap_injective (p : ℕ) [Fact (Nat.Prime p)] : Function.Injective ⇑(integralCoefficientMap p)

Extending integral coefficients to ℂ_p loses no information.

theorem PadicComplex.isTopologicallyNilpotent_sub_one (p : ℕ) [Fact (Nat.Prime p)] (ζ : ↥𝓞_ℂ_[p]) (hζ : ζ ^ p = 1) : IsTopologicallyNilpotent (ζ - 1)

The translated constant term of a p-th root of unity is topologically nilpotent.

theorem PadicComplex.dense_setOf_isAlgebraic (p : ℕ) [Fact (Nat.Prime p)] : Dense {x : ℂ_[p] | IsAlgebraic ℚ x}

The algebraic numbers are dense in ℂ_[p].

instance PadicComplex.separableSpace (p : ℕ) [Fact (Nat.Prime p)] : TopologicalSpace.SeparableSpace ℂ_[p]

ℂ_[p] is separable: the countable set of algebraic numbers is dense.