Modulize; adjust for current mathlib; adjust deprecations; minor adjustments

grunweg · grunweg · commit 78dc2d53f2fc · 2026-01-30T22:45:32.000+01:00
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2076,6 +2076,7 @@ public import Mathlib.Analysis.NormedSpace.FunctionSeries
 public import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 public import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
 public import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
+public import Mathlib.Analysis.NormedSpace.HahnBanach.Splits
 public import Mathlib.Analysis.NormedSpace.HomeomorphBall
 public import Mathlib.Analysis.NormedSpace.IndicatorFunction
 public import Mathlib.Analysis.NormedSpace.Int
diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Splits.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Splits.lean
@@ -3,8 +3,10 @@ Copyright (c) 2025 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
-import Mathlib.Analysis.Normed.Module.Complemented
-import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
+module
+
+public import Mathlib.Analysis.Normed.Module.Complemented
+public import Mathlib.Analysis.Normed.Module.HahnBanach
 
 /-! # Linear maps which split
 
@@ -19,6 +21,8 @@ This concept is used to give a conceptual definition of immersions between Banac
 
 -/
 
+public section
+
 open Function Set
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E E' F F' G : Type*}
@@ -28,20 +32,11 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E E' F F' G : Type*}
 
 noncomputable section
 
-namespace LinearMap
-
-lemma range_prodMap {f : E →L[𝕜] F} {g : E' →L[𝕜] F'} :
-    range (f.prodMap g) = (range f).prod (range g) := by
-  ext x
-  simp [Prod.ext_iff]
-
-lemma _root_.Submodule.map_add {f : E →L[𝕜] F} {p q : Submodule 𝕜 E} :
-    Submodule.map f p + Submodule.map f q = Submodule.map f (p + q) := by
+lemma Submodule.map_add {f : E →L[𝕜] F} {p q : Submodule 𝕜 E} :
+    p.map (f : E →ₛₗ[.id _] F) + q.map (f : E →ₛₗ[.id _] F) = (p + q).map (f : E →ₛₗ[.id _] F) := by
   ext x
   simp
 
