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 WeakBilin.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [a : AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    Equations
    instance WeakBilin.instModule {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [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_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)
    Equations
    • = s
    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.embedding {𝕜 : 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) :
    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_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.

    Equations
    • =
    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.

    Equations
    • =
    instance WeakBilin.instTopologicalAddGroup {𝕜 : 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 TopologicalAddGroup, meaning that addition and negation are continuous.

    Equations
    • =