Documentation

Mathlib.Analysis.Normed.Module.ContinuousInverse

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.

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

Main definitions and results #

ContinuousLinearMap.HasRightInverse: 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
ContinuousLinearEquiv.hasRightInverse 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.HasLefttInverse.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 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 hav 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 continuout left inverse.
f has a continuous left inverse if and only if it is injective, has closed range, and its range admits a closed complement

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) :

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

Equations

f.HasLeftInverse = ∃ (g : F →L[R] E), Function.LeftInverse ⇑g ⇑f

Instances For

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) :

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

Equations

f.HasRightInverse = ∃ (g : F →L[R] E), Function.RightInverse ⇑g ⇑f

Instances For

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) :

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

Equations

h.leftInverse = Classical.choose h

Instances For

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.

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) :

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

Equations

h.rightInverse = Classical.choose h

Instances For

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 splits.

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.