Spaces with separating dual #
We introduce a typeclass SeparatingDual R V
, registering that the points of the topological
module V
over R
can be separated by continuous linear forms.
This property is satisfied for normed spaces over ℝ
or ℂ
(by the analytic Hahn-Banach theorem)
and for locally convex topological spaces over ℝ
(by the geometric Hahn-Banach theorem).
Under the assumption SeparatingDual R V
, we show in
SeparatingDual.exists_continuousLinearMap_apply_eq
that the group of continuous linear
equivalences acts transitively on the set of nonzero vectors.
Any nonzero vector can be mapped by a continuous linear map to a nonzero scalar.
When E
is a topological module over a topological ring R
, the class SeparatingDual R E
registers that continuous linear forms on E
separate points of E
.
Instances
In a topological vector space with separating dual, the group of continuous linear equivalences
acts transitively on the set of nonzero vectors: given two nonzero vectors x
and y
, there
exists A : V ≃L[R] V
mapping x
to y
.