Finite dimensional topological vector spaces over complete fields #
𝕜 be a complete nontrivially normed field, and
E a topological vector space (TVS) over
𝕜 (i.e we have
[AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
[ContinuousSMul 𝕜 E]).
E is finite dimensional and Hausdorff, then all linear maps from
E to any other TVS are
E is a normed space, this gets us the equivalence of norms in finite dimension.
Main results : #
LinearMap.continuous_iff_isClosed_ker: a linear form is continuous if and only if its kernel is closed.
LinearMap.continuous_of_finiteDimensional: a linear map on a finite-dimensional Hausdorff space over a complete field is continuous.
Generalize more of
Mathlib.Analysis.NormedSpace.FiniteDimension to general TVSs.
Implementation detail #
The main result from which everything follows is the fact that, if
ξ : ι → E is a finite basis,
ξ.equivFun : E →ₗ (ι → 𝕜) is continuous. However, for technical reasons, it is easier to
prove this when
E live in the same universe. So we start by doing that as a private
lemma, then we deduce
LinearMap.continuous_of_finiteDimensional from it, and then the general
result follows as
The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.
𝕜 is a nontrivially normed field, any T2 topology on
𝕜 which makes it a topological
vector space over itself (with the norm topology) is equal to the norm topology.
Any linear form on a topological vector space over a nontrivially normed field is continuous if its kernel is closed.
Any linear form on a topological vector space over a nontrivially normed field is continuous if and only if its kernel is closed.
Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is automatically continuous.
Any linear map on a finite dimensional space over a complete field is continuous.
In finite dimensions over a non-discrete complete normed field, the canonical identification
(in terms of a basis) with
𝕜^n (endowed with the product topology) is continuous.
This is the key fact which makes all linear maps from a T2 finite dimensional TVS over such a field
LinearMap.continuous_of_finiteDimensional), which in turn implies that all
norms are equivalent in finite dimensions.
The continuous linear map induced by a linear map on a finite dimensional space
A surjective linear map
f with finite dimensional codomain is an open map.
The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.
Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if they have the same (finite) dimension.
Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if and only if they have the same (finite) dimension.
A continuous linear equivalence between two finite-dimensional topological vector spaces over a complete normed field of the same (finite) dimension.
Construct a continuous linear map given the value at a finite basis.
The continuous linear equivalence between a vector space over
𝕜 with a finite basis and
functions from its basis indexing type to
Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional vector space whose determinant is nonzero.
A finite-dimensional subspace is complete.
A finite-dimensional subspace is closed.
An injective linear map with finite-dimensional domain is a closed embedding.