# mathlib3documentation

topology.algebra.module.finite_dimension

# Finite dimensional topological vector spaces over complete fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let π be a complete nontrivially normed field, and E a topological vector space (TVS) over π (i.e we have [add_comm_group E] [module π E] [topological_space E] [topological_add_group E] and [has_continuous_smul π 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 : #

• linear_map.continuous_iff_is_closed_ker : a linear form is continuous if and only if its kernel is closed.
• linear_map.continuous_of_finite_dimensional : a linear map on a finite-dimensional Hausdorff space over a complete field is continuous.

## TODO #

Generalize more of analysis/normed_space/finite_dimension to general TVSs.

## Implementation detail #

The main result from which everything follows is the fact that, if ΞΎ : ΞΉ β E is a finite basis, then ΞΎ.equiv_fun : E ββ (ΞΉ β π) is continuous. However, for technical reasons, it is easier to prove this when ΞΉ and E live ine the same universe. So we start by doing that as a private lemma, then we deduce linear_map.continuous_of_finite_dimensional from it, and then the general result follows as continuous_equiv_fun_basis.

@[protected, instance]
def continuous_linear_map.finite_dimensional {π : Type u_1} {E : Type u_2} {F : Type u_3} [field π] [topological_space π] [module π E] [module π F] [ F] [ E] [ F] :
(E βL[π] F)

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

theorem unique_topology_of_t2 {π : Type u} [hnorm : nontrivially_normed_field π] {t : topological_space π} (hβ : topological_add_group π) (hβ : π) (hβ : t2_space π) :

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 linear_map.continuous_of_is_closed_ker {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] (l : E ββ[π] π) (hl : is_closed ) :

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

theorem linear_map.continuous_iff_is_closed_ker {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] (l : E ββ[π] π) :

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

theorem linear_map.continuous_of_nonzero_on_open {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] (l : E ββ[π] π) (s : set E) (hsβ : is_open s) (hsβ : s.nonempty) (hsβ : β (x : E), x β s β βl x β  0) :

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

theorem linear_map.continuous_of_finite_dimensional {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] (f : E ββ[π] F') :

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

@[protected, instance]
def linear_map.continuous_linear_map_class_of_finite_dimensional {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] :
continuous_linear_map_class (E ββ[π] F') π E F'
Equations
theorem continuous_equiv_fun_basis {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] [t2_space E] {ΞΉ : Type u_1} [fintype ΞΉ] (ΞΎ : basis ΞΉ π E) :

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 wich makes all linear maps from a T2 finite dimensional TVS over such a field continuous (see linear_map.continuous_of_finite_dimensional), which in turn implies that all norms are equivalent in finite dimensions.

def linear_map.to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] :
(E ββ[π] F') ββ[π] E βL[π] F'

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

Equations
@[simp]
theorem linear_map.coe_to_continuous_linear_map' {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] (f : E ββ[π] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] (f : E ββ[π] F') :
@[simp]
theorem linear_map.coe_to_continuous_linear_map_symm {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] :
@[simp]
theorem linear_map.det_to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] [t2_space E] [ E] (f : E ββ[π] E) :
@[simp]
theorem linear_map.ker_to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] (f : E ββ[π] F') :
@[simp]
theorem linear_map.range_to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F' : Type x} [add_comm_group F'] [module π F'] [ F'] [complete_space π] [t2_space E] [ E] (f : E ββ[π] F') :
theorem linear_map.is_open_map_of_finite_dimensional {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [ E] (f : F ββ[π] E) (hf : function.surjective βf) :

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

@[protected, instance]
def linear_map.can_lift_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [ E] :
can_lift (E ββ[π] F) (E βL[π] F) coe (Ξ» (_x : E ββ[π] F), true)
Equations
def linear_equiv.to_continuous_linear_equiv {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
E βL[π] F

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

Equations
@[simp]
theorem linear_equiv.coe_to_continuous_linear_equiv {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[simp]
theorem linear_equiv.coe_to_continuous_linear_equiv' {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[simp]
theorem linear_equiv.coe_to_continuous_linear_equiv_symm {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[simp]
theorem linear_equiv.coe_to_continuous_linear_equiv_symm' {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[simp]
theorem linear_equiv.to_linear_equiv_to_continuous_linear_equiv {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[simp]
theorem linear_equiv.to_linear_equiv_to_continuous_linear_equiv_symm {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] (e : E ββ[π] F) :
@[protected, instance]
def linear_equiv.can_lift_continuous_linear_equiv {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] :
can_lift (E ββ[π] F) (E βL[π] F) continuous_linear_equiv.to_linear_equiv (Ξ» (_x : E ββ[π] F), true)
Equations
theorem finite_dimensional.nonempty_continuous_linear_equiv_of_finrank_eq {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] [ 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 finite_dimensional.nonempty_continuous_linear_equiv_iff_finrank_eq {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] [ 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.

noncomputable def continuous_linear_equiv.of_finrank_eq {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] [t2_space E] [t2_space F] [ E] [ 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
noncomputable def basis.constrL {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] [t2_space E] (v : basis ΞΉ π E) (f : ΞΉ β F) :
E βL[π] F

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

Equations
@[simp, norm_cast]
theorem basis.coe_constrL {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] [t2_space E] (v : basis ΞΉ π E) (f : ΞΉ β F) :
β(v.constrL f) = β(v.constr π) f
noncomputable def basis.equiv_funL {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] [t2_space E] (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
@[simp]
theorem basis.constrL_apply {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] [t2_space E] (v : basis ΞΉ π E) (f : ΞΉ β F) (e : E) :
β(v.constrL f) e = finset.univ.sum (Ξ» (i : ΞΉ), β(v.equiv_fun) e i β’ f i)
@[simp]
theorem basis.constrL_basis {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] {F : Type w} [module π F] [ F] [complete_space π] {ΞΉ : Type u_1} [fintype ΞΉ] [t2_space E] (v : basis ΞΉ π E) (f : ΞΉ β F) (i : ΞΉ) :
β(v.constrL f) (βv i) = f i
noncomputable def continuous_linear_map.to_continuous_linear_equiv_of_det_ne_zero {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] [t2_space E] [ 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
@[simp]
theorem continuous_linear_map.coe_to_continuous_linear_equiv_of_det_ne_zero {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] [t2_space E] [ E] (f : E βL[π] E) (hf : f.det β  0) :
@[simp]
theorem continuous_linear_map.to_continuous_linear_equiv_of_det_ne_zero_apply {π : Type u} [hnorm : nontrivially_normed_field π] {E : Type v} [module π E] [ E] [complete_space π] [t2_space E] [ E] (f : E βL[π] E) (hf : f.det β  0) (x : E) :
= βf x
theorem matrix.to_lin_fin_two_prod_to_continuous_linear_map {π : Type u} [hnorm : nontrivially_normed_field π] [complete_space π] (a b c d : π) :
βlinear_map.to_continuous_linear_map (β(matrix.to_lin (basis.fin_two_prod π) (basis.fin_two_prod π)) (βmatrix.of ![![a, b], ![c, d]])) = (a β’ π π + b β’ π π).prod (c β’ π π + d β’ π π)