Serre's theorem: orthonormal bases are lifts of residue bases

Let R be an ultrametric seminormed commutative ring with a multiplicative pseudo-uniformiser ϖ, and let M be an ultrametric seminormed R-module with contractive scalar action. Suppose that the norms of R and of M take their values in ‖ϖ‖ ^ ℤ ∪ {0}; this is the condition zpowCeil ‖ϖ‖ ‖x‖ = ‖x‖ of TauCeti.zpowCeil. When the norm of R satisfies it, rounding the norm of a module up (TauCeti.zpowCeilAddGroupNorm) gives a bounded-equivalent norm satisfying it as well. Write R⁰ and M⁰ for the closed unit balls, R~ = R⁰ ⧸ R⁰⁰ for the residue ring and M~ = TauCeti.ResidueModule R M for the residue module. Under the condition on the norms, R⁰⁰ • M⁰ = ϖM⁰ is the open unit ball of M (TauCeti.mem_unitBallIdeal_smul_top_iff), and likewise R⁰⁰ = ϖR⁰, so that R~ = R⁰ ⧸ ϖR⁰ and M~ = M⁰ ⧸ ϖM⁰.

Serre's theorem compares orthonormal families of M with bases of M~. For a family e : I → M⁰ with residues ē i = ResidueModule.mk (e i):

• e is orthonormal exactly when the residues ē are linearly independent over R~ (TauCeti.ResidueModule.linearIndependent_mk_iff). Orthonormal families always have independent residues, without the condition on the norms.
• if the residues span M~, then e has dense span (TauCeti.ResidueModule.dense_span_of_span_mk_eq_top). The proof is successive approximation: a vector of M⁰ agrees with a combination of the e i modulo ϖM⁰, the error is ϖ times a vector of M⁰, and iterating approximates the vector modulo ϖ ^ k M⁰ for every k. For an orthonormal family the converse holds, without the condition on the norms (TauCeti.ResidueModule.span_mk_eq_top_of_isOrthonormalFamily), so that the two are equivalent (TauCeti.ResidueModule.span_mk_eq_top_iff).

Thus e is an orthonormal basis exactly when ē is a basis of M~ (TauCeti.ResidueModule.isOrthonormalBasis_iff); the residues of an orthonormal basis form a basis without the condition on the norms (TauCeti.ResidueModule.linearIndependent_mk_and_span_mk_eq_top), and in particular any lift of a basis of M~ to M⁰ is an orthonormal basis of M (TauCeti.ResidueModule.isOrthonormalBasis_of_basis). No completeness is needed for these statements. Over a complete ring and for a complete module, where orthonormal bases are the same as linear isometries with model spaces C₀(I, R), this shows that M is orthonormalisable exactly when its residue module is free (TauCeti.isONable_iff_free_residueModule).

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §1.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
• K. Buzzard, Eigenvarieties, in L-functions and Galois Representations, LMS Lecture Note Series 320 (2007), §2.

