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 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup 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 : NontriviallyNormedField 𝕜] {t : TopologicalSpace 𝕜} (h₁ : TopologicalAddGroup 𝕜) (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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜) (hl : IsClosed ↑(LinearMap.ker l)) : 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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜) : Continuous ⇑l ↔ IsClosed ↑(LinearMap.ker l)

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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜) (s : Set E) (hs₁ : IsOpen s) (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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] : ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F'

Equations

• ⋯ = ⋯

theorem continuous_equivFun_basis {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E] {ι : 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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [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.

def Module.End.toContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (E : Type v) [NormedAddCommGroup E] [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.

@[simp]

theorem LinearMap.coe_toContinuousLinearMap' {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F') : ⇑(LinearMap.toContinuousLinearMap f) = ⇑f

@[simp]

theorem LinearMap.coe_toContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F') : ↑(LinearMap.toContinuousLinearMap f) = f

@[simp]

theorem LinearMap.coe_toContinuousLinearMap_symm {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] : ⇑LinearMap.toContinuousLinearMap.symm = ContinuousLinearMap.toLinearMap

@[simp]

theorem LinearMap.det_toContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E) : (LinearMap.toContinuousLinearMap f).det = LinearMap.det f

@[simp]

theorem LinearMap.ker_toContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F') : LinearMap.ker (LinearMap.toContinuousLinearMap f) = LinearMap.ker f

@[simp]

theorem LinearMap.range_toContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type x} [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F') : LinearMap.range (LinearMap.toContinuousLinearMap f) = LinearMap.range f

theorem LinearMap.isOpenMap_of_finiteDimensional {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : F →ₗ[𝕜] E) (hf : Function.Surjective ⇑f) : IsOpenMap ⇑f

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

instance LinearMap.canLiftContinuousLinearMap {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] : CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) ContinuousLinearMap.toLinearMap fun (x : E →ₗ[𝕜] F) => True

Equations

• ⋯ = ⋯

def LinearEquiv.toContinuousLinearEquiv {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [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 := ⋯ }

@[simp]

theorem LinearEquiv.coe_toContinuousLinearEquiv {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : ↑↑e.toContinuousLinearEquiv = ↑e

@[simp]

theorem LinearEquiv.coe_toContinuousLinearEquiv' {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : ⇑e.toContinuousLinearEquiv = ⇑e

@[simp]

theorem LinearEquiv.coe_toContinuousLinearEquiv_symm {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : ↑↑e.toContinuousLinearEquiv.symm = ↑e.symm

@[simp]

theorem LinearEquiv.coe_toContinuousLinearEquiv_symm' {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : ⇑e.toContinuousLinearEquiv.symm = ⇑e.symm

@[simp]

theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : e.toContinuousLinearEquiv.toLinearEquiv = e

theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm

instance LinearEquiv.canLiftContinuousLinearEquiv {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (cond : Module.finrank 𝕜 E = Module.finrank 𝕜 F) : 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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : Nonempty (E ≃L[𝕜] F) ↔ Module.finrank 𝕜 E = Module.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.

def ContinuousLinearEquiv.ofFinrankEq {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (cond : Module.finrank 𝕜 E = Module.finrank 𝕜 F) : 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

• ContinuousLinearEquiv.ofFinrankEq cond = (LinearEquiv.ofFinrankEq E F cond).toContinuousLinearEquiv

def Basis.constrL {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (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)

@[simp]

theorem Basis.coe_constrL {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Basis ι 𝕜 E) (f : ι → F) : ↑(v.constrL f) = (v.constr 𝕜) f

@[simp]

theorem Basis.equivFunL_apply {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Basis ι 𝕜 E) : ∀ (a : E) (a_1 : ι), v.equivFunL a a_1 = (v.repr a) a_1

def Basis.equivFunL {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space 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

• v.equivFunL = { toLinearEquiv := v.equivFun, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Basis.equivFunL_symm_apply_repr {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Basis ι 𝕜 E) (x : E) : v.equivFunL.symm ⇑(v.repr x) = x

@[simp]

theorem Basis.constrL_apply {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] {ι : 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 : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] [T2Space E] (v : Basis ι 𝕜 E) (f : ι → F) (i : ι) : (v.constrL f) (v i) = f i

def ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E] [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

@[simp]

theorem ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (f : E →L[𝕜] E) (hf : f.det ≠ 0) : ↑(f.toContinuousLinearEquivOfDetNeZero hf) = f

@[simp]

theorem ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E] [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 : NontriviallyNormedField 𝕜] [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) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [UniformSpace E] [T2Space E] [UniformAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] : CompleteSpace E

theorem Submodule.complete_of_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [UniformSpace E] [T2Space E] [UniformAddGroup E] [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} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space 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} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [T2Space F] [TopologicalAddGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space E] [FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F} (hf : LinearMap.ker f = ⊥) : ClosedEmbedding ⇑f

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

theorem closedEmbedding_smul_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space E] {c : E} (hc : c ≠ 0) : ClosedEmbedding fun (x : 𝕜) => x • c

theorem isClosedMap_smul_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space 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} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [T2Space F] [TopologicalAddGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F) (hf : LinearMap.range f = ⊤) : ∃ (g : F →L[𝕜] E), f.comp g = ContinuousLinearMap.id 𝕜 F