feat: equivalent characterisation of split continuous linear maps (#35057)

We add an equivalent characterisation of continuous linear maps with a continuous left inverse:
`f` admits a continuous left inverse iff it is injective, has closed range and `range f` has a closed complement.

This equivalence is used for extracting an explicit complement for immersions, hence transitively for proving that immersions are closed under composition.

From the path towards immersions, submersions and embedded submanifolds.

Author: grunweg

Mathlib/Algebra/Module/Submodule/Range.lean

@@ -206,13 +206,24 @@ theorem comap_le_comap_iff {f : M →ₛₗ[τ₁₂] M₂} (hf : range f = ⊤)
 theorem comap_injective {f : M →ₛₗ[τ₁₂] M₂} (hf : range f = ⊤) : Injective (comap f) := fun _ _ h =>
   le_antisymm ((comap_le_comap_iff hf).1 (le_of_eq h)) ((comap_le_comap_iff hf).1 (ge_of_eq h))
 
--- TODO (?): generalize to semilinear maps with `f ∘ₗ g` bijective.
+-- TODO (?): generalize the next two lemmas to semilinear maps with `f ∘ₗ g` bijective.
+
 theorem ker_eq_range_of_comp_eq_id {M P} [AddCommGroup M] [Module R M]
     [AddCommGroup P] [Module R P] {f : M →ₗ[R] P} {g : P →ₗ[R] M} (h : f ∘ₗ g = .id) :
     ker f = range (LinearMap.id - g ∘ₗ f) :=
   le_antisymm (fun x hx ↦ ⟨x, show x - g (f x) = x by rw [hx, map_zero, sub_zero]⟩) <|
     range_le_ker_iff.mpr <| by rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]
 
+/-- If `f : E →ₗ[R] F` has a left inverse `g`, then `range f = ker (f ∘ g - id)`.
+
+This is the dual version of `LinearMap.ker_eq_range_of_comp_eq_id`. -/
+lemma range_eq_ker_of_leftInverse {M P} [AddCommGroup M] [Module R M]
+    [AddCommGroup P] [Module R P] {f : M →ₗ[R] P} {g : P →ₗ[R] M}
+    (h : LeftInverse g f) : f.range = ker ((f.comp g) - LinearMap.id) :=
+  -- If `y = f x ∈ range f`, we have `(f ∘ g) y = f (g (f x)) = f x = y` by hypothesis `h`.
+  -- Conversely, f g z - z = 0 implies z = f (g z) ∈ range f.
+  le_antisymm (by rintro y ⟨x, rfl⟩; simp [h x]) (fun x hx ↦ ⟨g x, by simpa [sub_eq_zero] using hx⟩)
+
 end
 
 end AddCommMonoid

Mathlib/Analysis/Normed/Module/ContinuousInverse.lean

@@ -5,13 +5,7 @@ Authors: Michael Rothgang
 -/
 module
 
-public import Mathlib.Algebra.Order.BigOperators.Expect
-public import Mathlib.Algebra.Order.Field.Power
-public import Mathlib.Data.EReal.Inv
-public import Mathlib.Data.Real.Sqrt
-public import Mathlib.Logic.Equiv.PartialEquiv
-public import Mathlib.Tactic.ContinuousFunctionalCalculus
-public import Mathlib.Tactic.Positivity
+public import Mathlib.Analysis.Normed.Operator.Banach
 public import Mathlib.Topology.Algebra.Module.FiniteDimension
 
 /-! # Continuous linear maps with a continuous left/right inverse
@@ -23,6 +17,12 @@ linear equivalences, and a sufficient criterion in finite dimension: a surjectiv
 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
