Continuous linear maps with a continuous left/right inverse

This file defines continuous linear maps which admit a continuous left/right inverse.

We prove that both of these classes of maps are closed under products, composition and contain linear equivalences, and a sufficient criterion in finite dimension: a surjective linear map on a finite-dimensional space always admits a continuous right inverse; an injective linear map on a finite-dimensional space always admits a continuous left inverse.

We also prove an equivalent characterisation of admitting a continuous left inverse: f admits a continuous left inverse if and only if it is injective, has closed range and its range admits a closed complement. This characterisation is used to extract a complement from immersions, for use in the regular value theorem. (For submersions, there is a natural choice of complement, and an analogous statement is not necessary.)

This concept is used to give an equivalent definition of immersions and submersions of manifolds.

Main definitions and results

• ContinuousLinearMap.HasLeftInverse: a continuous linear map admits a left inverse which is a continuous linear map itself

• ContinuousLinearMap.HasRightInverse: a continuous linear map admits a right inverse which is a continuous linear map itself

• ContinuousLinearMap.HasLeftInverse.isClosed_range: if f has a continuous left inverse, its range is closed

• ContinuousLinearMap.HasLeftInverse.closedComplemented_range: if f has a continuous left inverse, its range admits a closed complement

• ContinuousLinearMap.HasLeftInverse.complement: a choice of closed complement for range f

• ContinuousLinearMap.HasLeftInverse.of_injective_of_isClosed_range_of_closedComplement_range: if f is injective and has closed range with a closed complement, it admits a continuous left inverse

• ContinuousLinearEquiv.hasLeftInverse and ContinuousLinearEquiv.hasRightInverse: a continuous linear equivalence admits a continuous left (resp. right) inverse

• ContinuousLinearMap.HasLeftInverse.comp, ContinuousLinearMap.HasRightInverse.comp: if f : E → F and g : F → G both admit a continuous left (resp. right) inverse, so does g.comp f.

• ContinuousLinearMap.HasLeftInverse.of_comp, ContinuousLinearMap.HasRightInverse.of_comp: suppose f : E → F and g : F → G are continuous linear maps. If g.comp f : E → G admits a continuous left inverse, then so does f. If g.comp f : E → G admits a continuous right inverse, then so does g.

• ContinuousLinearMap.HasLeftInverse.prodMap, ContinuousLinearMap.HasRightInverse.prodMap: having a continuous left/right inverse is closed under taking products

• ContinuousLinearMap.HasLeftInverse.inl, ContinuousLinearMap.HasLeftInverse.inr: ContinuousLinearMap.inl and .inr have a continuous left inverse

• ContinuousLinearMap.HasRightInverse.fst, ContinuousLinearMap.HasRightInverse.snd: ContinuousLinearMap.fst and .snd have a continuous right inverse

• ContinuousLinearMap.HasLeftInverse.of_injective_of_finiteDimensional: if f : E → F is injective and F is finite-dimensional, f has a continuous left inverse.

• ContinuousLinearMap.HasRightInverse.of_surjective_of_finiteDimensional: if f : E → F is surjective and F is finite-dimensional, f has a continuous right inverse.

TODO

• Suppose E and F are Banach and f : E → F is Fredholm. If f is surjective, it has a continuous right inverse. If f is injective, it has a continuous left inverse.

def ContinuousLinearMap.HasLeftInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E →L[R] F) : Prop

A continuous linear map admits a left inverse which is a continuous linear map itself.

def ContinuousLinearMap.HasRightInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E →L[R] F) : Prop

A continuous linear map admits a right inverse which is a continuous linear map itself.

noncomputable def ContinuousLinearMap.HasLeftInverse.leftInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasLeftInverse) : F →L[R] E

Choice of continuous left inverse for f : F →L[R] E, given that such an inverse exists.

theorem ContinuousLinearMap.HasLeftInverse.leftInverse_leftInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasLeftInverse) : Function.LeftInverse ⇑h.leftInverse ⇑f

theorem ContinuousLinearMap.HasLeftInverse.injective {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasLeftInverse) : Function.Injective ⇑f

theorem ContinuousLinearMap.HasLeftInverse.congr {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f g : E →L[R] F} (hf : f.HasLeftInverse) (hfg : g = f) : g.HasLeftInverse

