Left inverses for triangular operators

An operator on a product which retains the first coordinate admits a continuous linear left inverse exactly when its restriction to the second factor does. This is the linear algebra of the differential of a parameter-preserving family of immersions.

The construction uses Mathlib's ContinuousLinearMap.HasLeftInverse: subtract the contribution of the first coordinate, then apply a left inverse on the second factor.

If a compression P ∘L A is invertible, the left inverse (P ∘L A).inverse ∘L P also gives a projection off the range of A. Composing a linear map with this projection annihilates A.

A continuous linear injection of a space into a finite-dimensional space of strictly larger dimension over a complete field has a continuous left inverse and a nonzero continuous covector annihilating its range (ContinuousLinearMap.exists_leftInverse_ne_zero_comp_eq_zero).

theorem ContinuousLinearMap.hasLeftInverse_fst_prod_iff {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [TopologicalSpace G] [AddCommGroup G] [Module R G] [IsTopologicalAddGroup G] (A : E × F →L[R] G) : ((fst R E F).prod A).HasLeftInverse ↔ (A ∘SL inr R E F).HasLeftInverse

A continuous linear operator retaining the first coordinate is split-injective exactly when its restriction to the second factor is split-injective.

theorem ContinuousLinearMap.sub_comp_inverse_comp_comp_eq_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] [TopologicalSpace G] [AddCommGroup G] [Module R G] [IsTopologicalAddGroup G] (a : E →L[R] G) (A : F →L[R] E) (P : E →L[R] F) (hQ : (P ∘SL A).IsInvertible) : (a - a ∘SL A ∘SL (P ∘SL A).inverse ∘SL P) ∘SL A = 0

Projecting a continuous linear map off the range of an operator with invertible compression annihilates that operator.

theorem ContinuousLinearMap.exists_leftInverse_ne_zero_comp_eq_zero {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (A : F →L[𝕜] E) (hA : Function.Injective ⇑A) (h : Module.finrank 𝕜 F < Module.finrank 𝕜 E) : ∃ (P : E →L[𝕜] F) (a : E →L[𝕜] 𝕜), Function.LeftInverse ⇑P ⇑A ∧ a ≠ 0 ∧ a ∘SL A = 0

A continuous linear injection of a space F into a finite-dimensional space E of strictly larger dimension has a continuous left inverse and a nonzero continuous covector annihilating its range.