Documentation

Mathlib.Topology.Algebra.Module.WeakBilin

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.

Main definitions #

The main definition is the type WeakBilin B.

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_4} {F : Type u_5} [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] :
(E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) β†’ Type u_4

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

Equations
Instances For
    instance instAddCommMonoidWeakBilin {π•œ : Type u_2} {E : Type u_1} {F : Type u_3} [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (x✝ : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) :
    Equations
    instance instModuleWeakBilin {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (x✝ : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) :
    Module π•œ (WeakBilin x✝)
    Equations
    instance WeakBilin.instAddCommGroup {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [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_4} {F : Type u_5} [CommSemiring π•œ] [CommSemiring 𝕝] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid 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_4} {F : Type u_5} [CommSemiring π•œ] [CommSemiring 𝕝] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] [SMul 𝕝 π•œ] [Module 𝕝 E] [s : IsScalarTower 𝕝 π•œ E] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) :
    IsScalarTower 𝕝 π•œ (WeakBilin B)
    instance WeakBilin.instTopologicalSpace {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace π•œ] [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) :
    Equations
    theorem WeakBilin.coeFn_continuous {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [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_4} {F : Type u_5} [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_4} {F : Type u_5} [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.isEmbedding {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace π•œ] [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] {B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ} (hB : Function.Injective ⇑B) :
    Topology.IsEmbedding 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_4} {F : Type u_5} [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_4} {F : Type u_5} [TopologicalSpace π•œ] [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) [ContinuousAdd π•œ] :

    Addition in WeakBilin B is continuous.

    instance WeakBilin.instContinuousSMul {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace π•œ] [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) [ContinuousSMul π•œ π•œ] :

    Scalar multiplication by π•œ on WeakBilin B is continuous.

    def WeakBilin.eval {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace π•œ] [CommSemiring π•œ] [AddCommMonoid E] [Module π•œ E] [AddCommMonoid F] [Module π•œ F] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) [ContinuousAdd π•œ] [ContinuousConstSMul π•œ π•œ] :
    F β†’β‚—[π•œ] StrongDual π•œ (WeakBilin B)

    Map F into the topological dual of E with the weak topology induced by F

    Equations
    • WeakBilin.eval B = { toFun := fun (f : F) => { toLinearMap := B.flip f, cont := β‹― }, map_add' := β‹―, map_smul' := β‹― }
    Instances For
      instance WeakBilin.instIsTopologicalAddGroup {π•œ : Type u_2} {E : Type u_4} {F : Type u_5} [TopologicalSpace π•œ] [CommRing π•œ] [AddCommGroup E] [Module π•œ E] [AddCommGroup F] [Module π•œ F] (B : E β†’β‚—[π•œ] F β†’β‚—[π•œ] π•œ) [ContinuousAdd π•œ] :

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