@@ -31,6 +31,16 @@ This concept is used to give an equivalent definition of immersions and submersi
   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.hasRightInverse` and `ContinuousLinearEquiv.hasRightInverse`:
   a continuous linear equivalence admits a continuous left (resp. right) inverse
 * `ContinuousLinearMap.HasLeftInverse.comp`, `ContinuousLinearMap.HasRightInverse.comp`:
@@ -56,8 +66,6 @@ This concept is used to give an equivalent definition of immersions and submersi
 * 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
 
 -/
 
@@ -185,6 +193,72 @@ lemma of_injective_of_finiteDimensional [CompleteSpace 𝕜] [FiniteDimensional
 
 end NontriviallyNormedField
 
+/-! An equivalent characterisation of maps with a continuous left inverse -/
+section Ring
+
+-- The next lemmas assume we are working over a ring.
+variable {R E E' F F' G : Type*} [Ring R]
+  [TopologicalSpace E] [AddCommGroup E] [Module R E]
+  [TopologicalSpace F] [AddCommGroup F] [Module R F] {f : E →L[R] F}
+
+/-- If `f` has a continuous left inverse, its range admits a closed complement. -/
+lemma closedComplemented_range (hf : f.HasLeftInverse) : Submodule.ClosedComplemented f.range := by
+  -- Idea of proof: let g be a left inverse for f. Then ker g is a closed subspace of F,
+  -- and a complement to range f.
+  -- Mathlib's definition of closed complement takes a continuous projection to f.range instead
+  -- of a complementary subspace: consider `f.comp g` instead, which is continuous as both maps are,
+  -- and idempotent as a continuous left inverse.
+  use (f.comp hf.leftInverse).codRestrict f.range (by intro y; simp)
+  rintro ⟨y, x, rfl⟩
+  ext
+  simp only [coe_coe, coe_codRestrict_apply, coe_comp', Function.comp_apply]
+  rw [hf.leftInverse_leftInverse]
+
+section
+
+variable [T1Space F]
+
+lemma isClosed_range (hf : f.HasLeftInverse) [IsTopologicalAddGroup F] :
+    IsClosed (range f) := by
+  -- `range f = ker (f ∘ g - id)` is closed since `f ∘ g - id` is continuous.
+  rw [← f.range_toLinearMap, ← f.coe_range,
+    f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)]
+  exact ((f.comp hf.leftInverse) - (ContinuousLinearMap.id R F)).isClosed_ker
+
+/-- Choice of a closed complement of `range f` -/
+def complement (h : f.HasLeftInverse) : Submodule R F :=
+  h.closedComplemented_range.complement
+
+lemma isClosed_complement (h : f.HasLeftInverse) : IsClosed (X := F) h.complement :=
+  h.closedComplemented_range.isClosed_complement
+
+lemma isCompl_complement (h : f.HasLeftInverse) : IsCompl f.range h.complement :=
+  h.closedComplemented_range.isCompl_complement
+
+end
+
+end Ring
+
+section
+
+variable {R E F : Type*} [NontriviallyNormedField R]
+  [NormedAddCommGroup E] [NormedSpace R E] [CompleteSpace E]
+  [NormedAddCommGroup F] [NormedSpace R F] [CompleteSpace F]
+
+/-- A continuous linear map between Banach spaces has a continuous left inverse if it isjective,
+has closed range and its range has a closed complement. -/
+lemma of_injective_of_isClosed_range_of_closedComplement_range {f : E →L[R] F}
+    (hf : Injective f) (hf' : IsClosed (range f)) (hf'' : Submodule.ClosedComplemented f.range) :
+    f.HasLeftInverse := by
+  have : (f.rangeRestrict).ker = ⊥ := by
+    rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf
+  -- We compose the continuous inverse of `f : E → range f` with the projection `p : F → range f`.
+  obtain ⟨p, hp⟩ := hf''
+  refine ⟨(f.leftInverse_of_injective_of_isClosed_range hf hf').comp p, fun x ↦ ?_⟩
+  simpa [hp ⟨f x, by simp⟩] using f.rangeRestrict.leftInverse_apply_of_inj this x
+
+end
+
 end HasLeftInverse
 
 namespace HasRightInverse
@@ -214,7 +288,7 @@ lemma _root_.ContinuousLinearEquiv.hasRightInverse (f : E ≃L[R] F) :
   ext y
   exact f.injective <| by simpa using f.hasRightInverse.rightInverse_rightInverse y
 
-/-- An invertible continuous linear map splits. -/
+/-- An invertible continuous linear map has a continuous right inverse. -/
 lemma of_isInvertible (hf : IsInvertible f) : f.HasRightInverse := by
   obtain ⟨e, rfl⟩ := hf
   exact e.hasRightInverse

Mathlib/Analysis/Normed/Operator/Banach.lean

@@ -375,14 +375,25 @@ variable {E F : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
   [CompleteSpace E] [CompleteSpace F]
 
--- TODO: once mathlib has Fredholm operators, generalise the next two lemmas accordingly
+-- TODO: once mathlib has Fredholm operators, generalise the next four lemmas accordingly
 
 /-- If `f : E →L[𝕜] F` is injective with closed range (and `E` and `F` are Banach spaces),
 `f` is anti-Lipschitz. -/
 lemma antilipschitz_of_injective_of_isClosed_range (f : E →L[𝕜] F)
     (hf : Injective f) (hf' : IsClosed (Set.range f)) : ∃ K, AntilipschitzWith K f :=
   ⟨_, .comp (.subtype_coe (Set.range f)) (f.equivRange hf hf').antilipschitz⟩
 
+/-- A choice of anti-Lipschitz constant for `f : E →L[𝕜] F` injective with closed range
+(assuming `E` and `F` are Banach spaces). -/
+noncomputable def antilipschitzConstant_of_injective_of_isClosed_range (f : E →L[𝕜] F)
+    (hf : Injective f) (hf' : IsClosed (Set.range f)) : ℝ≥0 :=
+  Classical.choose (f.antilipschitz_of_injective_of_isClosed_range hf hf')
+
+lemma antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range (f : E →L[𝕜] F)
+    (hf : Injective f) (hf' : IsClosed (Set.range f)) :
+    AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') f :=
+  Classical.choose_spec (f.antilipschitz_of_injective_of_isClosed_range hf hf')
+
 /-- An injective bounded linear operator between Banach spaces has closed range
 iff it is anti-Lipschitz. -/
 lemma isClosed_range_iff_antilipschitz_of_injective (f : E →L[𝕜] F)
@@ -391,6 +402,23 @@ lemma isClosed_range_iff_antilipschitz_of_injective (f : E →L[𝕜] F)
   choose K hf' using h
   exact hf'.isClosed_range f.uniformContinuous
 
+/-- A choice of continuous left inverse of an injective continuous linear map with closed range:
+this is `LinearMap.leftInverse` as a continuous linear map;
+by injectivity, the junk value of `leftInverse` never matters, and continuity of the inverse
+follows form the closed range condition. -/
+noncomputable def leftInverse_of_injective_of_isClosed_range
+    (f : E →L[𝕜] F) (hf : Injective f) (hf' : IsClosed (range f)) : f.range →L[𝕜] E :=
+  letI K := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
+  letI hfK := f.antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range hf hf'
+  LinearMap.mkContinuous f.rangeRestrict.leftInverse K (by
+    rintro ⟨y, x, rfl⟩
+    have aux := hfK.le_mul_dist x 0
+    simp only [dist_zero_right, map_zero] at aux
+    convert aux
+    exact f.rangeRestrict.leftInverse_apply_of_inj
+      (by rw [ker_codRestrict]; exact LinearMap.ker_eq_bot.mpr hf) x
+  )
+
 end
 
 end ContinuousLinearMap

Mathlib/Topology/Algebra/Module/LinearMap.lean

@@ -155,6 +155,10 @@ initialize_simps_projections ContinuousLinearMap (toFun → apply, toLinearMap 
 theorem ext {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
+@[simp, norm_cast]
+theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f :=
+  rfl
+
 /-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : M₁ →SL[σ₁₂] M₂ where
@@ -178,6 +182,8 @@ theorem range_coeFn_eq :
   · rintro ⟨hfc, f, rfl⟩
     exact ⟨⟨f, hfc⟩, rfl⟩
 
+lemma range_toLinearMap (f : M₁ →SL[σ₁₂] M₂) : Set.range f.toLinearMap = Set.range f := by simp
+
 -- make some straightforward lemmas available to `simp`.
 protected theorem map_zero (f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0 :=
   map_zero f
@@ -198,10 +204,6 @@ theorem map_smul_of_tower {R S : Type*} [Semiring S] [SMul R M₁] [Module S M
     f (c • x) = c • f x :=
   LinearMap.CompatibleSMul.map_smul (f : M₁ →ₗ[S] M₂) c x
 
-@[simp, norm_cast]
-theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f :=
-  rfl
-
 @[ext]
 theorem ext_ring [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g :=
   coe_inj.1 <| LinearMap.ext_ring h
@@ -1181,18 +1183,35 @@ open ContinuousLinearMap
 def ClosedComplemented (p : Submodule R M) : Prop :=
   ∃ f : M →L[R] p, ∀ x : p, f x = x
 
-theorem ClosedComplemented.exists_isClosed_isCompl {p : Submodule R M} [T1Space p]
-    (h : ClosedComplemented p) :
+variable {p : Submodule R M}
+
+namespace ClosedComplemented
+
+variable [T1Space p]
+
+theorem exists_isClosed_isCompl (h : ClosedComplemented p) :
     ∃ q : Submodule R M, IsClosed (q : Set M) ∧ IsCompl p q :=
   Exists.elim h fun f hf => ⟨ker f, isClosed_ker f, LinearMap.isCompl_of_proj hf⟩
 
-protected theorem ClosedComplemented.isClosed [IsTopologicalAddGroup M] [T1Space M]
+/-- An arbitrary choice of closed complement of a closed complemented submodule. -/
+noncomputable def complement (h : ClosedComplemented p) : Submodule R M :=
+  Classical.choose h.exists_isClosed_isCompl
+
+theorem isClosed_complement (h : ClosedComplemented p) : IsClosed (h.complement : Set M) :=
+  Classical.choose_spec (h.exists_isClosed_isCompl) |>.1
+
+theorem isCompl_complement (h : ClosedComplemented p) : IsCompl p h.complement :=
+  Classical.choose_spec (h.exists_isClosed_isCompl) |>.2
+
+protected theorem isClosed [IsTopologicalAddGroup M] [T1Space M]
     {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M) := by
   rcases h with ⟨f, hf⟩
   have : (ContinuousLinearMap.id R M - p.subtypeL.comp f).ker = p :=
     LinearMap.ker_id_sub_eq_of_proj hf
   exact this ▸ isClosed_ker _
 
+end ClosedComplemented
+
 @[simp]
 theorem closedComplemented_bot : ClosedComplemented (⊥ : Submodule R M) :=
   ⟨0, fun x => by simp only [zero_apply, eq_zero_of_bot_submodule x]⟩