The Banach module and Banach ring of operators over Tate scalars #

Let R be a seminormed ring admitting a multiplicative pseudo-uniformiser (TauCeti.NormedRing.IsTate R), and let E, F be seminormed R-modules with contractive scalar actions. Over such scalars every continuous linear map has a uniform bound, so the operator norm ContinuousLinearMap.ringOpNorm of TauCeti/Analysis/Normed/Operator/RingOpNorm.lean satisfies the usual laws. This file installs the resulting structures on E →L[R] F as scoped instances in the scope TauCeti.RingOpNorm:

E →L[R] F is a seminormed group, normed when F is, and ultrametric when F is;
scalar actions on F commuting with R act contractively on E →L[R] F; in particular E →L[R] F is an R-module with contractive action when R is commutative;
evaluation (f, x) ↦ f x is jointly continuous;
E →L[R] F is complete when F is a complete normed group;
the endomorphisms E →L[R] E form a seminormed ring, normed when E is, with ‖1‖ = 1 as soon as E has a vector of nonzero norm, and composition is jointly continuous, so that they form a topological ring; scalars move out of either factor of a composition when R is commutative;
E →L[R] F is Hausdorff when F is normed.

Mathlib's topology of bounded convergence on continuous linear maps is only defined over normed fields, so over other scalar rings these instances introduce no diamond. Over a nontrivially normed field the scoped normed group structure equals Mathlib's (TauCeti.RingOpNorm.seminormedAddCommGroup_eq), but not definitionally, so the scope should not be opened there. On the zero module every operator has norm zero (norm_of_subsingleton).

For a complete normed R-module E, the endomorphism ring is a Banach ring, so Neumann inversion applies: for ‖t‖ < 1 the operator 1 - t is invertible with inverse the Neumann series ∑ tⁿ. This is packaged as the continuous linear automorphism ContinuousLinearMap.oneSub t ht. When E is ultrametric, 1 - t and its inverse are isometries, so the inverse has operator norm one on a module with a vector of nonzero norm.

Main definitions #

TauCeti.RingOpNorm.seminormedAddCommGroup, TauCeti.RingOpNorm.normedAddCommGroup, TauCeti.RingOpNorm.seminormedRing, TauCeti.RingOpNorm.normedRing: the scoped operator-norm structures.
ContinuousLinearMap.oneSub t ht: the automorphism 1 - t of a complete normed module over Tate scalars, for ‖t‖ < 1.

Main results #

TauCeti.RingOpNorm.completeSpace: the operator space is complete when the target is.
TauCeti.RingOpNorm.isUltrametricDist: the operator norm is ultrametric when the target is.
ContinuousLinearMap.lipschitzWith_comp_comp: composition X ↦ g ∘ X ∘ f with fixed operators is Lipschitz with constant ‖g‖ * ‖f‖.
ContinuousLinearMap.apply_comp_apply_of_mem_closure_adjoin, ContinuousLinearMap.comp_comp_mem_closure_adjoin: for a retract r ∘ i = id, operator-norm limits of polynomials in the extension i ∘ u ∘ r commute with i ∘ r and compress to limits of polynomials in u.
ContinuousLinearMap.coe_oneSub_symm: the inverse of 1 - t is Ring.inverse (1 - t), the sum of the Neumann series.
ContinuousLinearMap.norm_oneSub_apply, ContinuousLinearMap.norm_oneSub_symm_apply and ContinuousLinearMap.ringOpNorm_oneSub_symm: in the ultrametric case 1 - t and its inverse preserve norms, and the inverse has operator norm one (the Neumann estimate TauCeti.norm_inverse_one_sub in the Banach ring of operators).

References #

C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §3.

The completeness proof follows Mathlib's ContinuousLinearMap.ofTendstoOfBoundedRange and ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq in Mathlib/Analysis/Normed/Operator/Completeness.lean.