Coefficient extension of operators on model spaces

A bounded unital ring homomorphism f : R →+* S extends the matrix of an operator C₀(J, R) →L[R] C₀(I, R) coefficientwise to an operator over S. Null columns and a uniform entry bound ensure that the extended matrix defines a continuous linear map. The construction respects identities, addition, scalar multiplication and composition, including composition of coefficient homomorphisms. Its matrix characterizes it uniquely. Over Tate target scalars it is Lipschitz in operator norm, so it preserves operator-norm sums and sends the closure of the polynomials in an endomorphism u into the closure of the polynomials in its extension.

The coefficient rings need not have a common ground field. Tate data on the source supplies the entry bound; the target need only be complete and ultrametric.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§2–3.

noncomputable def ContinuousLinearMap.mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : ZeroAtInftyContinuousMap J S →L[S] ZeroAtInftyContinuousMap I S

Extend the matrix coefficients of an operator along a bounded ring homomorphism. Boundedness is a proposition, so the construction is independent of its witness.

@[simp]

theorem ContinuousLinearMap.matrixCoeff_mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u.mapCoeffs f hf).matrixCoeff = u.matrixCoeff.map ⇑f

The extended operator has the coefficientwise extended matrix.

theorem ContinuousLinearMap.eq_mapCoeffs_iff {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (v : ZeroAtInftyContinuousMap J S →L[S] ZeroAtInftyContinuousMap I S) : v = u.mapCoeffs f hf ↔ v.matrixCoeff = u.matrixCoeff.map ⇑f

Matrix coefficients uniquely determine coefficient extension.

theorem ContinuousLinearMap.norm_matrixCoeff_mapCoeffs_le {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (C : NNReal) (hf : ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (i : I) (j : J) : ‖(u.mapCoeffs f ⋯).matrixCoeff i j‖ ≤ ↑C * ‖u.matrixCoeff i j‖

The norm of an extended matrix entry is bounded by the homomorphism bound times its original norm.

theorem ContinuousLinearMap.ringOpNorm_mapCoeffs_le {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (C : NNReal) (hf : ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : ‖u.mapCoeffs f ⋯‖ ≤ ↑C * ‖u‖

A norm bound for coefficient extension.

@[simp]

theorem ContinuousLinearMap.mapCoeffs_zero {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : mapCoeffs 0 f hf = 0

@[simp]

theorem ContinuousLinearMap.mapCoeffs_add {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u + v).mapCoeffs f hf = u.mapCoeffs f hf + v.mapCoeffs f hf

@[simp]

theorem ContinuousLinearMap.mapCoeffs_neg {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (-u).mapCoeffs f hf = -u.mapCoeffs f hf

@[simp]

theorem ContinuousLinearMap.mapCoeffs_sub {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u - v).mapCoeffs f hf = u.mapCoeffs f hf - v.mapCoeffs f hf

@[simp]

theorem ContinuousLinearMap.mapCoeffs_sum {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] {ι : Type u_6} (s : Finset ι) (u : ι → ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (∑ k ∈ s, u k).mapCoeffs f hf = ∑ k ∈ s, (u k).mapCoeffs f hf

@[simp]

theorem ContinuousLinearMap.mapCoeffs_smul {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (r : R) : (r • u).mapCoeffs f hf = f r • u.mapCoeffs f hf

@[simp]

theorem ContinuousLinearMap.mapCoeffs_one {I : Type u_1} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [DecidableEq I] (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : mapCoeffs 1 f hf = 1

@[simp]

theorem ContinuousLinearMap.mapCoeffs_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [TopologicalSpace K] [DiscreteTopology K] [DecidableEq K] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (v : ZeroAtInftyContinuousMap K R →L[R] ZeroAtInftyContinuousMap J R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u ∘SL v).mapCoeffs f hf = u.mapCoeffs f hf ∘SL v.mapCoeffs f hf

Coefficient extension preserves composition of operators.

@[simp]

theorem ContinuousLinearMap.mapCoeffs_mul {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u * v).mapCoeffs f hf = u.mapCoeffs f hf * v.mapCoeffs f hf

Coefficient extension is multiplicative on endomorphisms.

@[simp]

theorem ContinuousLinearMap.mapCoeffs_pow {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (n : ℕ) : (u ^ n).mapCoeffs f hf = u.mapCoeffs f hf ^ n

theorem ContinuousLinearMap.lipschitzWith_mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] (f : R →+* S) (C : NNReal) (hf : ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : LipschitzWith C fun (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) => u.mapCoeffs f ⋯

Coefficient extension along a homomorphism with bound C is C-Lipschitz in operator norm.

theorem ContinuousLinearMap.continuous_mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : Continuous fun (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) => u.mapCoeffs f hf

Coefficient extension is continuous in operator norm.

theorem HasSum.mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] {ι : Type u_6} {u : ι → ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} {v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (h : HasSum u v) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : HasSum (fun (k : ι) => (u k).mapCoeffs f hf) (v.mapCoeffs f hf)

Coefficient extension preserves operator-norm sums.

theorem ContinuousLinearMap.mapCoeffs_mem_closure_adjoin {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] {u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R} (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (hv : v ∈ closure ↑R[u]) : v.mapCoeffs f hf ∈ closure ↑S[u.mapCoeffs f hf]

Coefficient extension sends the operator-norm closure of the polynomials in u into the closure of the polynomials in the extension of u.

@[simp]

theorem ContinuousLinearMap.mapCoeffs_id {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [IsUltrametricDist R] [CompleteSpace R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (hf : ∃ (C : NNReal), ∀ (r : R), ‖(RingHom.id R) r‖ ≤ ↑C * ‖r‖) : u.mapCoeffs (RingHom.id R) hf = u

Extension along the identity homomorphism is the original operator.

theorem ContinuousLinearMap.mapCoeffs_mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [NormedCommRing S] [IsUltrametricDist S] [CompleteSpace S] [TauCeti.NormedRing.IsTate S] {T : Type u_6} [NormedCommRing T] [IsUltrametricDist T] [CompleteSpace T] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (f : R →+* S) (g : S →+* T) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) (hg : ∃ (D : NNReal), ∀ (s : S), ‖g s‖ ≤ ↑D * ‖s‖) (hgf : ∃ (E : NNReal), ∀ (r : R), ‖(g.comp f) r‖ ≤ ↑E * ‖r‖) : (u.mapCoeffs f hf).mapCoeffs g hg = u.mapCoeffs (g.comp f) hgf

Successive coefficient extensions agree with extension along the composite homomorphism.