theorem ContinuousLinearEquiv.hasLeftInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) : (↑f).HasLeftInverse

A continuous linear equivalence has a continuous left inverse.

@[simp]

theorem ContinuousLinearEquiv.leftInverse_hasLeftInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) : ⋯.leftInverse = ↑f.symm

theorem ContinuousLinearMap.HasLeftInverse.of_isInvertible {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (hf : f.IsInvertible) : f.HasLeftInverse

An invertible continuous linear map has a continuous left inverse.

theorem ContinuousLinearMap.HasLeftInverse.prodMap {R : Type u_1} [Semiring R] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace E'] [AddCommMonoid E'] [Module R E'] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {g : E' →L[R] F'} (hf : f.HasLeftInverse) (hg : g.HasLeftInverse) : (f.prodMap g).HasLeftInverse

If f and g admit continuous left inverses, so does f × g.

theorem ContinuousLinearMap.HasLeftInverse.comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} [TopologicalSpace G] [AddCommMonoid G] [Module R G] {g : F →L[R] G} (hg : g.HasLeftInverse) (hf : f.HasLeftInverse) : (g.comp f).HasLeftInverse

theorem ContinuousLinearMap.HasLeftInverse.of_comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} [TopologicalSpace G] [AddCommMonoid G] [Module R G] {g : F →L[R] G} (hfg : (g.comp f).HasLeftInverse) : f.HasLeftInverse

theorem ContinuousLinearMap.HasLeftInverse.comp_continuousLinearEquivalence {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {f₀ : F' ≃L[R] E} (hf : f.HasLeftInverse) : (f.comp ↑f₀).HasLeftInverse

theorem ContinuousLinearMap.HasLeftInverse.continuousLinearEquivalence_comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {g : F ≃L[R] F'} (hf : f.HasLeftInverse) : ((↑g).comp f).HasLeftInverse

theorem ContinuousLinearMap.HasLeftInverse.inl {R : Type u_1} [Semiring R] {F : Type u_4} {G : Type u_6} [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] : (inl R F G).HasLeftInverse

ContinuousLinearMap.inl has a continuous left inverse.

theorem ContinuousLinearMap.HasLeftInverse.inr {R : Type u_1} [Semiring R] {F : Type u_4} {G : Type u_6} [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] : (inr R F G).HasLeftInverse

ContinuousLinearMap.inr has a continuous left inverse.

theorem ContinuousLinearMap.HasLeftInverse.of_injective_of_finiteDimensional {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {E : Type u_8} {F : Type u_9} [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] {f : E →L[𝕜] F} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] (hf : Function.Injective ⇑f) : f.HasLeftInverse

If f : E → F is injective and E is finite-dimensional, f has a continuous left inverse.

An equivalent characterisation of maps with a continuous left inverse

theorem ContinuousLinearMap.HasLeftInverse.closedComplemented_range {R : Type u_7} {E : Type u_8} {F : Type u_10} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F} (hf : f.HasLeftInverse) : (↑f).range.ClosedComplemented

If f has a continuous left inverse, its range admits a closed complement.

theorem ContinuousLinearMap.HasLeftInverse.isClosed_range {R : Type u_7} {E : Type u_8} {F : Type u_10} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F} [T1Space F] (hf : f.HasLeftInverse) [IsTopologicalAddGroup F] : IsClosed (Set.range ⇑f)

noncomputable def ContinuousLinearMap.HasLeftInverse.complement {R : Type u_7} {E : Type u_8} {F : Type u_10} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F} [T1Space F] (h : f.HasLeftInverse) : Submodule R F

Choice of a closed complement of range f

theorem ContinuousLinearMap.HasLeftInverse.isClosed_complement {R : Type u_7} {E : Type u_8} {F : Type u_10} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F} [T1Space F] (h : f.HasLeftInverse) : IsClosed ↑h.complement

theorem ContinuousLinearMap.HasLeftInverse.isCompl_complement {R : Type u_7} {E : Type u_8} {F : Type u_10} [Ring R] [TopologicalSpace E] [AddCommGroup E] [Module R E] [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F} [T1Space F] (h : f.HasLeftInverse) : IsCompl (↑f).range h.complement

