# mathlibdocumentation

topology.algebra.weak_dual_topology

# Weak dual topology #

This file defines the weak-* topology on duals of suitable topological modules E over suitable topological semirings 𝕜. The (weak) dual consists of continuous linear functionals E →L[𝕜] 𝕜 from E to scalars 𝕜. The weak-* topology is the coarsest topology on this dual weak_dual 𝕜 E := (E →L[𝕜] 𝕜) w.r.t. which the evaluation maps at all z : E are continuous.

The weak dual is a module over 𝕜 if the semiring 𝕜 is commutative.

## Main definitions #

The main definitions are the type weak_dual 𝕜 E and a topology instance on it.

• weak_dual 𝕜 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 weak_dual.topological_space is the weak-* topology on weak_dual 𝕜 E, i.e., the coarsest topology making the evaluation maps at all z : E continuous.

## Main results #

We establish that weak_dual 𝕜 E has the following structure:

• weak_dual.has_continuous_add: The addition in weak_dual 𝕜 E is continuous.
• weak_dual.module: If the scalars 𝕜 are a commutative semiring, then weak_dual 𝕜 E is a module over 𝕜.
• weak_dual.has_continuous_smul: If the scalars 𝕜 are a commutative semiring, then the scalar multiplication by 𝕜 in weak_dual 𝕜 E is continuous.

We prove the following results characterizing the weak-* topology:

• weak_dual.eval_continuous: For any z : E, the evaluation mapping weak_dual 𝕜 E → 𝕜 taking x'to x' z is continuous.
• weak_dual.continuous_of_continuous_eval: For a mapping to weak_dual 𝕜 E to be continuous, it suffices that its compositions with evaluations at all points z : E are continuous.
• weak_dual.tendsto_iff_forall_eval_tendsto: Convergence in weak_dual 𝕜 E can be characterized in terms of convergence of the evaluations at all points z : E.

## Notations #

No new notation is introduced.

## Implementation notes #

The weak-* topology is defined as the induced topology under the mapping that associates to a dual element x' the functional E → 𝕜, when the space E → 𝕜 of functionals is equipped with the topology of pointwise convergence (product topology).

Typically one might assume that 𝕜 is a topological semiring in the sense of the typeclasses topological_space 𝕜, semiring 𝕜, has_continuous_add 𝕜, has_continuous_mul 𝕜, and that the space E is a topological module over 𝕜 in the sense of the typeclasses topological_space E, add_comm_monoid E, has_continuous_add E, module 𝕜 E, has_continuous_smul 𝕜 E. The definitions and results are, however, given with weaker assumptions when possible.

## Tags #

weak-star, weak dual