Continuous linear maps with closed range

Stream: Is there code for X?

[Michael Rothgang]

It seems we really don't have this - or am I missing something?

[Michael Rothgang]

@loogle ContinuousLinearMap, IsClosedMap

[loogle]

:shrug: nothing found

[Michael Rothgang]

@loogle ContinuousLinearMap, "IsClosed" also yields nothing relevant

[loogle]

:exclamation:

function expected at
  "IsClosed"
term has type
  String

[Yury G. Kudryashov]

What assumptions on the spaces do you have in mind?

[Michael Rothgang]

General normed spaces - assuming Banach is fine for my setting.

[Sébastien Gouëzel]

That's just not true. Consider the inclusion of $C^1$ functions in $C^0$ functions. It is a continuous linear maps, but the range is not closed.

[Michael Rothgang]

Never mind: I need further conditions, see https://math.stackexchange.com/questions/26071/when-is-the-image-of-a-linear-operator-closed?noredirect=1.

[Michael Rothgang]

Indeed - thanks.

[Notification Bot]

Michael Rothgang has marked this topic as resolved.

[Jireh Loreaux]

Note, we have docs#AntilipschitzWith.isClosed_range, and docs#ContinuousLinearMap.antilipschitz_of_bound, and docs#ContinuousLinearMap.antilipschitz_of_forall_le_inner_map which may help you out.

[Michael Rothgang]

I have now opened #23175 with the result I need: there is one open sorry that eludes me, though. MWE is the following:

import Mathlib.Analysis.Normed.Operator.Banach

variable {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜']
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜' F]
  [CompleteSpace E] [CompleteSpace F]

variable  {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [RingHomInvPair σ' σ]

@[simp]
lemma ContinuousLinearMap.equivRange_symm (f : E →SL[σ] F) (hinj : Function.Injective f) (hclo : IsClosed (Set.range f)) :
    (f.equivRange hinj hclo).symm.toLinearEquiv =
      (LinearEquiv.ofInjective f.toLinearMap hinj).symm := by
  rfl

@[simp]
lemma ContinuousLinearMap.equivRange_symm_apply (f : E →SL[σ] F) (hinj : Function.Injective f) (hclo : IsClosed (Set.range f))
    (x : E) : (f.equivRange hinj hclo).symm ⟨f x, by simp⟩ = x := by
  suffices f ((f.equivRange hinj hclo).symm ⟨f x, by simp⟩) = f x from hinj this
  trans f ((f.equivRange hinj hclo).symm.toLinearEquiv ⟨f x, by simp⟩)
  · rfl -- is there an API lemma for this already?
  dsimp only [equivRange_symm]
  --apply LinearEquiv.ofInjective_symm_apply hinj
  set x' : LinearMap.range f := ⟨f x, by simp⟩
  -- rw [LinearEquiv.ofInjective_symm_apply f (h := hinj) x']
  -- #check LinearEquiv.ofInjective_symm_apply f (h := hinj) x'
  -- goal state: f ((LinearEquiv.ofInjective (↑f) hinj).symm x') = f x
  sorry

[Michael Rothgang]

LinearEquiv.ofInjective_symm_apply looks like it should help, but trying to apply it makes the kernel think for a long time, and produce an error I don't the reason of. It's probably something relatively simple...

[Notification Bot]

Michael Rothgang has marked this topic as unresolved.

[Ruben Van de Velde]

Nasty, but works:

import Mathlib.Analysis.Normed.Operator.Banach

variable {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜']
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜' F]
  [CompleteSpace E] [CompleteSpace F]

variable  {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ'] [RingHomInvPair σ' σ]

@[simp]
lemma ContinuousLinearMap.equivRange_symm (f : E →SL[σ] F) (hinj : Function.Injective f) (hclo : IsClosed (Set.range f)) :
    (f.equivRange hinj hclo).symm.toLinearEquiv =
      (LinearEquiv.ofInjective f.toLinearMap hinj).symm := by
  rfl

@[simp]
lemma ContinuousLinearMap.equivRange_symm_apply (f : E →SL[σ] F) (hinj : Function.Injective f) (hclo : IsClosed (Set.range f))
    (x : E) : (f.equivRange hinj hclo).symm ⟨f x, by simp⟩ = x := by
  suffices f ((f.equivRange hinj hclo).symm ⟨f x, by simp⟩) = f x from hinj this
  trans f ((f.equivRange hinj hclo).symm.toLinearEquiv ⟨f x, by simp⟩)
  · rfl -- is there an API lemma for this already?
  dsimp only [equivRange_symm]
  --apply LinearEquiv.ofInjective_symm_apply hinj
  set x' : LinearMap.range f := ⟨f x, by simp⟩
  set f' : E →ₛₗ[σ] F := ↑f
  replace hinj : Function.Injective f' := hinj
  change f' ((LinearEquiv.ofInjective (f') hinj).symm x') = _
  rw [LinearEquiv.ofInjective_symm_apply (f := f') (h := hinj) x']

[Michael Rothgang]

Thanks a lot! I've pushed your fix, slightly edited to the PR - which is now ready for review.