Ranges of intertwined projections

For idempotent continuous linear maps p and q on a topological module, the operator U = q * p + (1 - q) * (1 - p) satisfies q * U = U * p. When U is invertible, it therefore carries the range of p isomorphically onto the range of q (ContinuousLinearMap.IsIdempotentElem.rangeEquiv). This is the intertwining operator of a pair of projections; it is the local chart of the image bundle of a continuous family of projections, and it shows that nearby projections have isomorphic ranges.

For a retract r ∘ i = id of M through N, the extension i ∘ e ∘ r of an endomorphism e of M is idempotent when e is, and i identifies the range of e with the range of i ∘ e ∘ r (ContinuousLinearMap.rangeEquivOfRetract).

A pseudo-inverse g of f, with f ∘ g ∘ f = f, gives the projection g ∘ f (ContinuousLinearMap.isIdempotentElem_comp_of_comp_comp_eq_self).

Main definitions

• ContinuousLinearMap.IsIdempotentElem.rangeEquiv: the isomorphism of the ranges of p and q induced by q * p + (1 - q) * (1 - p), when that operator is invertible.
• ContinuousLinearMap.rangeEquivOfRetract: the identification of the range of e with the range of its extension i ∘ e ∘ r along a retract.

Main results

• ContinuousLinearMap.IsIdempotentElem.apply_coe_range: an idempotent continuous linear map fixes every vector of its range.
• ContinuousLinearMap.IsIdempotentElem.mul_self_add_one_sub_mul_one_sub: the operator p * p + (1 - p) * (1 - p) intertwining an idempotent p with itself is the identity.
• ContinuousLinearMap.isIdempotentElem_comp_comp_of_retract: the extension of an idempotent along a retract is idempotent.
• ContinuousLinearMap.isIdempotentElem_comp_of_comp_comp_eq_self: if g is a pseudo-inverse of f, then g ∘ f is a continuous projection.

References

• T. Kato, Perturbation Theory for Linear Operators, Springer, Chapter I, §4.6, for the intertwining operator of a pair of projections.

@[simp]

theorem ContinuousLinearMap.IsIdempotentElem.apply_coe_range {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : M →L[R] M} (hp : IsIdempotentElem p) (w : ↥(↑p).range) : p ↑w = ↑w

An idempotent continuous linear map fixes every vector of its range.

theorem ContinuousLinearMap.IsIdempotentElem.mul_self_add_one_sub_mul_one_sub {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : M →L[R] M} [IsTopologicalAddGroup M] (hp : IsIdempotentElem p) : p * p + (1 - p) * (1 - p) = 1

The operator p * p + (1 - p) * (1 - p), which intertwines an idempotent p with itself, is the identity.

theorem ContinuousLinearMap.IsIdempotentElem.isUnit_mul_self_add_one_sub_mul_one_sub {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : M →L[R] M} [IsTopologicalAddGroup M] (hp : IsIdempotentElem p) : IsUnit (p * p + (1 - p) * (1 - p))

The operator p * p + (1 - p) * (1 - p) is invertible for an idempotent p.

noncomputable def ContinuousLinearMap.IsIdempotentElem.rangeEquiv {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : M →L[R] M} [IsTopologicalAddGroup M] (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hU : IsUnit (q * p + (1 - q) * (1 - p))) : ↥(↑p).range ≃L[R] ↥(↑q).range

Intertwined projections have isomorphic ranges. For idempotents p and q such that U = q * p + (1 - q) * (1 - p) is invertible, U restricts to an isomorphism from the range of p onto the range of q, with inverse the restriction of U⁻¹.

@[simp]

theorem ContinuousLinearMap.IsIdempotentElem.coe_rangeEquiv_apply {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : M →L[R] M} [IsTopologicalAddGroup M] (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hU : IsUnit (q * p + (1 - q) * (1 - p))) (w : ↥(↑p).range) : ↑((rangeEquiv hp hq hU) w) = (q * p + (1 - q) * (1 - p)) ↑w

The isomorphism of ranges applies q * p + (1 - q) * (1 - p).

@[simp]

theorem ContinuousLinearMap.IsIdempotentElem.coe_rangeEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] {p q : M →L[R] M} [IsTopologicalAddGroup M] (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) (hU : IsUnit (q * p + (1 - q) * (1 - p))) (w : ↥(↑q).range) : ↑((rangeEquiv hp hq hU).symm w) = (Ring.inverse (q * p + (1 - q) * (1 - p))) ↑w

The inverse isomorphism of ranges applies the inverse of q * p + (1 - q) * (1 - p).

theorem ContinuousLinearMap.isIdempotentElem_comp_of_comp_comp_eq_self {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] {f : M →L[R] N} {g : N →L[R] M} (hfg : f ∘SL g ∘SL f = f) : IsIdempotentElem (g ∘SL f)

If g is a pseudo-inverse of f, that is f ∘ g ∘ f = f, then g ∘ f is a projection.

theorem ContinuousLinearMap.isIdempotentElem_comp_comp_of_retract {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] {i : M →L[R] N} {r : N →L[R] M} {e : M →L[R] M} (he : IsIdempotentElem e) (hri : r ∘SL i = ContinuousLinearMap.id R M) : IsIdempotentElem (i ∘SL e ∘SL r)

For a retract r ∘ i = id of M through N, the extension i ∘ e ∘ r of an idempotent e of M is an idempotent of N.

noncomputable def ContinuousLinearMap.rangeEquivOfRetract {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] {i : M →L[R] N} {r : N →L[R] M} (e : M →L[R] M) (hri : r ∘SL i = ContinuousLinearMap.id R M) : ↥(↑e).range ≃ₗ[R] ↥(↑i ∘ₗ ↑e ∘ₗ ↑r).range

For a retract r ∘ i = id of M through N, the inclusion i identifies the range of an endomorphism e of M with the range of its extension i ∘ e ∘ r.

@[simp]

theorem ContinuousLinearMap.coe_rangeEquivOfRetract_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] {i : M →L[R] N} {r : N →L[R] M} (e : M →L[R] M) (hri : r ∘SL i = ContinuousLinearMap.id R M) (x : ↥(↑e).range) : ↑((rangeEquivOfRetract e hri) x) = i ↑x

The identification of ranges along a retract applies the inclusion i.

@[simp]

theorem ContinuousLinearMap.coe_rangeEquivOfRetract_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [TopologicalSpace N] [AddCommMonoid N] [Module R N] {i : M →L[R] N} {r : N →L[R] M} (e : M →L[R] M) (hri : r ∘SL i = ContinuousLinearMap.id R M) (y : ↥(↑i ∘ₗ ↑e ∘ₗ ↑r).range) : ↑((rangeEquivOfRetract e hri).symm y) = r ↑y

The inverse identification of ranges along a retract applies the retraction r.