The universal property of the model space C₀(I, R)

Let R be a seminormed ring, I a discrete index type and M a complete ultrametric normed R-module with contractive scalar action. A bounded family e : I → M, that is an element of lp (fun _ : I ↦ M) ∞, defines a continuous linear map

ZeroAtInftyContinuousMap.linearCombination R e : C₀(I, R) →L[R] M, a ↦ ∑' i, a i • e i.

The series converges because its terms tend to zero along the cofinite filter, which suffices in a complete ultrametric group, and the ultrametric inequality bounds its sum by ‖e‖ * ‖a‖. The map sends the coordinate vector single i 1 to e i, and over a norm-one ring its operator norm is the supremum ‖e‖ of the norms of the e i. None of this needs a pseudo-uniformiser.

Conversely, over a ring admitting a multiplicative pseudo-uniformiser (TauCeti.NormedRing.IsTate R) every continuous linear map u : C₀(I, R) →L[R] M has a uniform bound, so the family i ↦ u (single i 1) is bounded and u is its linear combination map. Over a commutative such ring this gives the linear isometric equivalence

linearCombinationEquiv R M : lp (fun _ : I ↦ M) ∞ ≃ₗᵢ[R] (C₀(I, R) →L[R] M)

for the operator norm of the scope TauCeti.RingOpNorm. Over a nontrivially normed field the norm identity is stated for Mathlib's operator norm (opNorm_linearCombination).

This is the basic way to construct continuous linear maps out of the model spaces C₀(I, R) of nonarchimedean functional analysis, for instance from bounded lifts of the coordinate vectors.

Main definitions

• ZeroAtInftyContinuousMap.linearCombination: the continuous linear map C₀(I, R) →L[R] M attached to a bounded family in M.
• ZeroAtInftyContinuousMap.linearCombinationEquiv: over a commutative ring with a multiplicative pseudo-uniformiser, bounded families correspond isometrically to continuous linear maps.

Main results

• ZeroAtInftyContinuousMap.hasSum_linearCombination: the unconditional expansion ∑ i, a i • e i = linearCombination R e a.
• ZeroAtInftyContinuousMap.linearCombination_single: the value on a coordinate vector.
• ZeroAtInftyContinuousMap.eq_linearCombination_iff: a continuous linear map is the linear combination map of a bounded family exactly when it sends each unit coordinate vector to the corresponding family member.
• ZeroAtInftyContinuousMap.linearCombination_eq_tsum_mul: for scalar-valued families, the pairing ∑' i, b i * a i.
• ZeroAtInftyContinuousMap.ringOpNorm_linearCombination: over a norm-one ring the operator norm is the family supremum.
• ZeroAtInftyContinuousMap.linearCombination_injective and ZeroAtInftyContinuousMap.linearCombination_self: bounded families are determined by their linear combination maps, and over Tate scalars every continuous linear map is one.

References

• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §10.
• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85.

theorem ZeroAtInftyContinuousMap.norm_tsum_smul_le {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] (a : ZeroAtInftyContinuousMap I R) (e : ↥(lp (fun (x : I) => M) ⊤)) : ‖∑' (i : I), a i • ↑e i‖ ≤ ‖e‖ * ‖a‖

The ultrametric inequality bounds ∑' i, a i • e i by ‖e‖ * ‖a‖ for a family a vanishing at infinity and a bounded family e.

theorem ZeroAtInftyContinuousMap.tendsto_smul_cofinite {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] (a : ZeroAtInftyContinuousMap I R) (e : ↥(lp (fun (x : I) => M) ⊤)) : Filter.Tendsto (fun (i : I) => a i • ↑e i) Filter.cofinite (nhds 0)

On a discrete index, the terms a i • e i of a family a vanishing at infinity against a bounded family e tend to zero along the cofinite filter.

