Ranges of idempotent operators close to a factored compression

Let E be a complete normed module over Tate scalars and e an idempotent endomorphism of E. Suppose the compression e ∘ c ∘ e of e by an operator c lies within operator-norm distance less than one of e, and that c = b ∘ a factors through an R-module P along linear maps a : E → P and b : P → E. Then the range of e is a direct summand of P (ContinuousLinearMap.exists_comp_eq_id_of_isIdempotentElem): there are linear maps f : P → range e and g : range e → P with f ∘ g = id. The inverse of 1 - (e - e ∘ c ∘ e) is the Neumann series (ContinuousLinearMap.oneSub), so no basis of the range and no division by nonunits of the scalars is involved, and the statement holds over coefficient rings with nilpotents.

Applied with P finite free and c the projection of a model space C₀(I, R) onto finitely many coordinates, it shows that row-compact idempotents have finitely generated projective range.

Main results

• ContinuousLinearMap.exists_mul_mul_mul_eq_of_isIdempotentElem: if ‖e - e ∘ c ∘ e‖ < 1, then e = e ∘ c ∘ e ∘ w for a continuous endomorphism w.
• ContinuousLinearMap.exists_comp_eq_id_of_isIdempotentElem: if ‖e - e ∘ c ∘ e‖ < 1 and c factors through P, the range of the idempotent e is a direct summand of P.

theorem ContinuousLinearMap.exists_mul_mul_mul_eq_of_isIdempotentElem {R : Type u_1} {E : Type u_2} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [CompleteSpace E] {e c : E →L[R] E} (he : IsIdempotentElem e) (h : ‖e - e * c * e‖ < 1) : ∃ (w : E →L[R] E), e * c * e * w = e

Over Tate scalars, let e be an idempotent endomorphism of a complete normed module whose compression e ∘ c ∘ e satisfies ‖e - e ∘ c ∘ e‖ < 1. Then e factors through its compression: e = e ∘ c ∘ e ∘ w for a continuous endomorphism w, the inverse of 1 - (e - e ∘ c ∘ e).

theorem ContinuousLinearMap.exists_comp_eq_id_of_isIdempotentElem {R : Type u_1} {E : Type u_2} {P : Type u_3} [SeminormedRing R] [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup E] [Module R E] [IsBoundedSMul R E] [CompleteSpace E] [AddCommMonoid P] [Module R P] {e c : E →L[R] E} (he : IsIdempotentElem e) (a : E →ₗ[R] P) (b : P →ₗ[R] E) (hc : ↑c = b ∘ₗ a) (h : ‖e - e * c * e‖ < 1) : ∃ (f : P →ₗ[R] ↥(↑e).range) (g : ↥(↑e).range →ₗ[R] P), f ∘ₗ g = LinearMap.id

Over Tate scalars, let e be an idempotent endomorphism of a complete normed module whose compression e ∘ c ∘ e satisfies ‖e - e ∘ c ∘ e‖ < 1, where c = b ∘ a factors through an R-module P. Then the range of e is a direct summand of P: there are linear maps f : P → range e and g : range e → P with f ∘ g = id.