# Finite dimensional topological vector spaces over complete fields #

Let π 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] and [ContinuousSMul π E]).

If E is finite dimensional and Hausdorff, then all linear maps from E to any other TVS are continuous.

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

## TODO #

Generalize more of Mathlib.Analysis.Normed.Module.FiniteDimension to general TVSs.

## Implementation detail #

The main result from which everything follows is the fact that, if ΞΎ : ΞΉ β E is a finite basis, then ΞΎ.equivFun : E ββ (ΞΉ β π) is continuous. However, for technical reasons, it is easier to prove this when ΞΉ and 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 continuous_equivFun_basis.

instance instFiniteDimensionalContinuousLinearMapId {π : Type u_1} {E : Type u_2} {F : Type u_3} [Field π] [TopologicalSpace π] [] [Module π E] [] [] [Module π F] [] [ContinuousSMul π F] [FiniteDimensional π E] [FiniteDimensional π F] :
FiniteDimensional π (E βL[π] F)

The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.

Equations
• β― = β―
theorem unique_topology_of_t2 {π : Type u} [hnorm : ] {t : TopologicalSpace π} (hβ : ) (hβ : ContinuousSMul π π) (hβ : T2Space π) :
t = UniformSpace.toTopologicalSpace

If π 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.

theorem LinearMap.continuous_of_isClosed_ker {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] (l : E ββ[π] π) (hl : IsClosed β) :
Continuous βl

Any linear form on a topological vector space over a nontrivially normed field is continuous if its kernel is closed.

theorem LinearMap.continuous_iff_isClosed_ker {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] (l : E ββ[π] π) :
Continuous βl β IsClosed β

Any linear form on a topological vector space over a nontrivially normed field is continuous if and only if its kernel is closed.

theorem LinearMap.continuous_of_nonzero_on_open {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] (l : E ββ[π] π) (s : Set E) (hsβ : ) (hsβ : s.Nonempty) (hsβ : β x β s, l x β  0) :
Continuous βl

Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is automatically continuous.

theorem LinearMap.continuous_of_finiteDimensional {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] F') :
Continuous βf

Any linear map on a finite dimensional space over a complete field is continuous.

