Row-compact maps between modules with property (Pr)

A module M over a normed ring R has property (Pr) (TauCeti.HasPr R M) if it is a continuous linear retract M →ⁱ C₀(J, R) →ʳ M, r ∘ i = id, of a model space. A continuous linear map u : M →L[R] N between two such modules is row compact in the sense of (Pr) modules (ContinuousLinearMap.IsPrCompact) if for some retract presentations (iM, rM) of M and (iN, rN) of N the extension iN ∘ u ∘ rM : C₀(J, R) →L[R] C₀(I, R) is row compact (ContinuousLinearMap.IsRowCompact). This extends row compactness from model spaces to their continuous linear retracts, without choosing an orthonormal basis of M or N.

Over ultrametric Tate scalars the condition does not depend on the presentations. If iN ∘ u ∘ rM is row compact and j : N →L[R] C₀(I', R), s : C₀(J', R) →L[R] M are any continuous linear maps, then j ∘ u ∘ s is the composite (j ∘ rN) ∘ (iN ∘ u ∘ rM) ∘ (iM ∘ s), which is row compact because row-compact maps form a two-sided operator ideal (ContinuousLinearMap.isRowCompact_comp_of_retract). No finite-dimensional complement of the range of iM is presumed.

The ideal, closedness and approximation properties of row-compact maps transport to (Pr) modules. Over complete ultrametric Tate scalars, let M be a normed module with a bounded scalar action (IsBoundedSMul). If M is finitely generated with (Pr), every map into M from a module with (Pr) is row compact. The identity of M is row compact exactly when M has (Pr) and is finitely generated. Hence a row-compact endomorphism u of M with (1 - u) ^ n = 0 forces M to be finitely generated projective.

A row-compact idempotent e of a module with (Pr) has finitely generated projective range: through a retract presentation r ∘ i = id, the inclusion i identifies range e with the range of the row-compact idempotent i ∘ e ∘ r of the model space (ContinuousLinearMap.IsRowCompact.projective_range_of_isIdempotentElem).

Main definitions

• ContinuousLinearMap.IsPrCompact: row compactness of a map between modules with property (Pr), through retract presentations.

Main results

• ContinuousLinearMap.IsPrCompact.isRowCompact_comp: for a row-compact u : M →L[R] N, every composite j ∘ u ∘ s with model spaces is row compact; in particular the extension through any presentation is.
• ContinuousLinearMap.isPrCompact_iff_isRowCompact_comp: independence of the presentation.
• ContinuousLinearMap.isPrCompact_iff_isRowCompact: on model spaces the notion is row compactness.
• ContinuousLinearMap.IsPrCompact.comp_clm, ContinuousLinearMap.IsPrCompact.clm_comp, ContinuousLinearMap.isPrCompact_of_tendsto: the closed operator ideal property.
• ContinuousLinearMap.IsPrCompact.aeval: polynomials with zero constant coefficient preserve row compactness.
• ContinuousLinearMap.IsPrCompact.tendsto_ringOpNorm_comp_indicatorCLM_comp_sub: a row-compact map is the operator-norm limit of its truncations rN ∘ π_S ∘ iN ∘ u through any presentation of the target.
• ContinuousLinearMap.IsPrCompact.isCompletelyContinuous: row-compact maps are completely continuous.
• ContinuousLinearMap.isPrCompact_id_iff: the identity is row compact exactly on finitely generated modules with property (Pr).
• ContinuousLinearMap.IsPrCompact.projective_of_one_sub_pow_eq_zero: a row-compact u with (1 - u) ^ n = 0 forces the module to be finitely generated projective.
• ContinuousLinearMap.IsPrCompact.finite_range_of_isIdempotentElem, ContinuousLinearMap.IsPrCompact.projective_range_of_isIdempotentElem: a row-compact idempotent has finitely generated projective range.

References

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

