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.

theorem separatingDual_def (R : Type u_1) (V : Type u_2) [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] : SeparatingDual R V ↔ ∀ (x : V), x ≠ 0 → ∃ (f : V →L[R] R), f x ≠ 0

class SeparatingDual (R : Type u_1) (V : Type u_2) [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] : Prop

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.

• exists_ne_zero' : ∀ (x : V), x ≠ 0 → ∃ (f : V →L[R] R), f x ≠ 0

  Any nonzero vector can be mapped by a continuous linear map to a nonzero scalar.

instance instSeparatingDualRealInstRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace {E : Type u_1} [TopologicalSpace E] [AddCommGroup E] [TopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T1Space E] : SeparatingDual ℝ E

Equations

• ⋯ = ⋯

instance instSeparatingDualToRingToNormedRingToNormedCommRingToNormedFieldToDenselyNormedFieldToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToModule {E : Type u_1} {𝕜 : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : SeparatingDual 𝕜 E

Equations

• ⋯ = ⋯

theorem SeparatingDual.exists_ne_zero {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] [SeparatingDual R V] {x : V} (hx : x ≠ 0) : ∃ (f : V →L[R] R), f x ≠ 0

theorem SeparatingDual.exists_separating_of_ne {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] [SeparatingDual R V] {x : V} {y : V} (h : x ≠ y) : ∃ (f : V →L[R] R), f x ≠ f y

theorem SeparatingDual.t1Space {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] [SeparatingDual R V] [T1Space R] : T1Space V

theorem SeparatingDual.t2Space {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [TopologicalSpace V] [TopologicalSpace R] [Module R V] [SeparatingDual R V] [T2Space R] : T2Space V

theorem separatingDual_iff_injective {R : Type u_1} {V : Type u_2} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V] [TopologicalRing R] [Module R V] : SeparatingDual R V ↔ Function.Injective ⇑(LinearMap.flip (ContinuousLinearMap.coeLM R))

theorem SeparatingDual.dualMap_surjective_iff {R : Type u_1} {V : Type u_2} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V] [TopologicalRing R] [Module R V] [SeparatingDual R V] {W : Type u_3} [AddCommGroup W] [Module R W] [FiniteDimensional R W] {f : W →ₗ[R] V} : Function.Surjective (⇑(LinearMap.dualMap f) ∘ ContinuousLinearMap.toLinearMap) ↔ Function.Injective ⇑f

Given a finite-dimensional subspace W of a space V with separating dual, any linear functional on W extends to a continuous linear functional on V. This is stated more generally for an injective linear map from W to V.

theorem SeparatingDual.exists_eq_one {R : Type u_1} {V : Type u_2} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V] [TopologicalRing R] [Module R V] [SeparatingDual R V] {x : V} (hx : x ≠ 0) : ∃ (f : V →L[R] R), f x = 1

theorem SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair {R : Type u_1} {V : Type u_2} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V] [TopologicalRing R] [Module R V] [SeparatingDual R V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (f : V →L[R] R), f x = 1 ∧ f y ≠ 0

theorem SeparatingDual.exists_continuousLinearEquiv_apply_eq {R : Type u_1} {V : Type u_2} [Field R] [AddCommGroup V] [TopologicalSpace R] [TopologicalSpace V] [TopologicalRing R] [TopologicalAddGroup V] [Module R V] [SeparatingDual R V] [ContinuousSMul R V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (A : V ≃L[R] V), A x = y

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.