instance LinearMap.continuousLinearMapClassOfFiniteDimensional {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] :
ContinuousLinearMapClass (E ββ[π] F') π E F'
Equations
• β― = β―
theorem continuous_equivFun_basis {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] [] {ΞΉ : Type u_1} [Finite ΞΉ] (ΞΎ : Basis ΞΉ π E) :
Continuous βΞΎ.equivFun

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 continuous (see LinearMap.continuous_of_finiteDimensional), which in turn implies that all norms are equivalent in finite dimensions.

def LinearMap.toContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] :
(E ββ[π] F') ββ[π] E βL[π] F'

The continuous linear map induced by a linear map on a finite dimensional space

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Module.End.toContinuousLinearMap {π : Type u} [hnorm : ] [CompleteSpace π] (E : Type v) [NormedSpace π E] [FiniteDimensional π E] :
(E ββ[π] E) ββ[π] E βL[π] E

Algebra equivalence between the linear maps and continuous linear maps on a finite dimensional space.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.coe_toContinuousLinearMap' {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] F') :
β(LinearMap.toContinuousLinearMap f) = βf
@[simp]
theorem LinearMap.coe_toContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] F') :
β(LinearMap.toContinuousLinearMap f) = f
@[simp]
theorem LinearMap.coe_toContinuousLinearMap_symm {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] :
βLinearMap.toContinuousLinearMap.symm = ContinuousLinearMap.toLinearMap
@[simp]
theorem LinearMap.det_toContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] E) :
(LinearMap.toContinuousLinearMap f).det = LinearMap.det f
@[simp]
theorem LinearMap.ker_toContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] F') :
LinearMap.ker (LinearMap.toContinuousLinearMap f) =
@[simp]
theorem LinearMap.range_toContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F' : Type x} [] [Module π F'] [] [] [ContinuousSMul π F'] [CompleteSpace π] [] [FiniteDimensional π E] (f : E ββ[π] F') :
LinearMap.range (LinearMap.toContinuousLinearMap f) =
theorem LinearMap.isOpenMap_of_finiteDimensional {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [FiniteDimensional π E] (f : F ββ[π] E) (hf : ) :
IsOpenMap βf

A surjective linear map f with finite dimensional codomain is an open map.

instance LinearMap.canLiftContinuousLinearMap {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [FiniteDimensional π E] :
CanLift (E ββ[π] F) (E βL[π] F) ContinuousLinearMap.toLinearMap fun (x : E ββ[π] F) => True
Equations
• β― = β―
def LinearEquiv.toContinuousLinearEquiv {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
E βL[π] F

The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.

Equations
• e.toContinuousLinearEquiv = { toLinearEquiv := e, continuous_toFun := β―, continuous_invFun := β― }
Instances For
@[simp]
theorem LinearEquiv.coe_toContinuousLinearEquiv {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
ββe.toContinuousLinearEquiv = βe
@[simp]
theorem LinearEquiv.coe_toContinuousLinearEquiv' {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
βe.toContinuousLinearEquiv = βe
@[simp]
theorem LinearEquiv.coe_toContinuousLinearEquiv_symm {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
ββe.toContinuousLinearEquiv.symm = βe.symm
@[simp]
theorem LinearEquiv.coe_toContinuousLinearEquiv_symm' {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
βe.toContinuousLinearEquiv.symm = βe.symm
@[simp]
theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
e.toContinuousLinearEquiv.toLinearEquiv = e
theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] (e : E ββ[π] F) :
e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm
instance LinearEquiv.canLiftContinuousLinearEquiv {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] :
CanLift (E ββ[π] F) (E βL[π] F) ContinuousLinearEquiv.toLinearEquiv fun (x : E ββ[π] F) => True
Equations
• β― = β―
theorem FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] [FiniteDimensional π F] (cond : = ) :
Nonempty (E βL[π] F)

Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if they have the same (finite) dimension.

theorem FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] [FiniteDimensional π F] :
Nonempty (E βL[π] F) β =

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.

def ContinuousLinearEquiv.ofFinrankEq {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] [] [FiniteDimensional π E] [FiniteDimensional π F] (cond : = ) :
E βL[π] F

A continuous linear equivalence between two finite-dimensional topological vector spaces over a complete normed field of the same (finite) dimension.

Equations
Instances For
def Basis.constrL {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) (f : ΞΉ β F) :
E βL[π] F

Construct a continuous linear map given the value at a finite basis.

Equations
• v.constrL f = LinearMap.toContinuousLinearMap ((v.constr π) f)
Instances For
@[simp]
theorem Basis.coe_constrL {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) (f : ΞΉ β F) :
β(v.constrL f) = (v.constr π) f
@[simp]
theorem Basis.equivFunL_apply {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) :
β (a : E) (a_1 : ΞΉ), v.equivFunL a a_1 = (v.repr a) a_1
def Basis.equivFunL {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) :
E βL[π] ΞΉ β π

The continuous linear equivalence between a vector space over π with a finite basis and functions from its basis indexing type to π.

Equations
• v.equivFunL = let __src := v.equivFun; { toLinearEquiv := __src, continuous_toFun := β―, continuous_invFun := β― }
Instances For
@[simp]
theorem Basis.equivFunL_symm_apply_repr {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) (x : E) :
v.equivFunL.symm β(v.repr x) = x
@[simp]
theorem Basis.constrL_apply {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] [] {ΞΉ : Type u_2} [Fintype ΞΉ] (v : Basis ΞΉ π E) (f : ΞΉ β F) (e : E) :
(v.constrL f) e = β i : ΞΉ, v.equivFun e i β’ f i
@[simp]
theorem Basis.constrL_basis {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] {F : Type w} [] [Module π F] [] [ContinuousSMul π F] [CompleteSpace π] {ΞΉ : Type u_1} [Finite ΞΉ] [] (v : Basis ΞΉ π E) (f : ΞΉ β F) (i : ΞΉ) :
(v.constrL f) (v i) = f i
def ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] [] [FiniteDimensional π E] (f : E βL[π] E) (hf : f.det β  0) :
E βL[π] E

Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional vector space whose determinant is nonzero.

Equations
• f.toContinuousLinearEquivOfDetNeZero hf = ((βf).equivOfDetNeZero hf).toContinuousLinearEquiv
Instances For
@[simp]
theorem ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] [] [FiniteDimensional π E] (f : E βL[π] E) (hf : f.det β  0) :
β(f.toContinuousLinearEquivOfDetNeZero hf) = f
@[simp]
theorem ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply {π : Type u} [hnorm : ] {E : Type v} [] [Module π E] [] [ContinuousSMul π E] [CompleteSpace π] [] [FiniteDimensional π E] (f : E βL[π] E) (hf : f.det β  0) (x : E) :
(f.toContinuousLinearEquivOfDetNeZero hf) x = f x
theorem Matrix.toLin_finTwoProd_toContinuousLinearMap {π : Type u} [hnorm : ] [CompleteSpace π] (a : π) (b : π) (c : π) (d : π) :
LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd π) (Basis.finTwoProd π)) !![a, b; c, d]) = (a β’ ContinuousLinearMap.fst π π π + b β’ ContinuousLinearMap.snd π π π).prod (c β’ ContinuousLinearMap.fst π π π + d β’ ContinuousLinearMap.snd π π π)
theorem FiniteDimensional.complete (π : Type u_1) (E : Type u_2) [] [CompleteSpace π] [] [] [] [] [Module π E] [ContinuousSMul π E] [FiniteDimensional π E] :
theorem Submodule.complete_of_finiteDimensional {π : Type u_1} {E : Type u_2} [] [CompleteSpace π] [] [] [] [] [Module π E] [ContinuousSMul π E] (s : Submodule π E) [FiniteDimensional π β₯s] :
IsComplete βs