theorem TauCeti.ResidueModule.linearIndependent_mk_of_isOrthonormalFamily {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] {e : I → ↥(unitClosedBallSubmodule R M)} (he : IsOrthonormalFamily R fun (i : I) => ↑(e i)) : LinearIndependent (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (⇑mk ∘ e)

Orthonormal families have independent residues.

theorem TauCeti.ResidueModule.linearIndependent_mk_iff {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) (hR : ∀ (a : R), zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) {e : I → ↥(unitClosedBallSubmodule R M)} : LinearIndependent (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (⇑mk ∘ e) ↔ IsOrthonormalFamily R fun (i : I) => ↑(e i)

Serre: orthonormality is independence of the residues. For norms with values in ‖ϖ‖ ^ ℤ ∪ {0}, a family of the closed unit ball is orthonormal exactly when its residues are linearly independent over the residue ring.

theorem TauCeti.ResidueModule.dense_span_of_span_mk_eq_top {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) {e : I → ↥(unitClosedBallSubmodule R M)} (hspan : Submodule.span (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (Set.range (⇑mk ∘ e)) = ⊤) : Dense ↑(Submodule.span R (Set.range fun (i : I) => ↑(e i)))

Lifts of a spanning family of residues have dense span. If the residues of a family of the closed unit ball span the residue module, for a norm with values in ‖ϖ‖ ^ ℤ ∪ {0}, then the family spans a dense submodule.

theorem TauCeti.ResidueModule.span_mk_eq_top_of_isOrthonormalFamily {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) {e : I → ↥(unitClosedBallSubmodule R M)} (he : IsOrthonormalFamily R fun (i : I) => ↑(e i)) (hdense : Dense ↑(Submodule.span R (Set.range fun (i : I) => ↑(e i)))) : Submodule.span (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (Set.range (⇑mk ∘ e)) = ⊤

Orthonormal families with dense span have spanning residues. If an orthonormal family of the closed unit ball has dense span, then its residues span the residue module. This needs only a multiplicative pseudo-uniformiser ϖ, with no condition on the values of the norms.

theorem TauCeti.ResidueModule.span_mk_eq_top_iff {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) {e : I → ↥(unitClosedBallSubmodule R M)} (he : IsOrthonormalFamily R fun (i : I) => ↑(e i)) : Submodule.span (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (Set.range (⇑mk ∘ e)) = ⊤ ↔ Dense ↑(Submodule.span R (Set.range fun (i : I) => ↑(e i)))

Serre: dense span is spanning residues. An orthonormal family of the closed unit ball has dense span exactly when its residues span the residue module, for a norm with values in ‖ϖ‖ ^ ℤ ∪ {0}.

theorem TauCeti.ResidueModule.linearIndependent_mk_and_span_mk_eq_top {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) {e : I → ↥(unitClosedBallSubmodule R M)} (he : IsOrthonormalBasis R fun (i : I) => ↑(e i)) : LinearIndependent (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (⇑mk ∘ e) ∧ Submodule.span (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (Set.range (⇑mk ∘ e)) = ⊤

Orthonormal bases have residues forming a basis. The residues of an orthonormal basis of the closed unit ball are linearly independent over the residue ring and span the residue module. This needs only a multiplicative pseudo-uniformiser ϖ, with no condition on the values of the norms.

theorem TauCeti.ResidueModule.isOrthonormalBasis_iff {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) (hR : ∀ (a : R), zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) {e : I → ↥(unitClosedBallSubmodule R M)} : (IsOrthonormalBasis R fun (i : I) => ↑(e i)) ↔ LinearIndependent (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (⇑mk ∘ e) ∧ Submodule.span (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (Set.range (⇑mk ∘ e)) = ⊤

Serre's theorem. For norms with values in ‖ϖ‖ ^ ℤ ∪ {0}, a family of the closed unit ball is an orthonormal basis exactly when its residues are a basis of the residue module: they are linearly independent over the residue ring and span.

theorem TauCeti.ResidueModule.isOrthonormalBasis_of_basis {R : Type u_1} {M : Type u_2} {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [SeminormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] (ϖ : NormedRing.PseudoUniformizer R) (hR : ∀ (a : R), zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) (b : Module.Basis I (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (ResidueModule R M)) {e : I → ↥(unitClosedBallSubmodule R M)} (he : ∀ (i : I), mk (e i) = b i) : IsOrthonormalBasis R fun (i : I) => ↑(e i)

Lifts of a residue basis are an orthonormal basis. For norms with values in ‖ϖ‖ ^ ℤ ∪ {0}, any family of the closed unit ball whose residues form a basis b of the residue module is an orthonormal basis.

theorem TauCeti.isONable_iff_free_residueModule {R : Type u_4} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [IsUltrametricDist M] [Module R M] [IsBoundedSMul R M] [CompleteSpace M] (ϖ : NormedRing.PseudoUniformizer R) (hR : ∀ (a : R), zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖) (hM : ∀ (m : M), zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) : IsONable R M ↔ Module.Free (↥(Subring.unitClosedBall R) ⧸ unitBallIdeal R) (ResidueModule R M)

Serre's criterion for orthonormalisability. Over a complete ultrametric normed commutative ring with a multiplicative pseudo-uniformiser ϖ, let M be a complete ultrametric module with contractive scalar action. If the norms of the ring and of M take their values in ‖ϖ‖ ^ ℤ ∪ {0}, then M is orthonormalisable exactly when its residue module is free over the residue ring.