# 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.

• 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.
• WeakDual 𝕜 E is a type synonym for Dual 𝕜 E (when the latter is defined): both are equal to the type E →L[𝕜] 𝕜 of continuous linear maps from a module E over 𝕜 to the ring 𝕜.
• The instance WeakDual.instTopologicalSpace is the weak-* topology on WeakDual 𝕜 E, i.e., the coarsest topology making the evaluation maps at all z : E continuous.
• WeakSpace 𝕜 E is a type synonym for E (when the latter is defined).
• The instance WeakSpace.instTopologicalSpace is the weak topology on E, i.e., the coarsest topology such that all v : dual 𝕜 E remain continuous.

## 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.

## Notations #

No new notation is introduced.

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

## Tags #

weak-star, weak dual, duality