The model space C₀(I, E) on a discrete index

For a discrete space I, the cocompact filter on I is the cofinite filter, so C₀(I, E) is the space of families I → E tending to zero along the cofinite filter, with the sup norm. Over a complete ultrametric normed ring R, the spaces C₀(I, R) are the model spaces of nonarchimedean functional analysis: orthonormalisable Banach modules are those linearly isometric to some C₀(I, R).

This file develops the coordinate structure of C₀(I, E):

• ZeroAtInftyContinuousMap.mkOfDiscrete: a family tending to zero along the cofinite filter as an element of C₀(I, E);
• ZeroAtInftyContinuousMap.single i x: the coordinate vector supported at i with value x, of norm ‖x‖ (ZeroAtInftyContinuousMap.norm_single), so that on an infinite index the coordinate vectors with a fixed nonzero value are not norm null (ZeroAtInftyContinuousMap.not_tendsto_single_cofinite); a finite sum of coordinate vectors at distinct coordinates has the maximum of their norms (ZeroAtInftyContinuousMap.nnnorm_sum_single), so any family supported on a finite set has norm equal to its maximum on that set (ZeroAtInftyContinuousMap.norm_eq_sup_of_forall_eq_zero);
• ZeroAtInftyContinuousMap.singleCLM R i: the isometry x ↦ single i x as a continuous linear map;
• ZeroAtInftyContinuousMap.tendsto_toWeakDual_evalCLM_cofinite: the coordinate functionals evalCLM R i of C₀(I, R) are weak-star null along the cofinite filter;
• ZeroAtInftyContinuousMap.cons: prepend one entry to a null sequence, with norm max ‖b‖ ‖f‖ (ZeroAtInftyContinuousMap.norm_cons);
• ZeroAtInftyContinuousMap.exists_norm_coe_eq_norm: the sup norm is attained at some coordinate when I is nonempty;
• ZeroAtInftyContinuousMap.hasSum_single: every f is the unconditional sum of its coordinate vectors single i (f i), and for scalar families f = ∑ i, f i • single i 1 (ZeroAtInftyContinuousMap.hasSum_smul_single_one);
• ZeroAtInftyContinuousMap.dense_setOf_finite_support and ZeroAtInftyContinuousMap.dense_span_single_one: finitely supported families are dense, and the coordinate vectors single i 1 span a dense submodule of C₀(I, R);
• ZeroAtInftyContinuousMap.linearIndependent_single_one: the coordinate vectors single i 1 are linearly independent, so over a ring with the strong rank condition a finitely generated submodule contains only finitely many of them (ZeroAtInftyContinuousMap.finite_setOf_single_one_mem);
• ZeroAtInftyContinuousMap.continuousLinearMap_ext: continuous linear maps out of C₀(I, E) are determined by their values on coordinate vectors;
• ZeroAtInftyContinuousMap.indicatorCLM R S: the coordinate projection f ↦ S.indicator f onto a set S of indices, of norm at most one; it has finite rank when S is finite and the coefficients form a finitely generated module, as on C₀(I, R) (ZeroAtInftyContinuousMap.isFiniteRank_indicatorCLM); these projections converge to the original family when every coordinate is retained eventually (ZeroAtInftyContinuousMap.tendsto_indicatorCLM).

It also compares the model spaces over different discrete index types. These isometries send coordinate vectors to coordinate vectors and commute with the coordinatewise action ZeroAtInftyContinuousMap.compLeft of a bounded coefficient map:

• ZeroAtInftyContinuousMap.sumEquiv: C₀(I ⊕ J, E) ≃ₗᵢ[R] C₀(I, E) × C₀(J, E);
• ZeroAtInftyContinuousMap.equivFunOnFintype: C₀(I, E) ≃ₗᵢ[R] (I → E) for finite I;
• ZeroAtInftyContinuousMap.curryEquiv: C₀(I × J, E) ≃ₗᵢ[R] C₀(I, C₀(J, E)).

Reindexing along an equivalence e : I ≃ J is the case e.toHomeomorphOfDiscrete of ZeroAtInftyContinuousMap.congrLeft.

None of these statements needs completeness or the ultrametric inequality. The extension of bounded families to continuous linear maps out of C₀(I, R) is developed in TauCeti.Topology.ContinuousMap.ZeroAtInfty.LinearCombination.

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.tendsto_cofinite {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap I β) : Filter.Tendsto (⇑f) Filter.cofinite (nhds 0)

A function vanishing at infinity on a discrete space tends to zero along the cofinite filter.

