Documentation

Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual

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] :

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.

Instances
    theorem SeparatingDual.exists_ne_zero' {R : Type u_1} {V : Type u_2} :
    ∀ {inst : Ring R} {inst_1 : AddCommGroup V} {inst_2 : TopologicalSpace V} {inst_3 : TopologicalSpace R} {inst_4 : Module R V} [self : SeparatingDual R V] (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 instSeparatingDual {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 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.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 (f.dualMap 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] [Module R V] [SeparatingDual R V] [TopologicalAddGroup 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.

    If a space of linear maps from E to F is complete, and E is nontrivial, then F is complete.

    theorem SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap (𝕜 : Type u_3) (F : Type u_5) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_6} [Finite ι] {M : ιType u_7} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)] [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)] {m : (i : ι) → M i} (hm : ∀ (i : ι), m i 0) :

    If a space of multilinear maps from Π i, E i to F is complete, and each E i has a nonzero element, then F is complete.

    theorem SeparatingDual.completeSpace_continuousMultilinearMap_iff (𝕜 : Type u_3) (F : Type u_5) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_6} [Finite ι] {M : ιType u_7} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)] {m : (i : ι) → M i} (hm : ∀ (i : ι), m i 0) :