Potentially orthonormalisable modules and property (Pr)

Let R be a normed ring. Besides the orthonormalisable modules TauCeti.IsONable R M, linearly isometric to a model space C₀(I, R), nonarchimedean functional analysis uses two weaker conditions which only see the topology of M:

• TauCeti.IsPotentiallyONable R M: M is continuously linearly equivalent to some C₀(I, R);
• TauCeti.HasPr R M (property (Pr)): M is a continuous linear retract of some C₀(I, R), that is, there are continuous linear maps i : M →L[R] C₀(I, R) and r : C₀(I, R) →L[R] M with r ∘ i = id. Then C₀(I, R) is the topological direct sum of the range of i and the kernel of r, so this is the condition that M is a topological direct summand of a model space; Buzzard defines property (Pr) equivalently by a direct sum M × Q being potentially orthonormalisable.

Then IsONable R M → IsPotentiallyONable R M → HasPr R M. Both new conditions are invariant under continuous linear equivalence, stable under finite products (using C₀(I ⊕ J, R) ≃ C₀(I, R) × C₀(J, R)), and (Pr) passes to continuous linear retracts.

Over a ring with a multiplicative pseudo-uniformiser (TauCeti.NormedRing.IsTate R), property (Pr) is the analytic analogue of projectivity:

• TauCeti.HasPr.lifting_property: every continuous linear map f : M →L[R] F out of a module with (Pr) lifts through every continuous linear surjection q : E →L[R] F from a complete ultrametric module onto a complete module. The lift is built from bounded lifts of the images of the coordinate vectors, which exist by the quantitative open mapping theorem.
• TauCeti.hasPr_iff_forall_exists_comp_eq_id: over a complete ultrametric such ring, a complete ultrametric module has (Pr) exactly when every continuous linear surjection onto it from a complete ultrametric module in Type (max u v) has a continuous linear section. For the converse, the vectors of norm at most one are the coordinate images of a surjection from a model space onto M.
• TauCeti.HasPr.projective: a finitely generated module with (Pr) is a continuous linear retract of some R ^ n (TauCeti.HasPr.exists_comp_eq_id_of_finite), so it is projective. It is complete by TauCeti.HasPr.completeSpace, since over a complete ring a retract of C₀(I, R) is complete.

References

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

