# 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

### Weak star topology on duals of topological modules #

@[instance]
def weak_dual.has_coe_to_fun (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] :
has_coe_to_fun E) (λ (_x : E), E → 𝕜)
def weak_dual (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] :
Type (max u_2 u_1)

The weak dual of a topological module E over a topological semiring 𝕜 consists of continuous linear functionals from E to scalars 𝕜. It is a type synonym with the usual dual (when the latter is defined), but will be equipped with a different topology.

Equations
@[instance]
def weak_dual.inhabited (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] :
@[instance]
def weak_dual.add_comm_monoid (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E]  :
Equations
@[instance]
def weak_dual.topological_space (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] :

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

Equations
theorem weak_dual.coe_fn_continuous (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] :
continuous (λ (x' : E) (z : E), x' z)
theorem weak_dual.eval_continuous (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] (z : E) :
continuous (λ (x' : E), x' z)
theorem weak_dual.continuous_of_continuous_eval (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] {α : Type u} {g : α → E} (h : ∀ (z : E), continuous (λ (a : α), (g a) z)) :
theorem weak_dual.tendsto_iff_forall_eval_tendsto (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E] {γ : Type u} {F : filter γ} {ψs : γ → E} {ψ : E} :
F (𝓝 ψ) ∀ (z : E), filter.tendsto (λ (i : γ), (ψs i) z) F (𝓝 (ψ z))
@[instance]
def weak_dual.has_continuous_add (𝕜 : Type u_1) [semiring 𝕜] (E : Type u_2) [ E]  :

Addition in weak_dual 𝕜 E is continuous.

@[instance]
def weak_dual.module (𝕜 : Type u) (E : Type u_1) [ E] :
E)

If the scalars 𝕜 are a commutative semiring, then weak_dual 𝕜 E is a module over 𝕜.

Equations
@[instance]
def weak_dual.has_continuous_smul (𝕜 : Type u) (E : Type u_1) [ E] :
E)

Scalar multiplication in weak_dual 𝕜 E is continuous (when 𝕜 is a commutative semiring).