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.

• Given B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, the type WeakBilin B is a type synonym for E.
• The instance WeakBilin.instTopologicalSpace is the weak topology induced by the bilinear form B.

Main results

We establish that WeakBilin B has the following structure:

• WeakBilin.instContinuousAdd: The addition in WeakBilin B is continuous.
• WeakBilin.instContinuousSMul: The scalar multiplication in WeakBilin B is continuous.

We prove the following results characterizing the weak topology:

• eval_continuous: For any y : F, the evaluation mapping fun x => B x y is continuous.
• continuous_of_continuous_eval: For a mapping to WeakBilin B to be continuous, it suffices that its compositions with pairing with B at all points y : F is continuous.
• tendsto_iff_forall_eval_tendsto: Convergence in WeakBilin B can be characterized in terms of convergence of the evaluations at all points y : F.

References

• [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

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

• WeakBilin x✝ = E

@[implicit_reducible]

noncomputable 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 →ₗ[𝕜] 𝕜) : AddCommMonoid (WeakBilin x✝)

Equations

• instAddCommMonoidWeakBilin x✝ = instAddCommMonoidWeakBilin._aux_1 x✝

@[implicit_reducible]

noncomputable 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

• instModuleWeakBilin x✝ = instModuleWeakBilin._aux_1 x✝

@[implicit_reducible]

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 →ₗ[𝕜] 𝕜) : AddCommGroup (WeakBilin B)

Equations

• WeakBilin.instAddCommGroup B = a

@[implicit_reducible, 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

• WeakBilin.instModule' B = m

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)

@[implicit_reducible]

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 →ₗ[𝕜] 𝕜) : TopologicalSpace (WeakBilin B)

Equations

• WeakBilin.instTopologicalSpace B = TopologicalSpace.induced (fun (x : WeakBilin B) (y : F) => (B x) y) Pi.topologicalSpace

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) : Continuous g

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 𝕜] : ContinuousAdd (WeakBilin B)

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 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakBilin B)

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' := ⋯ }

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 𝕜] : IsTopologicalAddGroup (WeakBilin B)

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