def ZeroAtInftyContinuousMap.mkOfDiscrete {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] (f : I → β) (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) : ZeroAtInftyContinuousMap I β

A family on a discrete space tending to zero along the cofinite filter, as a continuous function vanishing at infinity.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_mkOfDiscrete {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] (f : I → β) (hf : Filter.Tendsto f Filter.cofinite (nhds 0)) : ⇑(mkOfDiscrete f hf) = f

mkOfDiscrete f hf has underlying family f.

@[simp]

theorem ZeroAtInftyContinuousMap.mkOfDiscrete_coe {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] (f : ZeroAtInftyContinuousMap I β) : mkOfDiscrete ⇑f ⋯ = f

mkOfDiscrete recovers every function vanishing at infinity on a discrete space.

theorem ZeroAtInftyContinuousMap.tendsto_indicator_cofinite {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] (S : Set I) (f : ZeroAtInftyContinuousMap I β) : Filter.Tendsto (S.indicator ⇑f) Filter.cofinite (nhds 0)

Replacing the coordinates outside a set S by zero preserves vanishing at infinity.

def ZeroAtInftyContinuousMap.single {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i : I) (b : β) : ZeroAtInftyContinuousMap I β

The coordinate vector single i b of C₀(I, β): the family with value b at i and zero elsewhere.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_single {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i : I) (b : β) : ⇑(single i b) = Pi.single i b

single i b has underlying family Pi.single i b.

theorem ZeroAtInftyContinuousMap.single_apply {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i j : I) (b : β) : (single i b) j = if j = i then b else 0

The coordinates of single i b.

theorem ZeroAtInftyContinuousMap.single_eq_same {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i : I) (b : β) : (single i b) i = b

single i b takes the value b at i.

theorem ZeroAtInftyContinuousMap.single_eq_of_ne {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] {i j : I} (h : j ≠ i) (b : β) : (single i b) j = 0

single i b vanishes away from i.

@[simp]

theorem ZeroAtInftyContinuousMap.single_zero {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i : I) : single i 0 = 0

The coordinate vector with value zero is zero.

theorem ZeroAtInftyContinuousMap.single_injective {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] (i : I) : Function.Injective (single i)

The coordinate vector at a fixed index is injective in its entry.

@[simp]

theorem ZeroAtInftyContinuousMap.single_eq_zero_iff {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace β] [Zero β] [DecidableEq I] {i : I} {b : β} : single i b = 0 ↔ b = 0

A coordinate vector vanishes exactly when its entry does.

Prepending a coordinate to a null sequence

def ZeroAtInftyContinuousMap.cons {β : Type u_2} [TopologicalSpace β] [Zero β] (b : β) (f : ZeroAtInftyContinuousMap ℕ β) : ZeroAtInftyContinuousMap ℕ β

Prepend one entry to a sequence vanishing at infinity.

@[simp]

theorem ZeroAtInftyContinuousMap.cons_apply_zero {β : Type u_2} [TopologicalSpace β] [Zero β] (b : β) (f : ZeroAtInftyContinuousMap ℕ β) : (cons b f) 0 = b

@[simp]

theorem ZeroAtInftyContinuousMap.cons_apply_succ {β : Type u_2} [TopologicalSpace β] [Zero β] (b : β) (f : ZeroAtInftyContinuousMap ℕ β) (n : ℕ) : (cons b f) (n + 1) = f n

