mathlib documentation

topology.algebra.module.finite_dimension

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 [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 : #

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.

theorem linear_map.continuous_on_pi {ΞΉ : Type u_1} {π•œ : Type u_2} {F : Type u_3} [finite ΞΉ] [semiring π•œ] [topological_space π•œ] [add_comm_monoid F] [module π•œ F] [topological_space F] [has_continuous_add F] [has_continuous_smul π•œ F] (f : (ΞΉ β†’ π•œ) β†’β‚—[π•œ] F) :

A linear map on ΞΉ β†’ π•œ (where ΞΉ is finite) is continuous

@[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 ↑(l.ker)) :

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_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) :

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] :
(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} [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]
@[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') :
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) :
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} [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]
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) :
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]
@[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) :
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 π•œ π•œ π•œ)