Uniform boundedness over Tate rings #
Mathlib proves the Banach–Steinhaus theorem (banach_steinhaus) for continuous semilinear maps
over a nontrivially normed field via barrelled locally convex spaces. For modules over a general
Tate normed ring (TauCeti.NormedRing.IsTate), the locally convex machinery does not apply,
because the scalar ring need not be a field. Instead, the Baire category theorem on the complete
pseudometrizable domain produces an open ball on which the family is uniformly bounded by an
integer constant, and rescaling into that ball by powers of a multiplicative pseudo-uniformiser
converts that local constant bound into a global operator-norm bound.
This file establishes:
- the Banach–Steinhaus theorem (
TauCeti.NormedRing.IsTate.banach_steinhaus) for pointwise bounded families of continuous linear maps from a complete seminormed module over a Tate ring; - continuity and operator-norm bounds for pointwise limits of continuous linear maps along a
filter (
LinearMap.continuous_of_tendsto_of_pointwise_bounded,LinearMap.continuous_of_tendsto_of_isCountablyGenerated,ContinuousLinearMap.ofTendstoOfPointwiseBounded,ContinuousLinearMap.ofTendstoOfIsCountablyGenerated, andContinuousLinearMap.ringOpNorm_le_of_tendsto).
No commutativity or ultrametric hypothesis on the Tate ring is required in this file.
Main results #
TauCeti.NormedRing.IsTate.banach_steinhaus: a pointwise bounded family of continuous linear maps from a complete seminormed module over a Tate ring is uniformly bounded in operator norm.ContinuousLinearMap.ofTendstoOfPointwiseBounded,ContinuousLinearMap.ofTendstoOfIsCountablyGenerated: pointwise limits of continuous linear maps from a complete seminormed module over a Tate ring are continuous linear maps when the family is pointwise bounded or the filter is countably generated (in particular, for sequences).
The pointwise-limit constructors follow continuousLinearMapOfTendsto in
Mathlib/Analysis/LocallyConvex/Barrelled.lean and
ContinuousLinearMap.ofTendstoOfBoundedRange in
Mathlib/Analysis/Normed/Operator/Completeness.lean, using linearMapOfTendsto and a
uniform-boundedness continuity proof.
References #
- K. Buzzard, The Analytic Continuation of p-adic Modular Forms (eigenbook), §2.
- C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
- P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, Proposition 6.2.
Banach–Steinhaus theorem (Uniform Boundedness Principle) over a Tate ring.
If a family g : ι → E →L[R] F of continuous linear maps from a complete seminormed module E
over a Tate ring R is pointwise bounded, then the operator norms ‖g i‖ are uniformly
bounded.
Pointwise form of TauCeti.NormedRing.IsTate.banach_steinhaus: a pointwise bounded family of
continuous linear maps from a complete seminormed module over a Tate ring satisfies a uniform
linear bound ‖g i x‖ ≤ C * ‖x‖ with C > 0.
If a family g : α → E →L[R] F of continuous linear maps on a complete seminormed module over
a Tate ring is pointwise bounded and converges pointwise along a nontrivial filter l to a linear
map f, then f is continuous.
If a family g : α → E →L[R] F of continuous linear maps on a complete seminormed module over
a Tate ring converges pointwise along a countably generated nontrivial filter l (for instance, a
sequence along atTop) to a linear map f, then f is continuous.
If a family g : α → E →L[R] F converges pointwise to f : E →L[R] F along a nontrivial
filter l and eventually satisfies ‖g a‖ ≤ C, then ‖f‖ ≤ C.
Construct a bundled continuous linear map from the pointwise limit of a pointwise bounded family of continuous linear maps on a complete seminormed module over a Tate ring.
Instances For
Construct a bundled continuous linear map from the pointwise limit along a countably generated nontrivial filter (in particular, a pointwise convergent sequence) of continuous linear maps on a complete seminormed module over a Tate ring.