Spaces with separating dual #
We introduce a typeclass
SeparatingDual R V, registering that the points of the topological
R can be separated by continuous linear forms.
This property is satisfied for normed spaces over
ℂ (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.
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
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
A : V ≃L[R] V mapping