Extension of coefficients of measures from the unit ball

Let X be a profinite space, O a topological commutative ring, K a complete ultrametric normed field and j : O →+* K a ring homomorphism with ‖j a‖ ≤ 1 for every a. A measure μ ∈ D(X, O) takes values in O only on O-valued test functions; this file extends it to a K-valued measure ι_j(μ) = extendCoefficients j hj μ ∈ D(X, K).

On a locally constant function Σ_i c_i 1_{U_i} attached to a finite clopen partition the extension is Σ_i c_i j(μ(1_{U_i})). This does not depend on the partition, and by the ultrametric inequality it is bounded by max_i ‖c_i‖, so it extends by density and completeness of K to all of C(X, K). The resulting measure is characterised by its finite projections: along every map q : X → A to a finite discrete space, the coefficients of ι_j(μ) are the images under j of those of μ. In particular ι_j(μ)(j ∘ f) = j(μ(f)) for every f ∈ C(X, O) when j is continuous, and this property determines ι_j(μ). If j is moreover a topological embedding onto the closed unit ball of K, the measures ι_j(μ) are exactly the K-valued measures of operator norm at most 1: such a measure sends test functions j ∘ f into the closed unit ball, hence into the image of j.

The bound ‖j a‖ ≤ 1 cannot be dropped: give O = ℚ_p the norm max(1, |a|_p) for a ≠ 0, so that its topology is discrete. Then Haar averaging f ↦ p^{-n} Σ_{a mod p^n} f(a) is an O-valued measure on ℤ_p with μ(1_{p^n ℤ_p}) = p^{-n}, and for j = id into the usual ℚ_p no continuous extension exists, since p^n 1_{p^n ℤ_p} → 0 would have integral 1.

Main definitions

• AbstractMeasure.extendCoefficients j hj: the additive map D(X, O) → D(X, K).

Main results

• AbstractMeasure.finiteProjection_extendCoefficients: the finite projections of extendCoefficients j hj μ are those of μ with j applied to the coefficients.
• AbstractMeasure.extendCoefficients_apply_comp_eq_sum: integration of a function factoring through a finite discrete quotient.
• AbstractMeasure.extendCoefficients_apply_locallyConstant: agreement with j on locally constant source-valued tests, without assuming continuity of j.
• AbstractMeasure.norm_toCLMEquiv_extendCoefficients_le: the extension has norm at most 1.
• AbstractMeasure.extendCoefficients_apply_comp: ι_j(μ)(j ∘ f) = j(μ(f)) for continuous j.
• AbstractMeasure.eq_extendCoefficients_of_apply_comp: this property characterises ι_j(μ).
• AbstractMeasure.exists_apply_comp_eq_of_norm_le_one: for an embedding j onto the closed unit ball of K and compact X, a K-valued measure of norm at most 1 restricts to an O-valued measure.
• AbstractMeasure.mem_range_extendCoefficients_iff, AbstractMeasure.existsUnique_apply_comp_eq_iff_norm_le_one: for an embedding j onto the closed unit ball, the extensions of coefficients form the closed unit ball of D(X, K).
• AbstractMeasure.extendCoefficients_smul, AbstractMeasure.extendCoefficients_dirac, AbstractMeasure.extendCoefficients_map and AbstractMeasure.extendCoefficients_injective.

References

• J. Rodrigues Jacinto and C. Williams, An introduction to p-adic L-functions, Essential Number Theory 4 (2025), no. 1, 101–216, Proposition 3.16 and Remark 3.28.

noncomputable def AbstractMeasure.extendCoefficients {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) : AbstractMeasure X O O →+ AbstractMeasure X K K

Extension of coefficients from the unit ball. For a ring homomorphism j : O →+* K into the closed unit ball of a complete ultrametric field, extendCoefficients j hj μ is the K-valued measure on the profinite space X whose coefficient on each fibre of a map to a finite discrete space is the image under j of the coefficient of μ (finiteProjection_extendCoefficients). When j is continuous it is the unique K-valued measure with ι_j(μ)(j ∘ f) = j(μ(f)) for all f ∈ C(X, O) (extendCoefficients_apply_comp, eq_extendCoefficients_of_apply_comp).

@[simp]

theorem AbstractMeasure.finiteProjection_extendCoefficients {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) {A : Type u_4} [TopologicalSpace A] [DiscreteTopology A] [Finite A] (q : C(X, A)) : (finiteProjection q) ((extendCoefficients j hj) μ) = Finsupp.mapRange ⇑j ⋯ ((finiteProjection q) μ)

The finite projections of extendCoefficients j hj μ are those of μ, with j applied to the coefficients.

theorem AbstractMeasure.extendCoefficients_apply_comp_eq_sum {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) {A : Type u_4} [TopologicalSpace A] [DiscreteTopology A] [Fintype A] (q : C(X, A)) (g : A → K) : ((extendCoefficients j hj) μ) ((ContinuousMap.equivFnOfDiscrete.symm g).comp q) = ∑ a : A, g a * j (((finiteProjection q) μ) a)

Integrating a function that factors through a finite discrete quotient against extendCoefficients j hj μ is the finite sum of its values against the coefficients of μ transported by j.

@[simp]

theorem AbstractMeasure.extendCoefficients_apply_locallyConstant {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) (f : LocallyConstant X O) : ((extendCoefficients j hj) μ) ↑(LocallyConstant.map (⇑j) f) = j (μ ↑f)

