The rank of a continuous family of projections

Let p : B → F →L[𝕜] F be a continuous family of idempotent operators on a Banach space F. Near any x₀, the operator p x * p x₀ + (1 - p x) * (1 - p x₀) is invertible, since it equals 1 at x₀ and the units of F →L[𝕜] F form an open set. It then carries the range of p x₀ isomorphically onto the range of p x (ContinuousLinearMap.IsIdempotentElem.rangeEquiv), so the ranges of nearby projections are isomorphic and the rank of the family is locally constant. No compactness, separation or finite-dimensionality is assumed of the base or the fibres.

Main results

• TauCeti.isOpen_setOf_isUnit_intertwiner: the intertwining operator of a continuous family is invertible on an open set, and TauCeti.continuousOn_inverse_intertwiner: its inverse is continuous there.
• TauCeti.eventually_nonempty_continuousLinearEquiv_range: the ranges of nearby projections in a continuous family are isomorphic.
• TauCeti.isLocallyConstant_finrank_range: the rank of a continuous family of projections is locally constant.

References

• T. Kato, Perturbation Theory for Linear Operators, Springer, Chapter I, §4.6.

theorem TauCeti.continuous_intertwiner {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : B → F →L[𝕜] F} (hp : Continuous p) (x₀ : B) : Continuous fun (x : B) => p x * p x₀ + (1 - p x) * (1 - p x₀)

The intertwining operator p x * p x₀ + (1 - p x) * (1 - p x₀) of a continuous family of operators depends continuously on x.

theorem TauCeti.isOpen_setOf_isUnit_intertwiner {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : B → F →L[𝕜] F} [CompleteSpace F] (hp : Continuous p) (x₀ : B) : IsOpen {x : B | IsUnit (p x * p x₀ + (1 - p x) * (1 - p x₀))}

The points at which the intertwining operator p x * p x₀ + (1 - p x) * (1 - p x₀) of a continuous family of operators is invertible form an open set.

theorem TauCeti.continuousOn_inverse_intertwiner {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : B → F →L[𝕜] F} [CompleteSpace F] (hp : Continuous p) (x₀ : B) : ContinuousOn (fun (x : B) => Ring.inverse (p x * p x₀ + (1 - p x) * (1 - p x₀))) {x : B | IsUnit (p x * p x₀ + (1 - p x) * (1 - p x₀))}

The inverse of the intertwining operator p x * p x₀ + (1 - p x) * (1 - p x₀) of a continuous family of operators depends continuously on x where that operator is invertible.

theorem TauCeti.eventually_nonempty_continuousLinearEquiv_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : B → F →L[𝕜] F} [CompleteSpace F] (hp : Continuous p) (hidem : ∀ (x : B), IsIdempotentElem (p x)) (x₀ : B) : ∀ᶠ (x : B) in nhds x₀, Nonempty (↥(↑(p x₀)).range ≃L[𝕜] ↥(↑(p x)).range)

The ranges of nearby projections in a continuous family are isomorphic.

theorem TauCeti.isLocallyConstant_finrank_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {B : Type u_2} [TopologicalSpace B] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : B → F →L[𝕜] F} [CompleteSpace F] (hp : Continuous p) (hidem : ∀ (x : B), IsIdempotentElem (p x)) : IsLocallyConstant fun (x : B) => Module.finrank 𝕜 ↥(↑(p x)).range

The rank of a continuous family of projections is locally constant.