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 π]
[add_comm_group E]
[module π E]
[topological_space E]
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[finite_dimensional π E]
[finite_dimensional π F] :
finite_dimensional π (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β : has_continuous_smul π π)
(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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
(l : E ββ[π] π)
(hl : is_closed β(linear_map.ker l)) :
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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E] :
continuous_linear_map_class (E ββ[π] F') π E F'
Equations
theorem
continuous_equiv_fun_basis
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
[t2_space E]
{ΞΉ : Type u_1}
[fintype ΞΉ]
(ΞΎ : basis ΞΉ π E) :
continuous β(ΞΎ.equiv_fun)
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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E] :
The continuous linear map induced by a linear map on a finite dimensional space
@[simp]
theorem
linear_map.coe_to_continuous_linear_map'
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E ββ[π] F') :
@[simp]
theorem
linear_map.coe_to_continuous_linear_map
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E ββ[π] F') :
@[simp]
theorem
linear_map.coe_to_continuous_linear_map_symm
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E] :
@[simp]
theorem
linear_map.det_to_continuous_linear_map
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E ββ[π] E) :
@[simp]
theorem
linear_map.ker_to_continuous_linear_map
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E ββ[π] F') :
@[simp]
theorem
linear_map.range_to_continuous_linear_map
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F' : Type x}
[add_comm_group F']
[module π F']
[topological_space F']
[topological_add_group F']
[has_continuous_smul π F']
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E ββ[π] F') :
theorem
linear_map.is_open_map_of_finite_dimensional
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[finite_dimensional π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[finite_dimensional π E] :
Equations
def
linear_equiv.to_continuous_linear_equiv
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.
Equations
- e.to_continuous_linear_equiv = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
linear_equiv.coe_to_continuous_linear_equiv
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
@[simp]
theorem
linear_equiv.coe_to_continuous_linear_equiv'
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
@[simp]
theorem
linear_equiv.coe_to_continuous_linear_equiv_symm
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
@[simp]
theorem
linear_equiv.coe_to_continuous_linear_equiv_symm'
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
@[simp]
theorem
linear_equiv.to_linear_equiv_to_continuous_linear_equiv
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
(e : E ββ[π] F) :
@[protected, instance]
def
linear_equiv.can_lift_continuous_linear_equiv
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E] :
Equations
theorem
finite_dimensional.nonempty_continuous_linear_equiv_of_finrank_eq
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
[finite_dimensional π F]
(cond : finite_dimensional.finrank π E = finite_dimensional.finrank π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
[finite_dimensional π F] :
nonempty (E βL[π] F) β finite_dimensional.finrank π E = finite_dimensional.finrank π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
[t2_space E]
[t2_space F]
[finite_dimensional π E]
[finite_dimensional π F]
(cond : finite_dimensional.finrank π E = finite_dimensional.finrank π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
{ΞΉ : Type u_1}
[fintype ΞΉ]
[t2_space E]
(v : basis ΞΉ π E)
(f : ΞΉ β F) :
Construct a continuous linear map given the value at a finite basis.
@[simp, norm_cast]
theorem
basis.coe_constrL
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
{ΞΉ : Type u_1}
[fintype ΞΉ]
[t2_space E]
(v : basis ΞΉ π E)
(f : ΞΉ β F) :
noncomputable
def
basis.equiv_funL
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
{ΞΉ : Type u_1}
[fintype ΞΉ]
[t2_space E]
(v : basis ΞΉ π E) :
The continuous linear equivalence between a vector space over π with a finite basis and
functions from its basis indexing type to π.
Equations
- v.equiv_funL = {to_linear_equiv := {to_fun := v.equiv_fun.to_fun, map_add' := _, map_smul' := _, inv_fun := v.equiv_fun.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
basis.constrL_apply
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
{ΞΉ : Type u_1}
[fintype ΞΉ]
[t2_space E]
(v : basis ΞΉ π E)
(f : ΞΉ β F)
(e : E) :
@[simp]
theorem
basis.constrL_basis
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
{F : Type w}
[add_comm_group F]
[module π F]
[topological_space F]
[topological_add_group F]
[has_continuous_smul π F]
[complete_space π]
{ΞΉ : Type u_1}
[fintype ΞΉ]
[t2_space E]
(v : basis ΞΉ π E)
(f : ΞΉ β F)
(i : ΞΉ) :
noncomputable
def
continuous_linear_map.to_continuous_linear_equiv_of_det_ne_zero
{π : Type u}
[hnorm : nontrivially_normed_field π]
{E : Type v}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E βL[π] E)
(hf : f.det β 0) :
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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
[t2_space E]
[finite_dimensional π 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}
[add_comm_group E]
[module π E]
[topological_space E]
[topological_add_group E]
[has_continuous_smul π E]
[complete_space π]
[t2_space E]
[finite_dimensional π E]
(f : E βL[π] E)
(hf : f.det β 0)
(x : E) :
β(f.to_continuous_linear_equiv_of_det_ne_zero hf) x = β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 β’ continuous_linear_map.fst π π π + b β’ continuous_linear_map.snd π π π).prod (c β’ continuous_linear_map.fst π π π + d β’ continuous_linear_map.snd π π π)