Name for the continuous linear functionals of a topological

Stream: mathlib4

[Christopher Hoskin]

Currently, we have the abbrev NormedSpace.Dual 𝕜 E for the space of continuous linear functionals on a NormedSpace 𝕜 E (i.e. E →L[𝕜] 𝕜).

However, one often wants to work with the continuous linear functionals on a more general topological vector space (e.g. #26345) and one could relax the requirements for the abbrev to

abbrev NormedSpace.Dual (R : Type*) [Semiring R] [TopologicalSpace R]
  (M : Type*) [TopologicalSpace M] [AddCommMonoid M] [Module R M] : Type _ := M →L[R] R

However, the name NormedSpace.Dual feels wrong when the space isn't equipped with a distinguished seminorm.

In pen and paper maths, I've always called E →L[𝕜] 𝕜 the "topological dual" and E →ₗ[𝕜] 𝕜 the "algebraic dual".

@Jireh Loreaux has suggested the name StrongDual [1].

In #27699 I've currently redefined NormedSpace.Dual as:

variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
variable (E : Type*) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
...
abbrev NormedSpace.Dual : Type _ := StrongDual 𝕜 E

But there's a question about whether we want to keep NormedSpace.Dual or replace it entirely with StrongDual?

Thanks

Christopher

[1] https://en.wikipedia.org/wiki/Strong_dual_space

[Yaël Dillies]

I personally think NormedSpace.dual is a not-so-enlightening name, so I'm happy to see it go in favor of StrongDual

[Jireh Loreaux]

Can we have some additional input? Maybe from @Frédéric Dupuis, @Monica Omar, @Anatole Dedecker, or @Sébastien Gouëzel, just to ping a few people?

[Frédéric Dupuis]

StrongDual sounds good. We should definitely stick to only one name though, having two spellings for the same thing only gives headaches down the road.

[Christopher Hoskin]

Now that we have this abbreviation, would it be a useful exercise for me to look for occurrences of the pattern E→L[R] R etc and replace them with StrongDual R E?

ie. https://github.com/leanprover-community/mathlib4/pull/28726