theorem ZeroAtInftyContinuousMap.summable_smul {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (a : ZeroAtInftyContinuousMap I R) (e : ↥(lp (fun (x : I) => M) ⊤)) : Summable fun (i : I) => a i • ↑e i

In a complete ultrametric module, the series ∑' i, a i • e i is summable for every a ∈ C₀(I, R) and every bounded family e.

noncomputable def ZeroAtInftyContinuousMap.linearCombination {I : Type u_1} (R : Type u_2) {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) : ZeroAtInftyContinuousMap I R →L[R] M

The linear combination map of a bounded family e in a complete ultrametric module: the continuous linear map C₀(I, R) →L[R] M sending a to the unconditional sum ∑' i, a i • e i. It sends the coordinate vector single i 1 to e i.

theorem ZeroAtInftyContinuousMap.linearCombination_apply {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) (a : ZeroAtInftyContinuousMap I R) : (linearCombination R e) a = ∑' (i : I), a i • ↑e i

The value of the linear combination map is the sum ∑' i, a i • e i.

theorem ZeroAtInftyContinuousMap.hasSum_linearCombination {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) (a : ZeroAtInftyContinuousMap I R) : HasSum (fun (i : I) => a i • ↑e i) ((linearCombination R e) a)

Unconditional expansion: linearCombination R e a is the unconditional sum of the a i • e i.

@[simp]

theorem ZeroAtInftyContinuousMap.linearCombination_single {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] (e : ↥(lp (fun (x : I) => M) ⊤)) (i : I) (r : R) : (linearCombination R e) (single i r) = r • ↑e i

The linear combination map sends the coordinate vector single i r to r • e i.

theorem ZeroAtInftyContinuousMap.eq_linearCombination_iff {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] {e : ↥(lp (fun (x : I) => M) ⊤)} {u : ZeroAtInftyContinuousMap I R →L[R] M} : u = linearCombination R e ↔ ∀ (i : I), u (single i 1) = ↑e i

The linear combination map of a bounded family is the unique continuous linear map sending each unit coordinate vector single i 1 to e i.

@[simp]

theorem ZeroAtInftyContinuousMap.linearCombination_lpSingle {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] (i : I) (m : M) (a : ZeroAtInftyContinuousMap I R) : (linearCombination R (lp.single ⊤ i m)) a = a i • m

Pairing the coordinate family lp.single ∞ i m with a gives a i • m.

theorem ZeroAtInftyContinuousMap.norm_linearCombination_apply_le {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) (a : ZeroAtInftyContinuousMap I R) : ‖(linearCombination R e) a‖ ≤ ‖e‖ * ‖a‖

The linear combination map is bounded by the supremum of the family.

theorem ZeroAtInftyContinuousMap.ringOpNorm_linearCombination_le {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) : ‖linearCombination R e‖ ≤ ‖e‖

The operator norm of the linear combination map is at most the supremum of the family.

@[simp]

theorem ZeroAtInftyContinuousMap.ringOpNorm_linearCombination {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] [NormOneClass R] (e : ↥(lp (fun (x : I) => M) ⊤)) : ‖linearCombination R e‖ = ‖e‖

The norm of a linear combination map: over a norm-one ring, the operator norm of linearCombination R e is the supremum ‖e‖ = ⨆ i, ‖e i‖ of the family.

@[simp]

theorem ZeroAtInftyContinuousMap.linearCombination_zero {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] : linearCombination R 0 = 0

The zero family has the zero linear combination map.

theorem ZeroAtInftyContinuousMap.linearCombination_add {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] (e f : ↥(lp (fun (x : I) => M) ⊤)) : linearCombination R (e + f) = linearCombination R e + linearCombination R f

The linear combination map is additive in the family.

theorem ZeroAtInftyContinuousMap.linearCombination_injective {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DiscreteTopology I] [IsUltrametricDist M] [CompleteSpace M] : Function.Injective (linearCombination R)

A bounded family is determined by its linear combination map.

@[simp]

theorem ZeroAtInftyContinuousMap.opNorm_linearCombination {I : Type u_1} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] {K : Type u_4} [NontriviallyNormedField K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] [CompleteSpace M] (e : ↥(lp (fun (x : I) => M) ⊤)) : ‖linearCombination K e‖ = ‖e‖

Over a nontrivially normed field, the operator norm of linearCombination K e for Mathlib's operator norm is the supremum of the family.

theorem ZeroAtInftyContinuousMap.memℓp_infty_apply_single {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [DecidableEq I] (u : ZeroAtInftyContinuousMap I R →L[R] M) : Memℓp (fun (i : I) => u (single i 1)) ⊤

Over Tate scalars, the values of a continuous linear map u out of C₀(I, R) at the unit coordinate vectors form a bounded family, bounded by the operator norm of u.

theorem ZeroAtInftyContinuousMap.linearCombination_self {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] (u : ZeroAtInftyContinuousMap I R →L[R] M) : linearCombination R ⟨fun (i : I) => u (single i 1), ⋯⟩ = u

Every continuous linear map out of C₀(I, R) is a linear combination map over Tate scalars: u is the linear combination map of its values at the unit coordinate vectors.

theorem ZeroAtInftyContinuousMap.linearCombination_surjective {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] : Function.Surjective (linearCombination R)

Over Tate scalars, every continuous linear map out of C₀(I, R) is the linear combination map of a bounded family.

theorem ZeroAtInftyContinuousMap.linearCombination_smul {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] (c : R) (e : ↥(lp (fun (x : I) => M) ⊤)) : linearCombination R (c • e) = c • linearCombination R e

Over a commutative ring, the linear combination map is linear in the family.

theorem ZeroAtInftyContinuousMap.linearCombination_eq_tsum_mul {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] (b : ↥(lp (fun (x : I) => R) ⊤)) (a : ZeroAtInftyContinuousMap I R) : (linearCombination R b) a = ∑' (i : I), ↑b i * a i

The pairing of a bounded family b with a ∈ C₀(I, R) is the convergent sum ∑' i, b i * a i.

noncomputable def ZeroAtInftyContinuousMap.linearCombinationEquiv {I : Type u_1} (R : Type u_2) (M : Type u_3) [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] : ↥(lp (fun (x : I) => M) ⊤) ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R →L[R] M

The universal property of C₀(I, R). Over a commutative ring admitting a multiplicative pseudo-uniformiser, bounded families I → M in a complete ultrametric module correspond to continuous linear maps C₀(I, R) →L[R] M, isometrically for the sup norm and the operator norm. A family e is sent to its linear combination map a ↦ ∑' i, a i • e i, and a map u to its values u (single i 1) at the unit coordinate vectors.

@[simp]

theorem ZeroAtInftyContinuousMap.linearCombinationEquiv_apply {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] (e : ↥(lp (fun (x : I) => M) ⊤)) : (linearCombinationEquiv R M) e = linearCombination R e

The universal property sends a bounded family to its linear combination map.

@[simp]

theorem ZeroAtInftyContinuousMap.linearCombinationEquiv_symm_apply {I : Type u_1} {R : Type u_2} {M : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] (u : ZeroAtInftyContinuousMap I R →L[R] M) (i : I) : ↑((linearCombinationEquiv R M).symm u) i = u (single i 1)

The inverse of the universal property evaluates a map at the unit coordinate vectors.