The finest locally convex topology $V_{\mathrm{init}}$

Definition

GarrettFA_IsInitTopology

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysistopological-vector-spaces

Let $V$ be a vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ with a topological vector space topology. The topology of $V$ is the topology of $V_{\rm init}$ , the locally convex colimit of the finite-dimensional subspaces of $V$ , if:

$V$ is locally convex, and
every balanced convex set $U\subseteq V$ such that $U\cap W$ is a neighbourhood of $0$ in $W$ for every finite-dimensional subspace $W$ is a neighbourhood of $0$ in $V$ .

In the notes, $V_{\rm init}$ is used to show that weak duals of most spaces are not complete: it carries the finest locally convex topology, and for it every linear functional is continuous.

Formalization Note The predicate describes the given topology of $V$ ; finite-dimensional subspaces carry the subspace topology, which for Hausdorff $V$ is their unique vector space topology. Existence of such a topology on every vector space is a separate theorem item of the mission.

Definition code

import Mathlib

namespace GarrettFA

open Topology

/-- Garrett, *Completeness and quasi-completeness*, §5: the topology of `V` is the topology of
`V_init`, the locally convex colimit of the finite-dimensional subspaces of `V`:
1. `V` is locally convex (real convexity, `V` being a real vector space by restriction of
   scalars);
2. every balanced convex subset `U ⊆ V` whose trace `U ∩ W` is a neighbourhood of `0` in `W`
   for every finite-dimensional subspace `W` is a neighbourhood of `0` in `V`.
Each `W` carries the subspace topology from `V` (for a Hausdorff topological vector space this
is the unique Hausdorff vector space topology on `W`). -/
structure IsInitTopology (𝕜 : Type*) (V : Type*) [RCLike 𝕜] [AddCommGroup V] [Module 𝕜 V]
    [Module ℝ V] [IsScalarTower ℝ 𝕜 V] [TopologicalSpace V] : Prop where
  locallyConvex : LocallyConvexSpace ℝ V
  mem_nhds_of_balanced_convex : ∀ U : Set V, Balanced 𝕜 U → Convex ℝ U →
    (∀ W : Submodule 𝕜 V, FiniteDimensional 𝕜 W → {y : W | (y : V) ∈ U} ∈ 𝓝 (0 : W)) →
    U ∈ 𝓝 (0 : V)

end GarrettFA

Source

Paul Garrett, *Completeness and quasi-completeness* (lecture notes, April 24, 2014), http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf, p. 8, §5 (definition of

V_{\rm init}

as the locally convex colimit of the finite-dimensional subspaces)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Defines a property of a type $V$ given a real-or-complex scalar field $\mathbb K$ (in practice $\mathbb R$ or $\mathbb C$ ), a $\mathbb K$ -vector space structure on $V$ , a compatible real vector space structure, and a topology on $V$ (no continuity assumptions are built in). The topology of $V$ is the initial topology when both of the following hold:

$V$ is locally convex as a real topological vector space;
every set $U\subseteq V$ that is balanced over $\mathbb K$ ( $cU\subseteq U$ for $|c|\le1$ ) and convex (real sense), and such that for every finite-dimensional $\mathbb K$ -subspace $W\subseteq V$ the set $\{y\in W: y\in U\}$ is a neighbourhood of $0$ in $W$ (with the subspace topology from $V$ ), is a neighbourhood of $0$ in $V$ .

The subspaces $W$ range over all finite-dimensional subspaces, including the zero subspace.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The finest locally convex topology VinitV_{\mathrm{init}}Vinit​

The finest locally convex topology $V_{\mathrm{init}}$