Finite-dimensional module topology in coordinates

For a module over a topological semiring with a finite basis, the module topology is the coordinate topology through that basis. This identifies the canonical topology used on quadratic spaces and their endomorphisms with a finite product of copies of the scalars. In particular, over a Hausdorff locally compact division ring equipped with a topological semiring structure, the module topology of a finite-dimensional space is Hausdorff and locally compact, and every subspace of a finite-dimensional space is closed; over σ-compact scalars it is σ-compact. No norm or completeness hypothesis on the scalars is needed.

The basis-dependent API is grouped in TauCeti.ModuleTopology, alongside Mathlib's organizational ModuleTopology namespace.

noncomputable def TauCeti.ModuleTopology.equivFunHomeomorph {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) : V ≃ₜ (ι → K)

Coordinates through a finite basis give a homeomorphism for the module topology.

Equations

• TauCeti.ModuleTopology.equivFunHomeomorph b = { toFun := (↑b.equivFun).toFun, invFun := b.equivFun.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.ModuleTopology.equivFunHomeomorph_apply {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) (v : V) : (equivFunHomeomorph b) v = b.equivFun v

@[simp]

theorem TauCeti.ModuleTopology.equivFunHomeomorph_symm_apply {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) (c : ι → K) : (equivFunHomeomorph b).symm c = b.equivFun.symm c

theorem TauCeti.ModuleTopology.t2Space {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) [T2Space K] : T2Space V

The module topology is Hausdorff when the scalars are Hausdorff and the module has a finite basis.

theorem TauCeti.ModuleTopology.locallyCompactSpace {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) [LocallyCompactSpace K] : LocallyCompactSpace V

The module topology is locally compact when the scalars are locally compact and the module has a finite basis.

theorem TauCeti.ModuleTopology.sigmaCompactSpace {K : Type u_1} {V : Type u_2} {ι : Type u_3} [Semiring K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommMonoid V] [Module K V] [TopologicalSpace V] [IsModuleTopology K V] [Finite ι] (b : Module.Basis ι K V) [SigmaCompactSpace K] : SigmaCompactSpace V

The module topology is σ-compact when the scalars are σ-compact and the module has a finite basis.

theorem TauCeti.t2Space_moduleTopology {K : Type u_1} {V : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [T2Space K] : T2Space V

The module topology of a finite-dimensional space over a Hausdorff division ring equipped with a topological semiring structure is Hausdorff.

theorem TauCeti.locallyCompactSpace_moduleTopology {K : Type u_1} {V : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LocallyCompactSpace K] : LocallyCompactSpace V

The module topology of a finite-dimensional space over a locally compact division ring equipped with a topological semiring structure is locally compact.

theorem TauCeti.sigmaCompactSpace_moduleTopology {K : Type u_1} {V : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [SigmaCompactSpace K] : SigmaCompactSpace V

The module topology of a finite-dimensional space over a σ-compact division ring equipped with a topological semiring structure is σ-compact.

theorem Submodule.isClosed_of_isModuleTopology {K : Type u_1} {V : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalSemiring K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [T2Space K] [TopologicalSpace V] [IsModuleTopology K V] (W : Submodule K V) : IsClosed ↑W

Every subspace of a finite-dimensional space over a Hausdorff division ring equipped with a topological semiring structure is closed for the module topology.