English
Let 𝕜 be a complete normed field and E a finite-dimensional 𝕜-vector space endowed with a Hausdorff topological vector space structure. Then E carries the module topology, i.e., its topology is the canonical topology making 𝕜-scalar multiplication continuous.
Русский
Пусть 𝕜 — поле с полной нормой, E — конечномерное векторное пространство над 𝕜, на котором задано Гауссово топологическое пространство. Тогда на E существует модульная топология, совместимая с операцией умножения на скаляры из 𝕜.
LaTeX
$$$\\operatorname{IsModuleTopology} \\, 𝕜 \\, E$$$
Lean4
/-- A finite-dimensional t2 vector space over a complete field must carry the module topology.
Not declared as a global instance only for performance reasons. -/
@[local instance]
theorem isModuleTopologyOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] : IsModuleTopology 𝕜 E :=
-- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equivFun_basis`, and
-- use that it has the module topology
let b := Basis.ofVectorSpace 𝕜 E
have continuousEquiv : E ≃L[𝕜] (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜 :=
{ __ := b.equivFun
continuous_toFun := continuous_equivFun_basis_aux b
continuous_invFun :=
IsModuleTopology.continuous_of_linearMap (R := 𝕜) (A := (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜) (B := E)
b.equivFun.symm }
IsModuleTopology.iso continuousEquiv.symm
