Linear operator is surjective iff the range contains a ball

Stream: Is there code for X?

[Filippo A. E. Nuccio]

I am struggling to find a declaration saying that a linear map between normed spaces is surjective if and only if its image contains a ball. Of course we can strengthen/relax all assumptions and start playing with semi-linear almost-normed quasi-modules (and I will do so if I need to open a PR), but the result seems so basic (and the proof so short) that something along these lines ought to be there.

[Jireh Loreaux]

A quick search didn't return anything for me, but I would phrase this as "an absorbent submodule is ⊤", or something to this effect. Then docs#absorbent_ball and docs#Absorbent.mono would get you all the way there.

[Filippo A. E. Nuccio]

Excellent, thanks. I would have never thought at using sponges... :sponge:

[Filippo A. E. Nuccio]

Yet I would perhaps add a couple of explicit lemmas (whose proof would be the one you describe) so that future users might find them? Or do you prefer to avoid the "repetition"?

[Jireh Loreaux]

sure I think there should be the absorbent submodule → = ⊤ lemma, and a lemma (hs₁ : Absorbent 𝕜 s) (hs₂ : s ⊆ (LinearMap.range f)) t → Function.Surjective f (possibly rewritten as an ↔). A lemma specific to balls is also good, especially because the ball need not be centered at zero.

[Filippo A. E. Nuccio]

OK, I'll open the PR later tonight or tomorrow morning.

[Yi.Yuan]

I have this result in #29777,

lemma p34 {α β : Type*} [NormedAddCommGroup α] [NormedAddCommGroup β]
 [InnerProductSpace ℝ α] [InnerProductSpace ℝ β] (T : α →L[ℝ] β) {δ : ℝ}
 (h0 : δ > 0) (h : T '' (ball 0 1) ⊇ ball 0 δ) : (⇑T).Surjective

may be of some help

[Yi.Yuan]

Here is my proof, but there is a type sorry which is quite complicated.

example [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ₗ[𝕜] F) (s : Set F) :
    Absorbent 𝕜 s → s ⊆ Set.range f → (⇑f).Surjective := by
  intro hs_abs hs_sub y
  obtain ⟨r, rpos, hr⟩ := Absorbs.exists_pos (hs_abs y)
  simp at hr
  obtain ⟨a, ha⟩ : ∃ a : 𝕜, ‖a‖ ≥ r := by
    obtain ⟨b, hb⟩ := exists_int_ge r
    use b
    sorry
  have := hr a ha
  have ne : (a : 𝕜) ≠ 0 := by
    by_contra! nh
    simp [nh] at ha
    linarith
  rw [Set.mem_smul_set_iff_inv_smul_mem₀ ne] at this
  obtain ⟨x, hx⟩ : (a : 𝕜)⁻¹ • y ∈ range ⇑f := hs_sub this
  use (a : 𝕜) • x
  simpa [hx] using smul_inv_smul₀ ne y

[Yi.Yuan]

I think we should assume that NontriviallyNormedField 𝕜 to use NormedField.exists_lt_norm, but then the norms from [NontriviallyNormedField 𝕜] and [NormedSpace 𝕜 F] would conflict.

[Yi.Yuan]

see #29033

[Filippo A. E. Nuccio]

Thanks for your code! I've cleaned it up a bit and it is ready for review.

[Eric Wieser]

Yi.Yuan said:

but then the norms from [NontriviallyNormedField 𝕜] and [NormedSpace 𝕜 F] would conflict.

What do you mean by this?

[Filippo A. E. Nuccio]

It was also a bit unclear to me, but I found no "conflict".

[Filippo A. E. Nuccio]

I have finished the proofs (and also added the result for spheres, beyond open/closed balls).

[Yury G. Kudryashov]

I'm sorry for resuming the old thread. I think that the right statement behind this is: if a submodule in a TVS has a nonempty interior, then it's the whole space.

[Filippo A. E. Nuccio]

But do we already have explicit relations between being absorbent and having nonempty interior?

[Yury G. Kudryashov]

Indeed, the Absorbent version is more general, sorry. But it should be true for a TVS.

[Yury G. Kudryashov]

Here is a proof:

lemma SMulMemClass.eq_univ_of_absorbent {𝕜 E S : Type*}
    [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [SetLike S E] [SMulMemClass S 𝕜 E]
    (s : S) (hs : Absorbent 𝕜 (s : Set E)) : (s : Set E) = .univ := by
  rw [Set.eq_univ_iff_forall]
  intro x
  rcases (hs x).exists with ⟨c, hc⟩
  rcases hc (Set.mem_singleton _) with ⟨x, hx, rfl⟩
  exact smul_mem _ hx

[Yury G. Kudryashov]

We don't need any topology on E for this statement.

[Yury G. Kudryashov]

For "nonempty interior -> absorbent", we have docs#absorbent_nhds_zero. If we know that s belongs to nhds x, then x \in s and we have s = (-x) +_v s \in nhds 0.

[Filippo A. E. Nuccio]

This was already basically the argument, for submodules instead of SMulMemClass; I've updated the PR and taken into account a couple of suggestions from @Anatole Dedecker and @Jireh Loreaux . It is again ready for review.