theorem ContinuousLinearMap.HasLeftInverse.of_injective_of_isClosed_range_of_closedComplement_range {R : Type u_7} {E : Type u_8} {F : Type u_9} [NontriviallyNormedField R] [NormedAddCommGroup E] [NormedSpace R E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace R F] [CompleteSpace F] {f : E →L[R] F} (hf : Function.Injective ⇑f) (hf' : IsClosed (Set.range ⇑f)) (hf'' : (↑f).range.ClosedComplemented) : f.HasLeftInverse

A continuous linear map between Banach spaces has a continuous left inverse if it is injective, has closed range and its range has a closed complement.

noncomputable def ContinuousLinearMap.HasRightInverse.rightInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasRightInverse) : F →L[R] E

Choice of continuous right inverse for f : F →L[R] E, given that such an inverse exists.

theorem ContinuousLinearMap.HasRightInverse.rightInverse_rightInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasRightInverse) : Function.RightInverse ⇑h.rightInverse ⇑f

theorem ContinuousLinearMap.HasRightInverse.surjective {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (h : f.HasRightInverse) : Function.Surjective ⇑f

theorem ContinuousLinearMap.HasRightInverse.congr {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f g : E →L[R] F} (hf : f.HasRightInverse) (hfg : g = f) : g.HasRightInverse

theorem ContinuousLinearEquiv.hasRightInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) : (↑f).HasRightInverse

A continuous linear equivalence has a continuous right inverse.

@[simp]

theorem ContinuousLinearEquiv.rightInverse_hasRightInverse {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] (f : E ≃L[R] F) : ⋯.rightInverse = ↑f.symm

theorem ContinuousLinearMap.HasRightInverse.of_isInvertible {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} (hf : f.IsInvertible) : f.HasRightInverse

An invertible continuous linear map has a continuous right inverse.

theorem ContinuousLinearMap.HasRightInverse.prodMap {R : Type u_1} [Semiring R] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace E'] [AddCommMonoid E'] [Module R E'] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {g : E' →L[R] F'} (hf : f.HasRightInverse) (hg : g.HasRightInverse) : (f.prodMap g).HasRightInverse

If f and g split, then so does f × g.

theorem ContinuousLinearMap.HasRightInverse.comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} [TopologicalSpace G] [AddCommMonoid G] [Module R G] {g : F →L[R] G} (hg : g.HasRightInverse) (hf : f.HasRightInverse) : (g.comp f).HasRightInverse

theorem ContinuousLinearMap.HasRightInverse.of_comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] {f : E →L[R] F} [TopologicalSpace G] [AddCommMonoid G] [Module R G] {g : F →L[R] G} (hfg : (g.comp f).HasRightInverse) : g.HasRightInverse

theorem ContinuousLinearMap.HasRightInverse.comp_continuousLinearEquivalence {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {f₀ : F' ≃L[R] E} (hf : f.HasRightInverse) : (f.comp ↑f₀).HasRightInverse

theorem ContinuousLinearMap.HasRightInverse.continuousLinearEquivalence_comp {R : Type u_1} [Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [TopologicalSpace E] [AddCommMonoid E] [Module R E] [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace F'] [AddCommMonoid F'] [Module R F'] {f : E →L[R] F} {g : F ≃L[R] F'} (hf : f.HasRightInverse) : ((↑g).comp f).HasRightInverse

theorem ContinuousLinearMap.HasRightInverse.fst {R : Type u_1} [Semiring R] {F : Type u_4} {G : Type u_6} [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] : (fst R F G).HasRightInverse

ContinuousLinearMap.fst has a continuous right inverse.

theorem ContinuousLinearMap.HasRightInverse.snd {R : Type u_1} [Semiring R] {F : Type u_4} {G : Type u_6} [TopologicalSpace F] [AddCommMonoid F] [Module R F] [TopologicalSpace G] [AddCommMonoid G] [Module R G] : (snd R F G).HasRightInverse

ContinuousLinearMap.snd has a continuous right inverse.

theorem ContinuousLinearMap.HasRightInverse.of_surjective_of_finiteDimensional {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {E : Type u_8} {F : Type u_9} [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] {f : E →L[𝕜] F} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] (hf : Function.Surjective ⇑f) : f.HasRightInverse

If f : E → F is surjective and F is finite-dimensional, f has a continuous right inverse.