feat(Analysis.LocallyConvex): a linear map is surjective iff its image contains a ball, or a closed ball, or a sphere (leanprover-community#29033)

Prove that a linear map is surjective if and only if its image contains either a ball or a sphere.

Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: faenuccio

Mathlib/Analysis/Convex/Basic.lean

@@ -3,12 +3,9 @@ Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov, Yaël Dillies
 -/
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
-import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Ring.Action.Pointwise.Set
 import Mathlib.Analysis.Convex.Star
 import Mathlib.Tactic.Field
-import Mathlib.Tactic.NoncommRing
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
 
 /-!
@@ -164,6 +161,8 @@ theorem convex_segment [IsOrderedRing 𝕜] (x y : E) : Convex 𝕜 [x -[𝕜] y
   · rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
   · match_scalars <;> noncomm_ring
 
+/-- See `Convex.semilinear_image` for a version for semilinar maps, but requiring that `𝕜` be a
+  linear order, instead of just a partial order. -/
 theorem Convex.linear_image (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s) := by
   rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
   exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
@@ -486,9 +485,29 @@ end AddCommGroup
 
 end OrderedRing
 
-section LinearOrderedSemiring
+section LinearOrder
 
-variable [Semiring 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E]
+variable [Semiring 𝕜] [AddCommMonoid E]
+section SemilinearMap
+
+variable [PartialOrder 𝕜]
+variable {𝕜' : Type*} [Semiring 𝕜'] [PartialOrder 𝕜']
+variable {σ : 𝕜 →+* 𝕜'} [RingHomSurjective σ]
+variable {F' : Type*} [AddCommMonoid F'] [Module 𝕜' F'] [Module 𝕜 E]
+
+theorem Convex.semilinear_image {s : Set E} (hs : Convex 𝕜 s) (hσ : ∀ {s t}, σ s ≤ σ t ↔ s ≤ t)
+    (f : E →ₛₗ[σ] F') : Convex 𝕜' (f '' s) := by
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
+  obtain ⟨r, rfl⟩ : ∃ r : 𝕜, σ r = a := RingHomSurjective.is_surjective ..
+  obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..
+  refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
+    ?_, by simp⟩
+  apply_fun σ using injective_of_le_imp_le _ hσ.mp
+  simpa
+
+end SemilinearMap
+
+variable [LinearOrder 𝕜] [IsOrderedRing 𝕜]
 
 theorem Convex_subadditive_le [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (x + y) ≤ (f x) + (f y))
     (hf2 : ∀ ⦃c⦄ x, 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) :
@@ -500,7 +519,7 @@ theorem Convex_subadditive_le [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (
     _ ≤ a • B + b • B := by gcongr <;> assumption
     _ ≤ B := by rw [← add_smul, hs, one_smul]
 
-end LinearOrderedSemiring
+end LinearOrder
 
 theorem Convex.midpoint_mem [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
     [AddCommGroup E] [Module 𝕜 E] [Invertible (2 : 𝕜)] {s : Set E} {x y : E}
@@ -590,6 +609,10 @@ protected theorem convex (K : Submodule 𝕜 E) : Convex 𝕜 (↑K : Set E) :=
 protected theorem starConvex (K : Submodule 𝕜 E) : StarConvex 𝕜 (0 : E) K :=
   K.convex K.zero_mem
 
+theorem Convex.semilinear_range {𝕜' : Type*} [Semiring 𝕜'] {σ : 𝕜' →+* 𝕜}
+  [RingHomSurjective σ] {F' : Type*} [AddCommMonoid F'] [Module 𝕜' F']
+  (f : F' →ₛₗ[σ] E) : Convex 𝕜 (LinearMap.range f : Set E) := Submodule.convex ..
+
 end Submodule
 
 section CommSemiring

Mathlib/Analysis/LocallyConvex/Basic.lean

@@ -3,12 +3,9 @@ Copyright (c) 2019 Jean Lo. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo, Bhavik Mehta, Yaël Dillies
 -/
-import Mathlib.Analysis.Convex.Basic
 import Mathlib.Analysis.Convex.Hull
-import Mathlib.Analysis.Normed.Field.Lemmas
-import Mathlib.Analysis.Normed.MulAction
+import Mathlib.Analysis.Normed.Module.Basic
 import Mathlib.Topology.Bornology.Absorbs
-
 /-!
 # Local convexity
 
@@ -29,6 +26,12 @@ For a module over a normed ring:
   `s`.
 * `Balanced`: A set `s` is balanced if `a • s ⊆ s` for all `a` of norm less than `1`.
 
+## Main Results
+* `Absorbent.submodule_eq_top` shows that when the base field is nontrivially normed, an absorbent
+  submodule is actually the whole space. As an application, we show in
+  `Absorbent.subset_image_iff_surjective` that a linear function is surjective if and only if its
+  image contains an absorbent set.
+
 ## References
 
 * [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
@@ -253,8 +256,9 @@ end NormedField
 
 section NontriviallyNormedField
 
-variable [NontriviallyNormedField 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E}
+variable [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E}
 
+variable [PartialOrder 𝕜] in
 protected theorem Balanced.convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (convexHull 𝕜 s) := by
   suffices Convex 𝕜 { x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull 𝕜 s } by
     rw [balanced_iff_smul_mem] at hs ⊢
@@ -264,6 +268,29 @@ protected theorem Balanced.convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (co
   rw [smul_add, ← smul_comm u, ← smul_comm v]
   exact convex_convexHull 𝕜 s (hx a ha) (hy a ha) hu hv huv
 
+variable {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E]
+
+theorem Absorbent.eq_univ_of_smulMemClass {V : S} (hV : Absorbent 𝕜 (V : Set E)) :
+    (V : Set E) = univ := by
+  rw [eq_univ_iff_forall]
+  intro x
+  obtain ⟨c, hc, hc'⟩ :=
+    ((absorbent_iff_eventually_nhdsNE_zero.mp hV x).and eventually_mem_nhdsWithin).exists
+  rw [← inv_smul_smul₀ hc' x]
+  exact SMulMemClass.smul_mem c⁻¹ hc
+
+theorem Absorbent.submodule_eq_top {V : Submodule 𝕜 E} (hV : Absorbent 𝕜 (V : Set E)) :
+    V = ⊤ := (StrictMono.apply_eq_top_iff (α := Submodule 𝕜 E) (β := Set E) (fun _ _ a_1 ↦ a_1)).mp
+  hV.eq_univ_of_smulMemClass
+
+variable {F ℱ 𝕜₂ : Type*} [Semiring 𝕜₂] {σ : 𝕜₂ →+* 𝕜}
+variable [AddCommGroup F] [Module 𝕜₂ F]
+variable [FunLike ℱ F E] [SemilinearMapClass ℱ σ F E]
+
+theorem Absorbent.subset_range_iff_surjective [RingHomSurjective σ] {f : ℱ} {s : Set E}
+    (hs_abs : Absorbent 𝕜 s) : s ⊆ LinearMap.range f ↔ (⇑f).Surjective :=
+  ⟨fun hs_sub ↦ LinearMap.range_eq_top.mp ((hs_abs.mono hs_sub).submodule_eq_top), fun h a _ ↦ h a⟩
+
 end NontriviallyNormedField
 
 section Real

Mathlib/Analysis/Normed/Module/Convex.lean

@@ -8,6 +8,7 @@ import Mathlib.Analysis.Convex.PathConnected
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Normed.Group.Pointwise
 import Mathlib.Analysis.Normed.Module.Basic
+import Mathlib.Analysis.Normed.Module.RCLike.Real
 
 /-!
 # Metric properties of convex sets in normed spaces
@@ -61,6 +62,36 @@ theorem convex_ball (a : E) (r : ℝ) : Convex ℝ (Metric.ball a r) := by
 theorem convex_closedBall (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r) := by
   simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r
 
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+open Pointwise in
+theorem convexHull_sphere_eq_closedBall [Nontrivial F] (x : F) {r : ℝ} (hr : 0 ≤ r) :
+    convexHull ℝ (sphere x r) = closedBall x r := by
+  suffices convexHull ℝ (sphere (0 : F) r) = closedBall 0 r by
+    rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
+      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
+  refine subset_antisymm (convexHull_min sphere_subset_closedBall (convex_closedBall 0 r))
+    (fun x h ↦ mem_convexHull_iff.mpr fun U hU_sub hU ↦ ?_)
+  have zero_mem : (0 : F) ∈ U := by
+    have _ : Invertible (2 : ℝ) := by use 2⁻¹ <;> grind
+    obtain ⟨z, hz⟩ := NormedSpace.sphere_nonempty (E := F).mpr hr
+    rw [← midpoint_self_neg (R := ℝ) (x := z)]
+    exact Convex.midpoint_mem hU (hU_sub hz) <| hU_sub (by simp_all)
+  by_cases hr₀ : r = 0
+  · simp_all
+  by_cases x_zero : x = 0
+  · rwa [x_zero]
+  set z := (r * ‖x‖⁻¹) • x with hz_def
+  have hr₁ : r⁻¹ * ‖x‖ ≤ 1 := by
+    simp only [mem_closedBall, dist_zero_right] at h
+    grw [h, inv_mul_le_one]
+  have hz : z ∈ U := by
+    apply hU_sub
+    simp_all [norm_smul]
+  have := StarConvex.smul_mem (hU.starConvex zero_mem) hz (by positivity) hr₁
+  rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
+    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
+
 /-- Given a point `x` in the convex hull of `s` and a point `y`, there exists a point
 of `s` at distance at least `dist x y` from `y`. -/
 theorem convexHull_exists_dist_ge {s : Set E} {x : E} (hx : x ∈ convexHull ℝ s) (y : E) :

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
+import Mathlib.Analysis.Normed.Module.Convex
 import Mathlib.Topology.Algebra.Module.StrongTopology
 import Mathlib.Analysis.Normed.Operator.LinearIsometry
 import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
@@ -24,11 +25,15 @@ file `NormedSpace.lean`.
 Note that most of statements that apply to semilinear maps only hold when the ring homomorphism
 is isometric, as expressed by the typeclass `[RingHomIsometric σ]`.
 
+## Main Results
+* `ball_subset_range_iff_surjective` (and its variants) shows that a semi-linear map between normed
+  spaces is surjective if and only if it contains a ball.
+
 -/
 
 suppress_compilation
 
-open Bornology
+open Bornology Metric
 open Filter hiding map_smul
 open scoped NNReal Topology Uniformity
 
@@ -37,8 +42,6 @@ variable {𝕜 𝕜₂ 𝕜₃ E F Fₗ G 𝓕 : Type*}
 
 section SemiNormed
 
-open Metric ContinuousLinearMap
-
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup Fₗ]
   [SeminormedAddCommGroup G]
 
@@ -48,6 +51,41 @@ variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [Nontr
 
 variable [FunLike 𝓕 E F]
 
+section
+
+variable [SemilinearMapClass 𝓕 σ₁₂ E F]
+
+theorem ball_zero_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : 𝓕} {r : ℝ}
+    (hr : 0 < r) : ball 0 r ⊆ Set.range f ↔ (⇑f).Surjective :=
+  absorbent_ball (by simpa)|>.subset_range_iff_surjective
+
+theorem ball_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : 𝓕} {x : F} {r : ℝ}
+    (hr : 0 < r) : ball x r ⊆ Set.range f ↔ (⇑f).Surjective := by
+  refine ⟨fun h ↦ ?_, by simp_all⟩
+  suffices ball 0 r ⊆ Set.range f from (ball_zero_subset_range_iff_surjective hr).mp this
+  intro _ _
+  change _ ∈ LinearMap.range f --this can be avoided by replacing `rw` with `erw` in the next line
+  rw [← Submodule.add_mem_iff_left (p := LinearMap.range f) (h <| mem_ball_self hr)]
+  apply h
+  simp_all
+
+theorem closedBall_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : 𝓕} (x : F) {r : ℝ}
+    (hr : 0 < r) : closedBall (x : F) r ⊆ Set.range f ↔ (⇑f).Surjective :=
+  ⟨fun h ↦ (ball_subset_range_iff_surjective hr).mp <| subset_trans ball_subset_closedBall h,
+    by simp_all⟩
+
+variable {F' 𝓕' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] [Nontrivial F']
+{τ : 𝕜 →+* ℝ} [FunLike 𝓕' E F'] [SemilinearMapClass 𝓕' τ E F']
+
+theorem sphere_subset_range_iff_surjective [RingHomSurjective τ] {f : 𝓕'} {x : F'} {r : ℝ}
+    (hr : 0 < r) : sphere x r ⊆ Set.range f ↔ (⇑f).Surjective := by
+  refine ⟨fun h ↦ ?_, by simp_all⟩
+  grw [← (closedBall_subset_range_iff_surjective x hr), ← convexHull_sphere_eq_closedBall x
+    (le_of_lt hr), convexHull_mono h, (convexHull_eq_self (𝕜 := ℝ) (s := Set.range ↑f)).mpr]
+  exact Submodule.Convex.semilinear_range (E := F') (F' := E) (σ := τ) f
+
+end
+
 /-- If `‖x‖ = 0` and `f` is continuous then `‖f x‖ = 0`. -/
 theorem norm_image_of_norm_zero [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous f) {x : E}
     (hx : ‖x‖ = 0) : ‖f x‖ = 0 := by
@@ -235,7 +273,6 @@ theorem opNorm_le_of_shell {f : E →SL[σ₁₂] F} {ε C : ℝ} (ε_pos : 0 <
     (hc : 1 < ‖c‖) (hf : ∀ x, ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C :=
   f.opNorm_le_bound' hC fun _ hx => SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf hx
 
-
 theorem opNorm_le_of_ball {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
     (hf : ∀ x ∈ ball (0 : E) ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C := by
   rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