[Merged by Bors] - feat: injectivity of continuous linear maps is an open condition

[grunweg]

in finite-dimensional spaces over a complete field. This is used to showing that immersions are open.
NB: this result is false for general continuous maps (only surjectivity is open there).

From the sphere-eversion project.

---

Placing the lemmas about normed groups is tricky (their natural place is Normed/Group/Basic, but they also require the topology on NNReal...). Better solutions welcome.

Aside: I don't see a good label for this; I would label with "baby differential topology" if I could.

---

[j-loreaux]

I'll note that you can get your result directly without going directly through AntiLipschitz (although ultimately it is using it under the hood somewhere), in the following way:

theorem isOpen_setOf_clm_injective [FiniteDimensional 𝕜 E] :
    IsOpen { f : E →L[𝕜] F | Function.Injective f } := by
  suffices this : ∀ (f : E →L[𝕜] F), Function.Injective f ↔ finrank 𝕜 E ≤ (f : E →ₗ[𝕜] F).rank by
    simpa [this] using isOpen_setOf_nat_le_rank (finrank 𝕜 E)
  simp_rw [LinearMap.rank, ← finrank_eq_rank]
  refine fun f ↦ ⟨by exact_mod_cast (LinearMap.finrank_range_of_inj · |>.symm |>.le), ?_⟩
  norm_cast
  rw [← add_zero (finrank 𝕜 (LinearMap.range (f : E →ₗ[𝕜] F))),
    ← f.finrank_range_add_finrank_ker]
  exact fun hf ↦ (LinearMapClass.ker_eq_bot (E →L[𝕜] F)).mp <| by
    simpa using Nat.eq_zero_of_le_zero (le_of_add_le_add_left hf)

That being said, I think we want the other results in this PR anyway, so no need to change your proof.

[grunweg]

Thank you for the useful comments. I have addressed them, so this is ready for another look.
awaiting-review

[j-loreaux]

@grunweg it's missing the new import

[j-loreaux]

bors d+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Indeed, thanks. Fixed now.
bors r+

[mathlib-bors]

Canceled.

[grunweg]

No idea why the build was cancelled again ("merge conflict"? certainly not with my PR). In any case, let's try merging master.
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style