Basic instances for the `p`-adic numbers #

This file provides a direct instance for the nontriviality of ℚ_[p], already implied by its field structure, and an instance expressing that 2 is invertible. These instances support finite-dimensional constructions and algebraic trace and norm calculations over the p-adic field.

It also records that the scalar action of ℤ_[p] on ℚ_[p] multiplies norms, ‖a • x‖ = ‖a‖ * ‖x‖. In particular the action is contractive, so ℚ_[p] itself is a coefficient ring for Mathlib's Mahler isometry PadicInt.mahlerEquiv and for the Amice transform of measures on ℤ_p.

Finally, it records that the inclusion PadicInt.Coe.ringHom : ℤ_[p] →+* ℚ_[p] is the structure map of the ℤ_[p]-algebra ℚ_[p], and that it is a topological embedding of norm at most 1 whose range contains the closed unit ball. These are the hypotheses under which ℚ_[p]-valued measures of norm at most 1 come from ℤ_[p]-valued measures.

For a normed ℚ_[p]-algebra K, the composite structure map TauCeti.padicIntAlgebraMap p K : ℤ_[p] →+* K is continuous. When ‖1‖ = 1 in K it is an isometry, so it maps ℤ_[p] into the closed unit ball of K, and it is injective when K is nontrivial. When ‖1‖ = 1 in K, the norm of a natural number in K is also its p-adic norm (TauCeti.norm_natCast_eq_norm_padic).

source

instance TauCeti.instNontrivialPadic_tauCeti (p : ℕ) [Fact (Nat.Prime p)] :

Nontrivial ℚ_[p]

A direct instance of the existing fact that the p-adic field has distinct zero and one.

source

@[instance_reducible]

noncomputable instance TauCeti.instInvertibleTwoPadic (p : ℕ) [Fact (Nat.Prime p)] :

Invertible 2

Two is invertible in the p-adic field, including when p = 2.

source

instance TauCeti.normSMulClass_padicInt_padic (p : ℕ) [Fact (Nat.Prime p)] :

NormSMulClass ℤ_[p] ℚ_[p]

The scalar action of ℤ_[p] on ℚ_[p] is multiplication by the inclusion, so it multiplies norms. This also provides the contractive action IsBoundedSMul ℤ_[p] ℚ_[p].

source

theorem PadicInt.algebraMap_eq_coe_ringHom {p : ℕ} [Fact (Nat.Prime p)] :

algebraMap ℤ_[p] ℚ_[p] = Coe.ringHom

The structure map of the ℤ_[p]-algebra ℚ_[p] is the inclusion PadicInt.Coe.ringHom.

source

theorem PadicInt.norm_coe_ringHom_le_one {p : ℕ} [Fact (Nat.Prime p)] (a : ℤ_[p]) :

‖Coe.ringHom a‖ ≤ 1

The inclusion ℤ_[p] → ℚ_[p] takes values in the closed unit ball.

source

theorem PadicInt.isEmbedding_coe_ringHom {p : ℕ} [Fact (Nat.Prime p)] :

Topology.IsEmbedding ⇑Coe.ringHom

The inclusion ℤ_[p] → ℚ_[p] is a topological embedding.

source

theorem PadicInt.closedBall_subset_range_coe_ringHom {p : ℕ} [Fact (Nat.Prime p)] :

Metric.closedBall 0 1 ⊆ Set.range ⇑Coe.ringHom

Every element of the closed unit ball of ℚ_[p] lies in the image of ℤ_[p].

source

noncomputable def TauCeti.padicIntAlgebraMap (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [SeminormedRing K] [NormedAlgebra ℚ_[p] K] :

ℤ_[p] →+* K

The structure map ℤ_p → K of a normed ℚ_p-algebra K, through ℚ_p. It is an isometry onto its image when ‖1‖ = 1 in K (TauCeti.norm_padicIntAlgebraMap).

Instances For

source

@[simp]