A finite-dimensional subspace is complete.

theorem Submodule.closed_of_finiteDimensional {π : Type u_1} {E : Type u_2} [] [CompleteSpace π] [] [] [Module π E] [ContinuousSMul π E] [] (s : Submodule π E) [FiniteDimensional π β₯s] :
IsClosed βs

A finite-dimensional subspace is closed.

theorem LinearMap.closedEmbedding_of_injective {π : Type u_1} {E : Type u_2} {F : Type u_3} [] [CompleteSpace π] [] [] [Module π E] [ContinuousSMul π E] [] [] [] [Module π F] [ContinuousSMul π F] [] [FiniteDimensional π E] {f : E ββ[π] F} (hf : ) :

An injective linear map with finite-dimensional domain is a closed embedding.

theorem closedEmbedding_smul_left {π : Type u_1} {E : Type u_2} [] [CompleteSpace π] [] [] [Module π E] [ContinuousSMul π E] [] {c : E} (hc : c β  0) :
ClosedEmbedding fun (x : π) => x β’ c
theorem isClosedMap_smul_left {π : Type u_1} {E : Type u_2} [] [CompleteSpace π] [] [] [Module π E] [ContinuousSMul π E] [] (c : E) :
IsClosedMap fun (x : π) => x β’ c
theorem ContinuousLinearMap.exists_right_inverse_of_surjective {π : Type u_1} {E : Type u_2} {F : Type u_3} [] [CompleteSpace π] [] [] [Module π E] [ContinuousSMul π E] [] [] [] [Module π F] [ContinuousSMul π F] [FiniteDimensional π F] (f : E βL[π] F) (hf : ) :
β (g : F βL[π] E), f.comp g =