Documentation

Mathlib.Topology.Algebra.Module.WeakDual

Weak dual topology #

We continue in the setting of Mathlib/Topology/Algebra/Module/WeakBilin.lean, which defines the weak topology given two vector spaces E and F over a commutative semiring 𝕜 and a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜. The weak topology on E is the coarsest topology such that for all y : F every map fun x => B x y is continuous.

In this file, we consider two special cases. In the case that F = E →L[𝕜] 𝕜 and B being the canonical pairing, we obtain the weak-* topology, WeakDual 𝕜 E := (E →L[𝕜] 𝕜). Interchanging the arguments in the bilinear form yields the weak topology WeakSpace 𝕜 E := E.

Main definitions #

The main definitions are the types WeakDual 𝕜 E and WeakSpace 𝕜 E, with the respective topology instances on it.

References #

Tags #

weak-star, weak dual, duality

def WeakDual (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
Type (max u_6 u_7)

The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all functionals fun v => v x are continuous.

Equations
Instances For
    instance instModuleWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    Module 𝕜 (WeakDual 𝕜 E)
    Equations
    instance instContinuousAddWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    Equations
    • =
    instance instFunLikeWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    FunLike (WeakDual 𝕜 E) E 𝕜
    Equations
    instance instContinuousLinearMapClassWeakDual (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜
    Equations
    • =
    instance WeakDual.instMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
    MulAction M (WeakDual 𝕜 E)

    If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts on WeakDual 𝕜 E.

    Equations
    instance WeakDual.instDistribMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :

    If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts distributively on WeakDual 𝕜 E.

    Equations
    instance WeakDual.instModule' {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (R : Type u_6) [Semiring R] [Module R 𝕜] [SMulCommClass 𝕜 R 𝕜] [ContinuousConstSMul R 𝕜] :
    Module R (WeakDual 𝕜 E)

    If 𝕜 is a topological module over a semiring R and scalar multiplication commutes with the multiplication on 𝕜, then WeakDual 𝕜 E is a module over R.

    Equations
    instance WeakDual.instContinuousConstSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
    instance WeakDual.instContinuousSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [TopologicalSpace M] [ContinuousSMul M 𝕜] :

    If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it continuously acts on WeakDual 𝕜 E.

    theorem WeakDual.coeFn_continuous {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    Continuous fun (x : WeakDual 𝕜 E) (y : E) => x y
    theorem WeakDual.eval_continuous {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (y : E) :
    Continuous fun (x : WeakDual 𝕜 E) => x y
    theorem WeakDual.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace α] {g : αWeakDual 𝕜 E} (h : ∀ (y : E), Continuous fun (a : α) => (g a) y) :
    instance WeakDual.instT2Space {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space 𝕜] :
    T2Space (WeakDual 𝕜 E)
    def WeakSpace (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    Type u_7

    The weak topology is the topology coarsest topology on E such that all functionals fun x => v x are continuous.

    Equations
    Instances For
      instance instModuleWeakSpace (𝕜 : Type u_1) (E : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Module 𝕜 (WeakSpace 𝕜 E)
      Equations
      instance instContinuousAddWeakSpace (𝕜 : Type u_2) (E : Type u_1) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Equations
      • =
      instance WeakSpace.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 E] :
      Module 𝕝 (WeakSpace 𝕜 E)
      Equations
      instance WeakSpace.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
      IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E)
      def WeakSpace.map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :
      WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F

      A continuous linear map from E to F is still continuous when E and F are equipped with their weak topologies.

      Equations
      Instances For
        theorem WeakSpace.map_apply {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) (x : E) :
        (map f) x = f x
        @[simp]
        theorem WeakSpace.coe_map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :
        (map f) = f
        def toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        E ≃ₗ[𝕜] WeakSpace 𝕜 E

        There is a canonical map E → WeakSpace 𝕜 E (the "identity" mapping). It is a linear equivalence.

        Equations
        Instances For
          def toWeakSpaceCLM (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
          E →L[𝕜] WeakSpace 𝕜 E

          For a topological vector space E, "identity mapping" E → WeakSpace 𝕜 E is continuous. This definition implements it as a continuous linear map.

          Equations
          Instances For
            @[simp]
            theorem toWeakSpaceCLM_eq_toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x : E) :
            (toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x
            theorem isOpenMap_toWeakSpace_symm {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :

            The canonical map from WeakSpace 𝕜 E to E is an open map.

            theorem WeakSpace.isOpen_of_isOpen {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V)) :

            A set in E which is open in the weak topology is open.

            theorem tendsto_iff_forall_eval_tendsto_topDualPairing {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {l : Filter α} {f : αWeakDual 𝕜 E} {x : WeakDual 𝕜 E} :
            Filter.Tendsto f l (nhds x) ∀ (y : E), Filter.Tendsto (fun (i : α) => ((topDualPairing 𝕜 E) (f i)) y) l (nhds (((topDualPairing 𝕜 E) x) y))