Extension agrees with the coefficient homomorphism on locally constant source-valued tests, without assuming that the coefficient homomorphism is continuous.

@[simp]

theorem AbstractMeasure.extendCoefficients_smul {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) (a : O) : (extendCoefficients j hj) (a • μ) = j a • (extendCoefficients j hj) μ

Extension of coefficients is semilinear along j.

@[simp]

theorem AbstractMeasure.extendCoefficients_dirac {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) (x : X) : (extendCoefficients j hj) (dirac O x) = dirac K x

Extension of coefficients sends Dirac measures to Dirac measures.

@[simp]

theorem AbstractMeasure.extendCoefficients_map {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) {Y : Type u_4} [TopologicalSpace Y] [CompactSpace Y] [T2Space Y] [TotallyDisconnectedSpace Y] (φ : C(X, Y)) : (extendCoefficients j hj) ((map φ) μ) = (map φ) ((extendCoefficients j hj) μ)

Extension of coefficients commutes with pushforward along continuous maps of profinite spaces.

theorem AbstractMeasure.extendCoefficients_apply_comp {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) (hjc : Continuous ⇑j) (f : C(X, O)) : ((extendCoefficients j hj) μ) ({ toFun := ⇑j, continuous_toFun := hjc }.comp f) = j (μ f)

For continuous j, the extension of coefficients of μ integrates j ∘ f to j (μ f) for every f ∈ C(X, O).

theorem AbstractMeasure.eq_extendCoefficients_of_apply_comp {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (μ : AbstractMeasure X O O) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) (hjc : Continuous ⇑j) {ν : AbstractMeasure X K K} (hν : ∀ (f : C(X, O)), ν ({ toFun := ⇑j, continuous_toFun := hjc }.comp f) = j (μ f)) : ν = (extendCoefficients j hj) μ

A K-valued measure taking the value j (μ f) on every test function j ∘ f is the extension of coefficients of μ.

theorem AbstractMeasure.extendCoefficients_injective {X : Type u_1} [TopologicalSpace X] {K : Type u_2} {O : Type u_3} [NormedField K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) [CompactSpace X] [IsUltrametricDist K] [T2Space X] [TotallyDisconnectedSpace X] [CompleteSpace K] (hj : ∀ (a : O), ‖j a‖ ≤ 1) [T2Space O] (hinj : Function.Injective ⇑j) : Function.Injective ⇑(extendCoefficients j hj)

Extension of coefficients along an injective j is injective.

theorem AbstractMeasure.norm_toCLMEquiv_extendCoefficients_le {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] {K : Type u_2} {O : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] (j : O →+* K) (hj : ∀ (a : O), ‖j a‖ ≤ 1) (μ : AbstractMeasure X O O) : ‖toCLMEquiv ((extendCoefficients j hj) μ)‖ ≤ 1

The extension of coefficients has operator norm at most 1.

theorem AbstractMeasure.exists_apply_comp_eq_of_norm_le_one {X : Type u_1} [TopologicalSpace X] [CompactSpace X] {K : Type u_2} {O : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] {j : O →+* K} (hj : ∀ (a : O), ‖j a‖ ≤ 1) (hje : Topology.IsEmbedding ⇑j) (hjr : Metric.closedBall 0 1 ⊆ Set.range ⇑j) {ν : AbstractMeasure X K K} (hν : ‖toCLMEquiv ν‖ ≤ 1) : ∃ (μ : AbstractMeasure X O O), ∀ (f : C(X, O)), ν ({ toFun := ⇑j, continuous_toFun := ⋯ }.comp f) = j (μ f)

If j is a topological embedding onto the closed unit ball of K, a K-valued measure ν of norm at most 1 sends the test functions j ∘ f into the image of j, and the preimages form an O-valued measure μ with ν (j ∘ f) = j (μ f).

theorem AbstractMeasure.mem_range_extendCoefficients_iff {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] {K : Type u_2} {O : Type u_3} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] {j : O →+* K} (hj : ∀ (a : O), ‖j a‖ ≤ 1) (hje : Topology.IsEmbedding ⇑j) (hjr : Metric.closedBall 0 1 ⊆ Set.range ⇑j) {ν : AbstractMeasure X K K} : ν ∈ (extendCoefficients j hj).range ↔ ‖toCLMEquiv ν‖ ≤ 1

The dual unit ball. If j is a topological embedding onto the closed unit ball of K, the extensions of coefficients of O-valued measures are exactly the K-valued measures of operator norm at most 1.

theorem AbstractMeasure.existsUnique_apply_comp_eq_iff_norm_le_one {X : Type u_1} [TopologicalSpace X] [CompactSpace X] {K : Type u_2} {O : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CommRing O] [TopologicalSpace O] [IsTopologicalRing O] {j : O →+* K} (hj : ∀ (a : O), ‖j a‖ ≤ 1) (hje : Topology.IsEmbedding ⇑j) (hjr : Metric.closedBall 0 1 ⊆ Set.range ⇑j) (ν : AbstractMeasure X K K) : (∃! μ : AbstractMeasure X O O, ∀ (f : C(X, O)), ν ({ toFun := ⇑j, continuous_toFun := ⋯ }.comp f) = j (μ f)) ↔ ‖toCLMEquiv ν‖ ≤ 1

If j is a topological embedding onto the closed unit ball of K, a K-valued measure ν has operator norm at most 1 exactly when there is a unique O-valued measure μ with ν (j ∘ f) = j (μ f) for every f ∈ C(X, O).