Algebraic facts about the topology of uniform convergence

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

Main statements

• UniformOnFun.continuousSMul_induced_of_image_bounded : let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

Implementation notes

Like in Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean, we use the type aliases UniformFun (denoted α →ᵤ β) and UniformOnFun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

References

• [N. Bourbaki, General Topology, Chapter X][bourbaki1966]
• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

Tags

uniform convergence, strong dual

theorem UniformFun.continuousSMul_induced_of_range_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] [FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom) (hφ : Topology.IsInducing (⇑ofFun ∘ ⇑φ)) (h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) : ContinuousSMul 𝕜 H

Let E be a topological vector space over a normed field 𝕜, let α be any type. Let H be a submodule of α →ᵤ E such that the range of each f ∈ H is von Neumann bounded. Then H is a topological vector space over 𝕜, i.e., the pointwise scalar multiplication is continuous in both variables.

For convenience we require that H is a vector space over 𝕜 with a topology induced by UniformFun.ofFun ∘ φ, where φ : H →ₗ[𝕜] (α → E).

theorem UniformOnFun.continuousSMul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} [FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom) (hφ : Topology.IsInducing (⇑(ofFun 𝔖) ∘ ⇑φ)) (h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) : ContinuousSMul 𝕜 H

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : Submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the Submodule version as UniformOnFun.continuousSMul_submodule_of_image_bounded.

theorem UniformOnFun.continuousSMul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} (H : Submodule 𝕜 (UniformOnFun α E 𝔖)) (h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) : ContinuousSMul 𝕜 ↥H

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.