def TauCeti.IsPotentiallyONable (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : Prop

A normed module is potentially orthonormalisable if it is continuously linearly equivalent to a model space C₀(I, R) of families on a discrete index type tending to zero along the cofinite filter.

theorem TauCeti.isPotentiallyONable_def (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : IsPotentiallyONable R M ↔ ∃ (I : Type u) (x : TopologicalSpace I) (_ : DiscreteTopology I), Nonempty (M ≃L[R] ZeroAtInftyContinuousMap I R)

A module is potentially orthonormalisable exactly when it is continuously linearly equivalent to C₀(I, R) for some discrete index type I. This is the introduction and elimination interface for IsPotentiallyONable.

def TauCeti.HasPr (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : Prop

A normed module has property (Pr) if it is a continuous linear retract of a model space C₀(I, R): there are continuous linear maps i : M →L[R] C₀(I, R) and r : C₀(I, R) →L[R] M with r ∘ i = id.

theorem TauCeti.hasPr_def (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : HasPr R M ↔ ∃ (I : Type u) (x : TopologicalSpace I) (_ : DiscreteTopology I) (i : M →L[R] ZeroAtInftyContinuousMap I R) (r : ZeroAtInftyContinuousMap I R →L[R] M), r ∘SL i = ContinuousLinearMap.id R M

A module has property (Pr) exactly when it is a continuous linear retract of C₀(I, R) for some discrete index type I. This is the introduction and elimination interface for HasPr.

theorem TauCeti.IsONable.isPotentiallyONable {R : Type v} [SeminormedRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] (h : IsONable R M) : IsPotentiallyONable R M

An orthonormalisable module is potentially orthonormalisable.

theorem TauCeti.IsPotentiallyONable.hasPr {R : Type v} [SeminormedRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] (h : IsPotentiallyONable R M) : HasPr R M

A potentially orthonormalisable module has property (Pr).

theorem TauCeti.IsPotentiallyONable.of_equiv {R : Type v} [SeminormedRing R] {M N : Type u} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (h : IsPotentiallyONable R N) (e : M ≃L[R] N) : IsPotentiallyONable R M

Potential orthonormalisability is invariant under continuous linear equivalence.

theorem TauCeti.HasPr.of_retract {R : Type v} [SeminormedRing R] {M N : Type u} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (h : HasPr R N) (i : M →L[R] N) (r : N →L[R] M) (hri : r ∘SL i = ContinuousLinearMap.id R M) : HasPr R M

A continuous linear retract of a module with property (Pr) has property (Pr).

theorem TauCeti.HasPr.of_equiv {R : Type v} [SeminormedRing R] {M N : Type u} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (h : HasPr R N) (e : M ≃L[R] N) : HasPr R M

Property (Pr) is invariant under continuous linear equivalence.

theorem TauCeti.IsPotentiallyONable.prod {R : Type v} [SeminormedRing R] {M N : Type u} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (hM : IsPotentiallyONable R M) (hN : IsPotentiallyONable R N) : IsPotentiallyONable R (M × N)

A finite product of potentially orthonormalisable modules is potentially orthonormalisable.

theorem TauCeti.HasPr.prod {R : Type v} [SeminormedRing R] {M N : Type u} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (hM : HasPr R M) (hN : HasPr R N) : HasPr R (M × N)

A finite product of modules with property (Pr) has property (Pr).

theorem TauCeti.HasPr.completeSpace {R : Type v} [SeminormedRing R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] [CompleteSpace R] (h : HasPr R M) : CompleteSpace M

Over a complete ring, a module with property (Pr) is complete: a Cauchy filter on M maps to a Cauchy filter on the complete model space C₀(I, R), whose limit the retraction sends to a limit of the original filter.

theorem TauCeti.HasPr.lifting_property {R : Type v} [SeminormedRing R] [NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] [NormedAddCommGroup F] [Module R F] [IsBoundedSMul R F] [CompleteSpace F] (h : HasPr R M) (q : E →L[R] F) (f : M →L[R] F) (hq : Function.Surjective ⇑q) : ∃ (g : M →L[R] E), q ∘SL g = f

Lifting property of (Pr) modules: over a ring with a multiplicative pseudo-uniformiser, every continuous linear map f : M →L[R] F out of a module with property (Pr) lifts through every continuous linear surjection q : E →L[R] F from a complete ultrametric module onto a complete module: there is g : M →L[R] E with q ∘ g = f.

theorem TauCeti.hasPr_iff_forall_exists_comp_eq_id {R : Type v} [NormedRing R] [NormedRing.IsTate R] [IsUltrametricDist R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [CompleteSpace M] [IsUltrametricDist M] : HasPr R M ↔ ∀ (E : Type (max u v)) [inst : NormedAddCommGroup E] [inst_1 : Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (q : E →L[R] M), Function.Surjective ⇑q → ∃ (s : M →L[R] E), q ∘SL s = ContinuousLinearMap.id R M

Property (Pr) is the splitting of surjections: over a complete ultrametric ring with a multiplicative pseudo-uniformiser, a complete ultrametric module M has property (Pr) exactly when every continuous linear surjection q : E →L[R] M from a complete ultrametric module E in Type (max u v) has a continuous linear section. This universe suffices because the converse only uses the model space C₀({x : M // ‖x‖ ≤ 1}, R); for sources in arbitrary universes, the forward direction is HasPr.lifting_property.

theorem TauCeti.HasPr.exists_comp_eq_id_of_finite {R : Type v} [NormedRing R] [NormedRing.IsTate R] [IsUltrametricDist R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [Module.Finite R M] (h : HasPr R M) : ∃ (n : ℕ) (i : M →L[R] Fin n → R) (r : (Fin n → R) →L[R] M), r ∘SL i = ContinuousLinearMap.id R M

Finite (Pr) modules are retracts of finite free modules: over a complete ultrametric ring with a multiplicative pseudo-uniformiser, a finitely generated module M with property (Pr) is a continuous linear retract r ∘ i = id of R ^ n for some n.

theorem TauCeti.HasPr.projective {R : Type v} [NormedRing R] [NormedRing.IsTate R] [IsUltrametricDist R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [Module.Finite R M] (h : HasPr R M) : Module.Projective R M

Finite (Pr) modules are projective: over a complete ultrametric ring with a multiplicative pseudo-uniformiser, a finitely generated module with property (Pr) is a projective module.