Documentation

Mathlib.Topology.Algebra.Module.WeakDual

Weak dual topology #

This file 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 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 WeakBilin B for the general case and the two special cases WeakDual 𝕜 E and WeakSpace 𝕜 E with the respective topology instances on it.

Main results #

We establish that WeakBilin B has the following structure:

We prove the following results characterizing the weak topology:

Notations #

No new notation is introduced.

References #

Tags #

weak-star, weak dual, duality

def WeakBilin {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] :
(E →ₗ[𝕜] F →ₗ[𝕜] 𝕜)Type u_5

The space E equipped with the weak topology induced by the bilinear form B.

Equations
Instances For
    instance WeakBilin.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [a : AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Equations
    instance WeakBilin.instModule {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [AddCommMonoid E] [m : Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Module 𝕜 (WeakBilin B)
    Equations
    instance WeakBilin.instAddCommGroup {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [a : AddCommGroup E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Equations
    @[instance 100]
    instance WeakBilin.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [m : Module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Module 𝕝 (WeakBilin B)
    Equations
    instance WeakBilin.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [SMul 𝕝 𝕜] [Module 𝕝 E] [s : IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    IsScalarTower 𝕝 𝕜 (WeakBilin B)
    Equations
    • = s
    instance WeakBilin.instTopologicalSpace {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Equations
    theorem WeakBilin.coeFn_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Continuous fun (x : WeakBilin B) (y : F) => (B x) y

    The coercion (fun x y => B x y) : E → (F → 𝕜) is continuous.

    theorem WeakBilin.eval_continuous {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (y : F) :
    Continuous fun (x : WeakBilin B) => (B x) y
    theorem WeakBilin.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [TopologicalSpace α] {g : αWeakBilin B} (h : ∀ (y : F), Continuous fun (a : α) => (B (g a)) y) :
    theorem WeakBilin.embedding {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective B) :
    Embedding fun (x : WeakBilin B) (y : F) => (B x) y

    The coercion (fun x y => B x y) : E → (F → 𝕜) is an embedding.

    theorem WeakBilin.tendsto_iff_forall_eval_tendsto {α : Type u_1} {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) {l : Filter α} {f : αWeakBilin B} {x : WeakBilin B} (hB : Function.Injective B) :
    Filter.Tendsto f l (nhds x) ∀ (y : F), Filter.Tendsto (fun (i : α) => (B (f i)) y) l (nhds ((B x) y))
    instance WeakBilin.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] :

    Addition in WeakBilin B is continuous.

    Equations
    • =
    instance WeakBilin.instContinuousSMul {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousSMul 𝕜 𝕜] :

    Scalar multiplication by 𝕜 on WeakBilin B is continuous.

    Equations
    • =
    instance WeakBilin.instTopologicalAddGroup {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [TopologicalSpace 𝕜] [CommRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousAdd 𝕜] :

    WeakBilin B is a TopologicalAddGroup, meaning that addition and negation are continuous.

    Equations
    • =
    def topDualPairing (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 𝕜] :
    (E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜

    The canonical pairing of a vector space and its topological dual.

    Equations
    Instances For
      theorem topDualPairing_apply {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (v : E →L[𝕜] 𝕜) (x : E) :
      ((topDualPairing 𝕜 E) v) x = v x
      def WeakDual (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Type (max u_8 u_9)

      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 WeakDual.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Equations
        instance WeakDual.instModule {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Module 𝕜 (WeakDual 𝕜 E)
        Equations
        Equations
        instance WeakDual.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Equations
        • =
        instance WeakDual.instInhabited {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Equations
        • WeakDual.instInhabited = ContinuousLinearMap.inhabited
        instance WeakDual.instFunLike {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        FunLike (WeakDual 𝕜 E) E 𝕜
        Equations
        • WeakDual.instFunLike = ContinuousLinearMap.funLike
        instance WeakDual.instContinuousLinearMapClass {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜
        Equations
        • =
        instance WeakDual.instCoeFunForall {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        CoeFun (WeakDual 𝕜 E) fun (x : WeakDual 𝕜 E) => E𝕜

        Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

        Equations
        • WeakDual.instCoeFunForall = DFunLike.hasCoeToFun
        instance WeakDual.instMulAction {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [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_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [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_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (R : Type u_8) [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_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
        Equations
        • =
        instance WeakDual.instContinuousSMul {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_8) [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.

        Equations
        • =
        theorem WeakDual.coeFn_continuous {𝕜 : Type u_2} {E : Type u_5} [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_5} [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_5} [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_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space 𝕜] :
        T2Space (WeakDual 𝕜 E)
        Equations
        • =
        def WeakSpace (𝕜 : Type u_8) (E : Type u_9) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Type u_9

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

        Equations
        Instances For
          instance WeakSpace.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
          Equations
          instance WeakSpace.instModule {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
          Module 𝕜 (WeakSpace 𝕜 E)
          Equations
          Equations
          instance WeakSpace.instContinuousAdd {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
          Equations
          • =
          def WeakSpace.map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [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_5} {F : Type u_6} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) (x : E) :
            (WeakSpace.map f) x = f x
            @[simp]
            theorem WeakSpace.coe_map {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :
            (WeakSpace.map f) = f
            def toWeakSpace (𝕜 : Type u_2) (E : Type u_5) [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 continuousLinearMapToWeakSpace (𝕜 : Type u_2) (E : Type u_5) [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 isOpenMap_toWeakSpace_symm {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
                IsOpenMap (toWeakSpace 𝕜 E).symm

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

                theorem WeakSpace.isOpen_of_isOpen {𝕜 : Type u_2} {E : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen ((continuousLinearMapToWeakSpace 𝕜 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_5} [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))