theorem ZeroAtInftyContinuousMap.cons_add {β : Type u_2} [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (b c : β) (f g : ZeroAtInftyContinuousMap ℕ β) : cons (b + c) (f + g) = cons b f + cons c g

Prepending entries commutes with addition.

theorem ZeroAtInftyContinuousMap.cons_smul {β : Type u_2} [TopologicalSpace β] [Zero β] {R : Type u_3} [SMulZeroClass R β] [ContinuousConstSMul R β] (r : R) (b : β) (f : ZeroAtInftyContinuousMap ℕ β) : cons (r • b) (r • f) = r • cons b f

Prepending entries commutes with scalar multiplication.

@[simp]

theorem ZeroAtInftyContinuousMap.norm_cons {β : Type u_2} [SeminormedAddCommGroup β] (b : β) (f : ZeroAtInftyContinuousMap ℕ β) : ‖cons b f‖ = max ‖b‖ ‖f‖

The norm of a sequence with a prepended entry is the maximum of the two norms.

theorem ZeroAtInftyContinuousMap.single_add {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace β] [AddZeroClass β] [ContinuousAdd β] (i : I) (b c : β) : single i (b + c) = single i b + single i c

single i is additive.

theorem ZeroAtInftyContinuousMap.single_neg {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] (i : I) (b : β) : single i (-b) = -single i b

The coordinate vector of a negation is the negated coordinate vector.

theorem ZeroAtInftyContinuousMap.single_sub {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] (i : I) (b c : β) : single i (b - c) = single i b - single i c

The coordinate vector of a difference is the difference of coordinate vectors.

theorem ZeroAtInftyContinuousMap.single_smul {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace β] {R : Type u_3} [Zero β] [SMulZeroClass R β] [ContinuousConstSMul R β] (i : I) (r : R) (b : β) : single i (r • b) = r • single i b

single i commutes with scalar multiplication.

theorem ZeroAtInftyContinuousMap.smul_single_one {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {R : Type u_3} [TopologicalSpace R] [MulZeroOneClass R] [ContinuousConstSMul R R] (i : I) (r : R) : r • single i 1 = single i r

In C₀(I, R), the coordinate vector single i r is r times the unit vector single i 1.

theorem ZeroAtInftyContinuousMap.sum_single_apply {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] (b : I → β) (s : Finset I) (j : I) : (∑ i ∈ s, single i (b i)) j = if j ∈ s then b j else 0

A finite sum of coordinate vectors agrees with the given family on the summation set and vanishes outside it.

@[simp]

theorem ZeroAtInftyContinuousMap.norm_single {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] [DecidableEq I] (i : I) (b : β) : ‖single i b‖ = ‖b‖

A coordinate vector has the norm of its nonzero entry.

noncomputable def ZeroAtInftyContinuousMap.singleCLM {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] (R : Type u_3) [Semiring R] [Module R β] [ContinuousConstSMul R β] [DecidableEq I] (i : I) : β →L[R] ZeroAtInftyContinuousMap I β

The coordinate vector map b ↦ single i b, as a continuous linear map β →L[R] C₀(I, β). It is an isometry by norm_single.

@[simp]

theorem ZeroAtInftyContinuousMap.singleCLM_apply {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] [DecidableEq I] (i : I) (b : β) : (singleCLM R i) b = single i b

Coordinate projections

noncomputable def ZeroAtInftyContinuousMap.indicatorCLM {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] (R : Type u_3) [Semiring R] [Module R β] [ContinuousConstSMul R β] (S : Set I) : ZeroAtInftyContinuousMap I β →L[R] ZeroAtInftyContinuousMap I β

The coordinate projection onto a set S of indices: the continuous linear map sending f to the family S.indicator f, which keeps the coordinates in S and replaces the others by zero. It has norm at most one (norm_indicatorCLM_apply_le), and for finite S it is the partial sum of the coordinate expansion over S (indicatorCLM_finset_apply).

@[simp]

theorem ZeroAtInftyContinuousMap.coe_indicatorCLM {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] (S : Set I) (f : ZeroAtInftyContinuousMap I β) : ⇑((indicatorCLM R S) f) = S.indicator ⇑f

theorem ZeroAtInftyContinuousMap.tendsto_indicatorCLM {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] (R : Type u_3) [Semiring R] [Module R β] [ContinuousConstSMul R β] {ι : Type u_4} {s : ι → Set I} {l : Filter ι} (hs : ∀ (i : I), ∀ᶠ (k : ι) in l, i ∈ s k) (f : ZeroAtInftyContinuousMap I β) : Filter.Tendsto (fun (k : ι) => (indicatorCLM R (s k)) f) l (nhds f)

Coordinate projections converge to a family vanishing at infinity if every coordinate is retained eventually. The sets need not be finite or increasing.

theorem ZeroAtInftyContinuousMap.norm_indicatorCLM_apply_le {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] (S : Set I) (f : ZeroAtInftyContinuousMap I β) : ‖(indicatorCLM R S) f‖ ≤ ‖f‖

The coordinate projections have norm at most one.

@[simp]

theorem ZeroAtInftyContinuousMap.indicatorCLM_univ {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] : indicatorCLM R Set.univ = ContinuousLinearMap.id R (ZeroAtInftyContinuousMap I β)

@[simp]

theorem ZeroAtInftyContinuousMap.indicatorCLM_empty {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] : indicatorCLM R ∅ = 0

theorem ZeroAtInftyContinuousMap.indicatorCLM_add_indicatorCLM_compl {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] (S : Set I) : indicatorCLM R S + indicatorCLM R Sᶜ = ContinuousLinearMap.id R (ZeroAtInftyContinuousMap I β)

The projections onto a set of indices and onto its complement add up to the identity.

theorem ZeroAtInftyContinuousMap.indicatorCLM_eq_self {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] {S : Set I} {f : ZeroAtInftyContinuousMap I β} (hf : ∀ i ∉ S, f i = 0) : (indicatorCLM R S) f = f

A coordinate projection fixes any family vanishing outside its index set.

theorem ZeroAtInftyContinuousMap.indicatorCLM_finset_apply {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] [DecidableEq I] (s : Finset I) (f : ZeroAtInftyContinuousMap I β) : (indicatorCLM R ↑s) f = ∑ i ∈ s, single i (f i)

For a finite set s, the coordinate projection onto s is the partial sum of the coordinate expansion over s.

theorem ZeroAtInftyContinuousMap.isFiniteRank_indicatorCLM {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {R : Type u_3} [Semiring R] [Module R β] [ContinuousConstSMul R β] [Module.Finite R β] (s : Finset I) : (↑(indicatorCLM R ↑s)).IsFiniteRank

The coordinate projection of C₀(I, β) onto a finite set of indices has finite rank when β is a finitely generated module, for instance on C₀(I, R): its range lies in the span of the coordinate vectors at these indices with values in a finite generating set of β.

theorem ZeroAtInftyContinuousMap.nnnorm_sum_single {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] [DecidableEq I] (s : Finset I) (b : I → β) : ‖∑ i ∈ s, single i (b i)‖₊ = s.sup fun (i : I) => ‖b i‖₊

A finite sum of coordinate vectors at distinct coordinates has the maximum of their norms as its norm; the empty sum has norm zero.

theorem ZeroAtInftyContinuousMap.nnnorm_eq_sup_of_forall_eq_zero {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {s : Finset I} {f : ZeroAtInftyContinuousMap I β} (hf : ∀ i ∉ s, f i = 0) : ‖f‖₊ = s.sup fun (i : I) => ‖f i‖₊

A family vanishing outside a finite set s has nnnorm equal to the maximum over s.

theorem ZeroAtInftyContinuousMap.norm_eq_sup_of_forall_eq_zero {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] {s : Finset I} {f : ZeroAtInftyContinuousMap I β} (hf : ∀ i ∉ s, f i = 0) : ‖f‖ = ↑(s.sup fun (i : I) => ‖f i‖₊)

A family vanishing outside a finite set s has norm equal to the maximum of its norms on s.

theorem ZeroAtInftyContinuousMap.exists_norm_coe_eq_norm {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] [Nonempty I] (f : ZeroAtInftyContinuousMap I β) : ∃ (i : I), ‖f i‖ = ‖f‖

The sup norm is attained: on a nonempty discrete index, some coordinate of f ∈ C₀(I, β) has norm ‖f‖. This covers every nonzero f, whose index type is necessarily nonempty.

theorem ZeroAtInftyContinuousMap.hasSum_single {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] [DecidableEq I] (f : ZeroAtInftyContinuousMap I β) : HasSum (fun (i : I) => single i (f i)) f

Coordinate expansion: every f ∈ C₀(I, β) is the unconditional sum of its coordinate vectors single i (f i).

theorem ZeroAtInftyContinuousMap.continuousLinearMap_ext {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] [DecidableEq I] {R : Type u_3} {M : Type u_4} [Semiring R] [Module R β] [ContinuousConstSMul R β] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [T2Space M] {φ ψ : ZeroAtInftyContinuousMap I β →L[R] M} (h : ∀ (i : I) (b : β), φ (single i b) = ψ (single i b)) : φ = ψ

Continuous linear maps out of C₀(I, β) agreeing on all coordinate vectors are equal.

theorem ZeroAtInftyContinuousMap.dense_setOf_finite_support {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedAddCommGroup β] : Dense {f : ZeroAtInftyContinuousMap I β | (Function.support ⇑f).Finite}

Finite-support density: the finitely supported families are dense in C₀(I, β).

theorem ZeroAtInftyContinuousMap.not_tendsto_single_cofinite {I : Type u_1} {β : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedAddCommGroup β] [DecidableEq I] [Infinite I] {b : β} (hb : b ≠ 0) : ¬Filter.Tendsto (fun (i : I) => single i b) Filter.cofinite (nhds 0)

On an infinite index type, the coordinate vectors single i b with a fixed nonzero value b do not tend to zero in norm along the cofinite filter. In particular the unit coordinate vectors of c₀ are not norm null.

theorem ZeroAtInftyContinuousMap.tendsto_toWeakDual_evalCLM_cofinite {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] (R : Type u_3) [SeminormedCommRing R] : Filter.Tendsto (fun (i : I) => StrongDual.toWeakDual (evalCLM R i)) Filter.cofinite (nhds 0)

The coordinate functionals of C₀(I, R) tend to zero in the weak-star topology along the cofinite filter.

theorem ZeroAtInftyContinuousMap.hasSum_smul_single_one {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_3} [SeminormedRing R] [DecidableEq I] (f : ZeroAtInftyContinuousMap I R) : HasSum (fun (i : I) => f i • single i 1) f

Coordinate expansion in the unit vectors: every f ∈ C₀(I, R) is the unconditional sum ∑ i, f i • single i 1.

theorem ZeroAtInftyContinuousMap.dense_span_single_one {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_3} [SeminormedRing R] [DecidableEq I] : Dense ↑(Submodule.span R (Set.range fun (i : I) => single i 1))

The unit vectors single i 1 span a dense submodule of C₀(I, R).

theorem ZeroAtInftyContinuousMap.linearIndependent_single_one {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_3} [SeminormedRing R] [DecidableEq I] : LinearIndependent R fun (i : I) => single i 1

The unit vectors single i 1 of C₀(I, R) are linearly independent.

theorem ZeroAtInftyContinuousMap.finite_setOf_single_one_mem {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_3} [SeminormedRing R] [DecidableEq I] [StrongRankCondition R] {Q : Submodule R (ZeroAtInftyContinuousMap I R)} (hQ : Q.FG) : {i : I | single i 1 ∈ Q}.Finite

Over a ring with the strong rank condition, a finitely generated submodule of C₀(I, R) contains only finitely many of the unit vectors single i 1.

theorem ZeroAtInftyContinuousMap.continuousLinearMap_ext_single_one {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_3} [SeminormedRing R] [DecidableEq I] {M : Type u_4} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [T2Space M] {φ ψ : ZeroAtInftyContinuousMap I R →L[R] M} (h : ∀ (i : I), φ (single i 1) = ψ (single i 1)) : φ = ψ

Continuous linear maps out of C₀(I, R) agreeing on the unit vectors single i 1 are equal.

Changes of index

@[simp]

theorem ZeroAtInftyContinuousMap.congrLeft_single {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [DecidableEq I] [DecidableEq J] (e : I ≃ₜ J) (i : I) (b : E) : (congrLeft R E e) (single i b) = single (e i) b

Reindexing sends coordinate vectors to coordinate vectors.

@[simp]

theorem ZeroAtInftyContinuousMap.compLeft_single {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Module R F] [ContinuousConstSMul R F] [DecidableEq I] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (i : I) (b : E) : (compLeft u hu) (single i b) = single i (u b)

A bounded coefficient map sends coordinate vectors to coordinate vectors.

def ZeroAtInftyContinuousMap.sumEquiv {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} (R : Type u_4) (E : Type u_5) [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] : ZeroAtInftyContinuousMap (I ⊕ J) E ≃ₗᵢ[R] ZeroAtInftyContinuousMap I E × ZeroAtInftyContinuousMap J E

Disjoint sums of index types. Restriction to the two summands identifies C₀(I ⊕ J, E) isometrically with the product C₀(I, E) × C₀(J, E), which carries the max norm.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_sumEquiv_fst {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (f : ZeroAtInftyContinuousMap (I ⊕ J) E) : ⇑((sumEquiv R E) f).1 = ⇑f ∘ Sum.inl

The first component of sumEquiv R E f is the restriction of f to the left summand.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_sumEquiv_snd {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (f : ZeroAtInftyContinuousMap (I ⊕ J) E) : ⇑((sumEquiv R E) f).2 = ⇑f ∘ Sum.inr

The second component of sumEquiv R E f is the restriction of f to the right summand.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_sumEquiv_symm {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (g : ZeroAtInftyContinuousMap I E × ZeroAtInftyContinuousMap J E) : ⇑((sumEquiv R E).symm g) = Sum.elim ⇑g.1 ⇑g.2

The inverse of sumEquiv glues the two components.

@[simp]

theorem ZeroAtInftyContinuousMap.sumEquiv_single_inl {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [DecidableEq I] [DecidableEq J] (i : I) (b : E) : (sumEquiv R E) (single (Sum.inl i) b) = (single i b, 0)

A coordinate vector on the left summand has zero right component.

@[simp]

theorem ZeroAtInftyContinuousMap.sumEquiv_single_inr {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [DecidableEq I] [DecidableEq J] (j : J) (b : E) : (sumEquiv R E) (single (Sum.inr j) b) = (0, single j b)

A coordinate vector on the right summand has zero left component.

theorem ZeroAtInftyContinuousMap.sumEquiv_compLeft {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} {F : Type u_6} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap (I ⊕ J) E) : (sumEquiv R F) ((compLeft u hu) f) = Prod.map (⇑(compLeft u hu)) (⇑(compLeft u hu)) ((sumEquiv R E) f)

Splitting a disjoint sum commutes with the coordinatewise action of a bounded coefficient map.

def ZeroAtInftyContinuousMap.equivFunOnFintype {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] (R : Type u_4) (E : Type u_5) [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Fintype I] : ZeroAtInftyContinuousMap I E ≃ₗᵢ[R] I → E

Finite blocks. For a finite index type I, every family I → E vanishes at infinity, and C₀(I, E) is isometric to the finite product I → E with its sup norm.

@[simp]

theorem ZeroAtInftyContinuousMap.equivFunOnFintype_apply {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Fintype I] (f : ZeroAtInftyContinuousMap I E) : (equivFunOnFintype R E) f = ⇑f

equivFunOnFintype R E f is the underlying family of f.

@[simp]

theorem ZeroAtInftyContinuousMap.coe_equivFunOnFintype_symm {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_4} {E : Type u_5} [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Fintype I] (g : I → E) : ⇑((equivFunOnFintype R E).symm g) = g

The inverse of equivFunOnFintype has underlying family g.

theorem ZeroAtInftyContinuousMap.equivFunOnFintype_compLeft {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {R : Type u_4} {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Module R F] [ContinuousConstSMul R F] [Fintype I] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap I E) : (equivFunOnFintype R F) ((compLeft u hu) f) = ⇑u ∘ (equivFunOnFintype R E) f

The identification of C₀(I, E) with I → E for finite I commutes with the coordinatewise action of a bounded coefficient map.

noncomputable def ZeroAtInftyContinuousMap.curryEquiv {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} (R : Type u_4) (E : Type u_5) [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] : ZeroAtInftyContinuousMap (I × J) E ≃ₗᵢ[R] ZeroAtInftyContinuousMap I (ZeroAtInftyContinuousMap J E)

Currying. A family on I × J vanishing at infinity is the same as a family on I of families on J vanishing at infinity: C₀(I × J, E) is isometric to C₀(I, C₀(J, E)) by f ↦ (i ↦ (j ↦ f (i, j))).

@[simp]

theorem ZeroAtInftyContinuousMap.curryEquiv_apply_apply {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (f : ZeroAtInftyContinuousMap (I × J) E) (i : I) (j : J) : (((curryEquiv R E) f) i) j = f (i, j)

curryEquiv R E f i j = f (i, j).

@[simp]

theorem ZeroAtInftyContinuousMap.curryEquiv_symm_apply {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] (g : ZeroAtInftyContinuousMap I (ZeroAtInftyContinuousMap J E)) (p : I × J) : ((curryEquiv R E).symm g) p = (g p.1) p.2

The inverse of curryEquiv uncurries.

@[simp]

theorem ZeroAtInftyContinuousMap.curryEquiv_single {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [Semiring R] [Module R E] [ContinuousConstSMul R E] [DecidableEq I] [DecidableEq J] (i : I) (j : J) (b : E) : (curryEquiv R E) (single (i, j) b) = single i (single j b)

Currying a coordinate vector gives a coordinate vector of coordinate vectors.

theorem ZeroAtInftyContinuousMap.curryEquiv_compLeft {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {J : Type u_3} {R : Type u_4} {E : Type u_5} {F : Type u_6} [TopologicalSpace J] [DiscreteTopology J] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Semiring R] [Module R E] [ContinuousConstSMul R E] [Module R F] [ContinuousConstSMul R F] (u : E →L[R] F) (hu : ∃ (C : ℝ), ∀ (x : E), ‖u x‖ ≤ C * ‖x‖) (f : ZeroAtInftyContinuousMap (I × J) E) : (curryEquiv R F) ((compLeft u hu) f) = (compLeft (compLeft u hu) ⋯) ((curryEquiv R E) f)

Currying commutes with the coordinatewise action of a bounded coefficient map.