def ContinuousLinearMap.IsPrCompact {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (u : M →L[R] N) : Prop

A continuous linear map u : M →L[R] N between modules with property (Pr) is row compact if there are continuous linear retract presentations rM ∘ iM = id of M through C₀(J, R) and rN ∘ iN = id of N through C₀(I, R) such that the extension iN ∘ u ∘ rM is row compact. Over ultrametric Tate scalars this does not depend on the presentations (ContinuousLinearMap.isPrCompact_iff_isRowCompact_comp). The index types live in the universes of M and N, as in TauCeti.HasPr.

theorem ContinuousLinearMap.isPrCompact_def {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] (u : M →L[R] N) : u.IsPrCompact ↔ ∃ (J : Type u) (x : TopologicalSpace J) (x_1 : DiscreteTopology J) (x_2 : DecidableEq J) (I : Type v) (x_3 : TopologicalSpace I) (_ : DiscreteTopology I) (iM : M →L[R] ZeroAtInftyContinuousMap J R) (rM : ZeroAtInftyContinuousMap J R →L[R] M) (iN : N →L[R] ZeroAtInftyContinuousMap I R) (rN : ZeroAtInftyContinuousMap I R →L[R] N), rM ∘SL iM = ContinuousLinearMap.id R M ∧ rN ∘SL iN = ContinuousLinearMap.id R N ∧ (iN ∘SL u ∘SL rM).IsRowCompact

A map is row compact in the sense of (Pr) modules exactly when it has row-compact extensions through some retract presentations of its source and target. This is the introduction and elimination interface for ContinuousLinearMap.IsPrCompact.

theorem ContinuousLinearMap.comp_comp_comp_of_retract {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {J : Type u_1} [TopologicalSpace J] {I : Type u_2} [TopologicalSpace I] {iM : M →L[R] ZeroAtInftyContinuousMap J R} {rM : ZeroAtInftyContinuousMap J R →L[R] M} {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hM : rM ∘SL iM = ContinuousLinearMap.id R M) (hN : rN ∘SL iN = ContinuousLinearMap.id R N) (u : M →L[R] N) : rN ∘SL (iN ∘SL u ∘SL rM) ∘SL iM = u

Retract factorisation: if rM ∘ iM = id and rN ∘ iN = id present the source and target of u, then u factors through its extension as rN ∘ (iN ∘ u ∘ rM) ∘ iM.

theorem ContinuousLinearMap.isPrCompact_of_isRowCompact_comp {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {J : Type u} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {I : Type v} [TopologicalSpace I] [DiscreteTopology I] {iM : M →L[R] ZeroAtInftyContinuousMap J R} {rM : ZeroAtInftyContinuousMap J R →L[R] M} {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hM : rM ∘SL iM = ContinuousLinearMap.id R M) (hN : rN ∘SL iN = ContinuousLinearMap.id R N) {u : M →L[R] N} (hu : (iN ∘SL u ∘SL rM).IsRowCompact) : u.IsPrCompact

A map whose extension through retract presentations of its source and target is row compact is row compact in the sense of (Pr) modules.

theorem ContinuousLinearMap.IsPrCompact.hasPr_source {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) : TauCeti.HasPr R M

The source of a row-compact map between (Pr) modules has property (Pr).

theorem ContinuousLinearMap.IsPrCompact.hasPr_target {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) : TauCeti.HasPr R N

The target of a row-compact map between (Pr) modules has property (Pr).

@[simp]

theorem ContinuousLinearMap.isPrCompact_zero_iff {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] : IsPrCompact 0 ↔ TauCeti.HasPr R M ∧ TauCeti.HasPr R N

The zero map between two modules is row compact exactly when both have property (Pr).

theorem ContinuousLinearMap.IsPrCompact.neg {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) : (-u).IsPrCompact

Negatives of row-compact maps between (Pr) modules are row compact.

@[simp]

theorem ContinuousLinearMap.isPrCompact_neg_iff {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} : (-u).IsPrCompact ↔ u.IsPrCompact

A negative is row compact between (Pr) modules exactly when the map is.

theorem ContinuousLinearMap.isPrCompact_of_finite_retract {R : Type w} [SeminormedRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [TauCeti.NormedRing.IsTate R] {I : Type v} [TopologicalSpace I] [DiscreteTopology I] [Finite I] {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hN : rN ∘SL iN = ContinuousLinearMap.id R N) (hM : TauCeti.HasPr R M) (u : M →L[R] N) : u.IsPrCompact

Over Tate scalars, every map into a retract of a model space with a finite index type is row compact, provided its source has property (Pr).

theorem ContinuousLinearMap.IsPrCompact.smul {R : Type w} [SeminormedCommRing R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [ContinuousConstSMul R N] {u : M →L[R] N} (hu : u.IsPrCompact) (c : R) : (c • u).IsPrCompact

Scalar multiples of row-compact maps between (Pr) modules are row compact.

theorem ContinuousLinearMap.isRowCompact_comp_of_retract {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {J : Type u_3} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {I : Type u_4} [TopologicalSpace I] [DiscreteTopology I] {iM : M →L[R] ZeroAtInftyContinuousMap J R} {rM : ZeroAtInftyContinuousMap J R →L[R] M} {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hM : rM ∘SL iM = ContinuousLinearMap.id R M) (hN : rN ∘SL iN = ContinuousLinearMap.id R N) {u : M →L[R] N} (hu : (iN ∘SL u ∘SL rM).IsRowCompact) {J' : Type u_5} {I' : Type u_6} [TopologicalSpace J'] [DiscreteTopology J'] [DecidableEq J'] [TopologicalSpace I'] [DiscreteTopology I'] (j : N →L[R] ZeroAtInftyContinuousMap I' R) (s : ZeroAtInftyContinuousMap J' R →L[R] M) : (j ∘SL u ∘SL s).IsRowCompact

Independence of the presentation. Over ultrametric Tate scalars, if the extension iN ∘ u ∘ rM of u through retract presentations of its source and target is row compact, then so is every composite j ∘ u ∘ s with continuous linear maps j into and s out of model spaces: it factors as (j ∘ rN) ∘ (iN ∘ u ∘ rM) ∘ (iM ∘ s).

theorem ContinuousLinearMap.IsPrCompact.isRowCompact_comp {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) {J' : Type u_3} {I' : Type u_4} [TopologicalSpace J'] [DiscreteTopology J'] [DecidableEq J'] [TopologicalSpace I'] [DiscreteTopology I'] (j : N →L[R] ZeroAtInftyContinuousMap I' R) (s : ZeroAtInftyContinuousMap J' R →L[R] M) : (j ∘SL u ∘SL s).IsRowCompact

Over ultrametric Tate scalars, for a row-compact map u between (Pr) modules every composite j ∘ u ∘ s with continuous linear maps into and out of model spaces is row compact. In particular the extension of u through any retract presentations is row compact.

theorem ContinuousLinearMap.isPrCompact_iff_isRowCompact_comp {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {J : Type u} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {I : Type v} [TopologicalSpace I] [DiscreteTopology I] {iM : M →L[R] ZeroAtInftyContinuousMap J R} {rM : ZeroAtInftyContinuousMap J R →L[R] M} {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hM : rM ∘SL iM = ContinuousLinearMap.id R M) (hN : rN ∘SL iN = ContinuousLinearMap.id R N) {u : M →L[R] N} : u.IsPrCompact ↔ (iN ∘SL u ∘SL rM).IsRowCompact

Row compactness on (Pr) modules does not depend on the presentation: over ultrametric Tate scalars, u is row compact exactly when its extension through any one pair of retract presentations is.

theorem ContinuousLinearMap.isPrCompact_iff_isRowCompact_comp_symm {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {J : Type u} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {I : Type v} [TopologicalSpace I] [DiscreteTopology I] (eM : M ≃L[R] ZeroAtInftyContinuousMap J R) (eN : N ≃L[R] ZeroAtInftyContinuousMap I R) {u : M →L[R] N} : u.IsPrCompact ↔ (↑eN ∘SL u ∘SL ↑eM.symm).IsRowCompact

Transport along equivalences with model spaces: over ultrametric Tate scalars, a map between potentially orthonormalisable modules is row compact exactly when its conjugate eN ∘ u ∘ eM⁻¹ between the model spaces is.

@[simp]

theorem ContinuousLinearMap.isPrCompact_iff_isRowCompact {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {J : Type u} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {I : Type v} [TopologicalSpace I] [DiscreteTopology I] {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} : u.IsPrCompact ↔ u.IsRowCompact

On model spaces, row compactness in the sense of (Pr) modules is row compactness.

theorem ContinuousLinearMap.IsPrCompact.add {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u v : M →L[R] N} (hu : u.IsPrCompact) (hv : v.IsPrCompact) : (u + v).IsPrCompact

Sums of row-compact maps between (Pr) modules are row compact.

theorem ContinuousLinearMap.IsPrCompact.sub {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u v : M →L[R] N} (hu : u.IsPrCompact) (hv : v.IsPrCompact) : (u - v).IsPrCompact

Differences of row-compact maps between (Pr) modules are row compact.

theorem ContinuousLinearMap.IsPrCompact.comp_clm {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {L : Type u_1} {M : Type u} {N : Type v} [SeminormedAddCommGroup L] [Module R L] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {u : M →L[R] N} (hu : u.IsPrCompact) (w : L →L[R] M) (hL : TauCeti.HasPr R L) : (u ∘SL w).IsPrCompact

Precomposing a row-compact map between (Pr) modules with a continuous linear map out of a module with property (Pr) gives a row-compact map.

theorem ContinuousLinearMap.IsPrCompact.clm_comp {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} {P : Type u_2} [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [SeminormedAddCommGroup P] [Module R P] {u : M →L[R] N} (hu : u.IsPrCompact) (w : N →L[R] P) (hP : TauCeti.HasPr R P) : (w ∘SL u).IsPrCompact

Postcomposing a row-compact map between (Pr) modules with a continuous linear map into a module with property (Pr) gives a row-compact map.

theorem ContinuousLinearMap.IsPrCompact.aeval {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] [ContinuousConstSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) {B : Polynomial R} (hB0 : B.coeff 0 = 0) : ((Polynomial.aeval u) B).IsPrCompact

A polynomial with zero constant coefficient preserves row compactness on modules with property (Pr), over ultrametric Tate scalars.

theorem ContinuousLinearMap.isPrCompact_of_tendsto {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {ι : Type u_1} {l : Filter ι} [l.NeBot] {u : M →L[R] N} {v : ι → M →L[R] N} (h : Filter.Tendsto (fun (n : ι) => ‖u - v n‖) l (nhds 0)) (hv : ∀ᶠ (n : ι) in l, (v n).IsPrCompact) : u.IsPrCompact

Closedness: over ultrametric Tate scalars, an operator-norm limit of row-compact maps between (Pr) modules is row compact.

theorem ContinuousLinearMap.IsPrCompact.tendsto_ringOpNorm_comp_indicatorCLM_comp_sub {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] {iN : N →L[R] ZeroAtInftyContinuousMap I R} {rN : ZeroAtInftyContinuousMap I R →L[R] N} (hN : rN ∘SL iN = ContinuousLinearMap.id R N) {u : M →L[R] N} (hu : u.IsPrCompact) : Filter.Tendsto (fun (S : Finset I) => ‖rN ∘SL ZeroAtInftyContinuousMap.indicatorCLM R ↑S ∘SL iN ∘SL u - u‖) Filter.atTop (nhds 0)

Approximation by truncations: over ultrametric Tate scalars, if rN ∘ iN = id presents the target of a row-compact map u between (Pr) modules, then the truncations rN ∘ π_S ∘ iN ∘ u converge to u in operator norm as the finite set S of coordinates grows. Here π_S = ZeroAtInftyContinuousMap.indicatorCLM R S is the coordinate projection.

theorem ContinuousLinearMap.IsPrCompact.isCompletelyContinuous {R : Type w} [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {M : Type u} {N : Type v} [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] {u : M →L[R] N} (hu : u.IsPrCompact) : u.IsCompletelyContinuous

Over ultrametric Tate scalars, row-compact maps between (Pr) modules are completely continuous.

theorem ContinuousLinearMap.isPrCompact_of_finite {R : Type w} [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [Module.Finite R M] (hM : TauCeti.HasPr R M) {L : Type u_1} [SeminormedAddCommGroup L] [Module R L] (hL : TauCeti.HasPr R L) (u : L →L[R] M) : u.IsPrCompact

Over complete ultrametric Tate scalars, every continuous linear map from a module with property (Pr) into a finitely generated module with property (Pr) is row compact. A finitely generated module with (Pr) is a retract of C₀(S, R) for a finite set S of generators.

theorem ContinuousLinearMap.isPrCompact_id_iff {R : Type w} [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] : (ContinuousLinearMap.id R M).IsPrCompact ↔ TauCeti.HasPr R M ∧ Module.Finite R M

The identity criterion on (Pr) modules: over complete ultrametric Tate scalars, the identity of a module is row compact exactly when the module has property (Pr) and is finitely generated.

theorem ContinuousLinearMap.IsPrCompact.finite_of_one_sub_pow_eq_zero {R : Type w} [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) {n : ℕ} (hn : (1 - u) ^ n = 0) : Module.Finite R M

The finiteness germ: over complete ultrametric Tate scalars, a row-compact endomorphism u of a (Pr) module with (1 - u) ^ n = 0 forces the module to be finitely generated.

theorem ContinuousLinearMap.IsPrCompact.projective_of_one_sub_pow_eq_zero {R : Type w} [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] {u : M →L[R] M} (hu : u.IsPrCompact) {n : ℕ} (hn : (1 - u) ^ n = 0) : Module.Projective R M

Over complete ultrametric Tate scalars, a row-compact endomorphism u of a (Pr) module with (1 - u) ^ n = 0 forces the module to be finitely generated projective.

theorem ContinuousLinearMap.IsPrCompact.finite_range_of_isIdempotentElem {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {e : M →L[R] M} (hu : e.IsPrCompact) (he : IsIdempotentElem e) : Module.Finite R ↥(↑e).range

A row-compact idempotent of a (Pr) module has finitely generated range.

theorem ContinuousLinearMap.IsPrCompact.projective_range_of_isIdempotentElem {R : Type w} [NormedCommRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R] {M : Type u} [SeminormedAddCommGroup M] [Module R M] {e : M →L[R] M} (hu : e.IsPrCompact) (he : IsIdempotentElem e) : Module.Projective R ↥(↑e).range

A row-compact idempotent of a (Pr) module has projective range.