Row compactness under coefficient extension

Extending an operator on C₀ along a bounded unital coefficient homomorphism multiplies each row norm by at most the homomorphism bound and preserves row compactness.

References

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

theorem ContinuousLinearMap.rowNorm_mapCoeffs_le {I : Type u_1} {J : Type u_2} {R : Type u_3} {S : Type u_4} [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) : (u.mapCoeffs f ⋯).rowNorm i ≤ ↑C * u.rowNorm i

Coefficient extension multiplies each row norm by at most the homomorphism bound.

theorem ContinuousLinearMap.IsRowCompact.mapCoeffs {I : Type u_1} {J : Type u_2} {R : Type u_3} {S : Type u_4} [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} (hu : u.IsRowCompact) (f : R →+* S) (hf : ∃ (C : NNReal), ∀ (r : R), ‖f r‖ ≤ ↑C * ‖r‖) : (u.mapCoeffs f hf).IsRowCompact

Row compactness is preserved by bounded coefficient extension.