-end LinearMap
-
 section
 
 variable {R M N : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
@@ -63,7 +58,7 @@ end
 /-- A continuous linear map `f : E → F` **splits** iff it is injective, has closed range and
 its image has a closed complement. -/
 protected def ContinuousLinearMap.Splits (f : E →L[𝕜] F) : Prop :=
-  Injective f ∧ IsClosed (Set.range f) ∧ Submodule.ClosedComplemented (LinearMap.range f)
+  Injective f ∧ IsClosed (Set.range f) ∧ Submodule.ClosedComplemented (f.range)
 
 -- XXX: should this be about ContinuousLinearMapClass?
 namespace ContinuousLinearMap.Splits
@@ -74,7 +69,7 @@ lemma injective (h : f.Splits) : Injective f := h.1
 
 lemma isClosed_range (h : f.Splits) : IsClosed (Set.range f) := h.2.1
 
-lemma closedComplemented (h : f.Splits) : Submodule.ClosedComplemented (LinearMap.range f) :=
+lemma closedComplemented (h : f.Splits) : Submodule.ClosedComplemented (f.range) :=
   h.2.2
 
 /-- Choice of a closed complement of `range f` -/
@@ -84,7 +79,7 @@ def complement (h : f.Splits) : Submodule 𝕜 F :=
 lemma complement_isClosed (h : f.Splits) : IsClosed (X := F) h.complement :=
   (Classical.choose_spec h.closedComplemented.exists_isClosed_isCompl).1
 
-lemma complement_isCompl (h : f.Splits) : IsCompl (LinearMap.range f) h.complement :=
+lemma complement_isCompl (h : f.Splits) : IsCompl f.range h.complement :=
   (Classical.choose_spec h.closedComplemented.exists_isClosed_isCompl).2
 
 lemma congr {g : E →L[𝕜] F} (hf : f.Splits) (hfg : g = f) : g.Splits :=
@@ -97,24 +92,19 @@ lemma _root_.ContinuousLinearEquiv.splits (f : E ≃L[𝕜] F) : f.toContinuousL
     apply EquivLike.injective
   · rw [f.coe_coe, EquivLike.range_eq_univ]
     exact isClosed_univ
-  · erw [LinearMap.range_eq_top_of_surjective f (EquivLike.surjective f)]
+  · erw [f.range_eq_top_of_surjective (EquivLike.surjective f)]
     exact Submodule.closedComplemented_top
 
 /-- If `f` and `g` split, then so does `f × g`. -/
 lemma prodMap (hf : f.Splits) (hg : g.Splits) : (f.prodMap g).Splits := by
   refine ⟨hf.injective.prodMap hg.injective, ?_, ?_⟩
-  · rw [coe_prodMap', range_prod_map]
+  · rw [coe_prodMap', range_prodMap]
     exact (hf.isClosed_range).prod hg.isClosed_range
-  · rw [LinearMap.range_prodMap]
-    exact hf.closedComplemented.prod hg.closedComplemented
+  · simpa using hf.closedComplemented.prod hg.closedComplemented
 
-section RCLike
+section
 
-variable {𝕜 : Type*} [RCLike 𝕜] {E E' F F' G : Type*}
-  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
-  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
-  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
-  [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] {f : E →L[𝕜] F} {g : E' →L[𝕜] F'}
+variable [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
 
 /-- If `f : E → F` splits and `E`, `F` are real or complex Banach spaces, `f` is anti-Lipschitz.
 This result is unseful to prove that the composition of split maps is a split map. -/
@@ -131,9 +121,9 @@ lemma isClosedMap (hf : f.Splits) : IsClosedMap f :=
   (hf.antilipschitzWith.isClosedEmbedding f.uniformContinuous).isClosedMap
 
 omit [CompleteSpace F] [CompleteSpace G] in
-lemma disjoint_aux  {g : F →L[𝕜] G} {F₁ F₂ : Submodule 𝕜 F} {G' : Submodule 𝕜 G}
-    (hF : Disjoint F₁ F₂) (hG' : Disjoint (LinearMap.range g) G') (hg : Injective g) :
-    Disjoint (Submodule.map g F₁) (Submodule.map g F₂ + G') := by
+lemma disjoint_aux {g : F →L[𝕜] G} {F₁ F₂ : Submodule 𝕜 F} {G' : Submodule 𝕜 G}
+    (hF : Disjoint F₁ F₂) (hG' : Disjoint g.range G') (hg : Injective g) :
+    Disjoint (F₁.map (g : F →ₛₗ[.id _] G)) (F₂.map (g : F →ₛₗ[.id _] G) + G') := by
   rw [Submodule.disjoint_def] at hF hG' ⊢
   intro x h1 h2
   -- Write x = g (f x₀)
@@ -149,6 +139,7 @@ lemma disjoint_aux  {g : F →L[𝕜] G} {F₁ F₂ : Submodule 𝕜 F} {G' : Su
   have : z ∈ range g := by
     rw [this, ← hgx₀, ← hgy₀, ← map_sub]
     use x₀ - y₀ -- Can or should this be a simproc?
+    simp only [map_sub, coe_coe]
   have : z = 0 := hG' z this hz
   -- g y₀ = y = x = g x₀, thus x₀ = y₀.
   have hxy : x = y := by rw [← add_zero y, ← this, hxyz]
@@ -160,16 +151,27 @@ lemma disjoint_aux  {g : F →L[𝕜] G} {F₁ F₂ : Submodule 𝕜 F} {G' : Su
   have : y₀ = 0 := hF y₀ ((hg aux) ▸ hx₀) hy₀
   simp [hxy, ← hgy₀, this]
 
+end
+
+section RCLike
+
+variable {𝕜 : Type*} [RCLike 𝕜] {E E' F F' G : Type*}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
+  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+  [CompleteSpace E] [CompleteSpace F] [CompleteSpace G] {f : E →L[𝕜] F} {g : E' →L[𝕜] F'}
+
 /-- The composition of split continuous linear maps between real or complex Banach spaces splits. -/
-lemma comp {g : F →L[𝕜] G} (hg : g.Splits) (hf : f.Splits)  : (g.comp f).Splits := by
+lemma comp {g : F →L[𝕜] G} (hg : g.Splits) (hf : f.Splits) : (g.comp f).Splits := by
   have h : IsClosed (range (g ∘ f)) := by
     rw [range_comp]
     apply hg.isClosedMap _ hf.isClosed_range
   refine ⟨hg.injective.comp hf.injective, h, ?_⟩
   · rw [Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl]
     let F' := hf.complement
-    refine ⟨h, (F'.map g) + hg.complement, ?_, ?_⟩
-    · have : IsClosed (X := G) (F'.map g) := hg.isClosedMap _ hf.complement_isClosed
+    refine ⟨h, (F'.map (g : F →ₛₗ[.id _] G)) + hg.complement, ?_, ?_⟩
+    · have : IsClosed (X := G) (F'.map (g : F →ₛₗ[.id _] G)) :=
+        hg.isClosedMap _ hf.complement_isClosed
       have : IsClosed (X := G) hg.complement := hg.complement_isClosed
       -- In general, the sum of closed subspaces need not be closed.
       -- In this case, however, this is true as F'.map G is a closed subspace of range g,
@@ -182,7 +184,7 @@ lemma comp {g : F →L[𝕜] G} (hg : g.Splits) (hf : f.Splits)  : (g.comp f).Sp
       intro u u₀ hu hconv
       simp_rw [Submodule.add_eq_sup, SetLike.mem_coe, Submodule.mem_sup] at hu
       -- Write u_n = x_n + y_n, for x_n in g(F') and y_n in G'.
-      let x : ℕ → Submodule.map g F' := by
+      let x : ℕ → Submodule.map (g : F →ₛₗ[.id _] G) F' := by
         intro n
         choose y hy z hz hyz using hu n
         exact ⟨y, hy⟩
@@ -191,7 +193,7 @@ lemma comp {g : F →L[𝕜] G} (hg : g.Splits) (hf : f.Splits)  : (g.comp f).Sp
         choose y hy z hz hyz using hu n
         exact ⟨z, hz⟩
       -- By construction, u_n = x_n + y_n.
-      have (n) : u n = x n + y n := by
+      have (n : ℕ) : u n = x n + y n := by
         simp [x, y]
         sorry -- need more API lemmas
       -- x equals the projection into g(F'); y equals the projection onto hg.complement.
@@ -203,15 +205,16 @@ lemma comp {g : F →L[𝕜] G} (hg : g.Splits) (hf : f.Splits)  : (g.comp f).Sp
       -- Thus, by continuity, x_n converges to some point in g(F').
       -- By linearity, u_n converges to a point in g(F')+G', qed.
       sorry
-    · have : LinearMap.range (g.comp f) = Submodule.map g (LinearMap.range f) := by aesop
+    · have : LinearMap.range (g.comp f : E →ₛₗ[.id _] G) = f.range.map (g : F →ₛₗ[.id _] G) := by
+        aesop
       -- some lemmas which could be useful for a manual proof:
       -- rw [LinearMap.range_comp]; rw [LinearMap.range_eq_map]; rw [Submodule.map_comp f g ⊤]
       -- rw [← LinearMap.range_eq_map f]
       constructor
       · exact this ▸ disjoint_aux hf.complement_isCompl.1 hg.complement_isCompl.1 hg.injective
       · rw [codisjoint_iff, this, ← Submodule.add_eq_sup, Submodule.sum_assoc, Submodule.map_add]
         rw [LinearMap.range_eq_map]
-        trans Submodule.map g ⊤ + hg.complement
+        trans Submodule.map (g : F →ₛₗ[.id _] G) ⊤ + hg.complement
         · congr
           rw [Submodule.add_eq_sup, ← codisjoint_iff]
           simpa using hf.complement_isCompl.2
@@ -230,15 +233,16 @@ omit [CompleteSpace E] [CompleteSpace F] [CompleteSpace G]
 
 /-- If `f : E → F` is injective and `F` is finite-dimensional, then `f` splits. -/
 lemma of_injective_of_finiteDimensional [FiniteDimensional 𝕜 F] (hf : Injective f) : f.Splits := by
-  have aux : IsClosed (X := F) (LinearMap.range f) := Submodule.closed_of_finiteDimensional _
-  exact ⟨hf, aux, Submodule.ClosedComplemented.of_finiteDimensional (LinearMap.range f)⟩
+  have aux : IsClosed (X := F) f.range := Submodule.closed_of_finiteDimensional _
+  exact ⟨hf, aux, Submodule.ClosedComplemented.of_finiteDimensional f.range⟩
 
 /-- If `f : E → F` is injective and `E` is finite-dimensional, then `f` splits. -/
 lemma of_injective_of_finiteDimensional_of_completeSpace
     [FiniteDimensional 𝕜 E] (hf : Injective f) : f.Splits := by
-  have aux : IsClosed (X := F) (LinearMap.range f) := Submodule.closed_of_finiteDimensional _
-  exact ⟨hf, aux, Submodule.ClosedComplemented.of_finiteDimensional (LinearMap.range f)⟩
+  have aux : IsClosed (X := F) f.range := Submodule.closed_of_finiteDimensional _
+  exact ⟨hf, aux, Submodule.ClosedComplemented.of_finiteDimensional f.range⟩
 
+-- FUTURE (once mathlib has a notion of Fredholm operators):
 -- If `f : E → F` is injective, `E` and `F` are Banach and `f` is Fredholm, then `f` splits.
 
 end RCLike
