# mathlib3documentation

topology.algebra.module.strong_topology

# Strong topologies on the space of continuous linear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define the strong topologies on E →L[𝕜] F associated with a family 𝔖 : set (set E) to be the topology of uniform convergence on the elements of 𝔖 (also called the topology of 𝔖-convergence).

The lemma uniform_on_fun.has_continuous_smul_of_image_bounded tells us that this is a vector space topology if the continuous linear image of any element of 𝔖 is bounded (in the sense of bornology.is_vonN_bounded).

We then declare an instance for the case where 𝔖 is exactly the set of all bounded subsets of E, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of bounded convergence"), which coincides with the operator norm topology in the case of normed_spaces.

Other useful examples include the weak-* topology (when 𝔖 is the set of finite sets or the set of singletons) and the topology of compact convergence (when 𝔖 is the set of relatively compact sets).

## Main definitions #

• continuous_linear_map.strong_topology is the topology mentioned above for an arbitrary 𝔖.
• continuous_linear_map.topological_space is the topology of bounded convergence. This is declared as an instance.

## Main statements #

• continuous_linear_map.strong_topology.topological_add_group and continuous_linear_map.strong_topology.has_continuous_smul show that the strong topology makes E →L[𝕜] F a topological vector space, with the assumptions on 𝔖 mentioned above.
• continuous_linear_map.topological_add_group and continuous_linear_map.has_continuous_smul register these facts as instances for the special case of bounded convergence.

## TODO #

• add a type alias for continuous linear maps with the topology of 𝔖-convergence?

## Tags #

uniform convergence, bounded convergence

def continuous_linear_map.strong_topology {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :

Given E and F two topological vector spaces and 𝔖 : set (set E), then strong_topology σ F 𝔖 is the "topology of uniform convergence on the elements of 𝔖" on E →L[𝕜] F.

If the continuous linear image of any element of 𝔖 is bounded, this makes E →L[𝕜] F a topological vector space.

Equations
def continuous_linear_map.strong_uniformity {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :

The uniform structure associated with continuous_linear_map.strong_topology. We make sure that this has nice definitional properties.

Equations
@[simp]
theorem continuous_linear_map.strong_uniformity_topology_eq {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_uniformity.uniform_embedding_coe_fn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.embedding_coe_fn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_uniformity.uniform_add_group {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.topological_add_group {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.t2_space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] [t2_space F] (𝔖 : set (set E)) (h𝔖 : ⋃₀ 𝔖 = set.univ) :
theorem continuous_linear_map.strong_topology.has_continuous_smul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] [ F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) (h𝔖₃ : (S : set E), S 𝔖 ) :
(E →SL[σ] F)
theorem continuous_linear_map.strong_topology.has_basis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] {ι : Type u_4} (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) {p : ι Prop} {b : ι set F} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (λ (Si : set E × ι), Si.fst 𝔖 p Si.snd) (λ (Si : set E × ι), {f : E →SL[σ] F | (x : E), x Si.fst f x b Si.snd})
theorem continuous_linear_map.strong_topology.has_basis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3} (F : Type u_5) [module 𝕜₁ E] [module 𝕜₂ F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : 𝔖) :
(nhds 0).has_basis (λ (SV : set E × set F), SV.fst 𝔖 SV.snd nhds 0) (λ (SV : set E × set F), {f : E →SL[σ] F | (x : E), x SV.fst f x SV.snd})
@[protected, instance]
def continuous_linear_map.topological_space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F]  :

The topology of bounded convergence on E →L[𝕜] F. This coincides with the topology induced by the operator norm when E and F are normed spaces.

Equations
@[protected, instance]
def continuous_linear_map.topological_add_group {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F]  :
@[protected, instance]
def continuous_linear_map.has_continuous_smul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F] [ F] :
(E →SL[σ] F)
@[protected, instance]
def continuous_linear_map.uniform_space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F]  :
Equations
@[protected, instance]
def continuous_linear_map.uniform_add_group {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F]  :
@[protected, instance]
def continuous_linear_map.t2_space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F] [ E] [t2_space F] :
@[protected]
theorem continuous_linear_map.has_basis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F] {ι : Type u_3} {p : ι Prop} {b : ι set F} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (λ (Si : set E × ι), p Si.snd) (λ (Si : set E × ι), {f : E →SL[σ] F | (x : E), x Si.fst f x b Si.snd})
@[protected]
theorem continuous_linear_map.has_basis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_6} [module 𝕜₁ E] [module 𝕜₂ F]  :
(nhds 0).has_basis (λ (SV : set E × set F), SV.snd nhds 0) (λ (SV : set E × set F), {f : E →SL[σ] F | (x : E), x SV.fst f x SV.snd})
@[simp]
theorem continuous_linear_map.precomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : E →SL[σ] F) (f : F →SL[τ] G) :
= f.comp L
@[simp]
theorem continuous_linear_map.precomp_coe_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : E →SL[σ] F) (f : F →SL[τ] G) :
= f.comp L
def continuous_linear_map.precomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : E →SL[σ] F) :
(F →SL[τ] G) →L[𝕜₃] E →SL[ρ] G

Pre-composition by a fixed continuous linear map as a continuous linear map. Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.

Equations
@[simp]
theorem continuous_linear_map.postcomp_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : F →SL[τ] G) (f : E →SL[σ] F) :
= L.comp f
def continuous_linear_map.postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : F →SL[τ] G) :
(E →SL[σ] F) →SL[τ] E →SL[ρ] G

Post-composition by a fixed continuous linear map as a continuous linear map. Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.

Equations
@[simp]
theorem continuous_linear_map.postcomp_coe_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [module 𝕜₁ E] [module 𝕜₂ F] [module 𝕜₃ G] (L : F →SL[τ] G) (f : E →SL[σ] F) :
= L.comp f
@[simp]
theorem continuous_linear_equiv.arrow_congrSL_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [ E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ σ₂₁] [ σ₁₂] [ σ₄₃] [ σ₃₄] [ σ₁₄ σ₂₄] [ σ₄₃ σ₂₃] [ σ₂₃ σ₁₃] [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) :
((e₁₂.arrow_congrSL e₄₃).symm) L = (e₄₃.symm).comp (L.comp e₁₂)
@[simp]
theorem continuous_linear_equiv.arrow_congrSL_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [ E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ σ₂₁] [ σ₁₂] [ σ₄₃] [ σ₃₄] [ σ₁₄ σ₂₄] [ σ₄₃ σ₂₃] [ σ₂₃ σ₁₃] [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) :
(e₁₂.arrow_congrSL e₄₃) L = e₄₃.comp (L.comp (e₁₂.symm))
@[simp]
theorem continuous_linear_equiv.arrow_congrSL_to_linear_equiv_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [ E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ σ₂₁] [ σ₁₂] [ σ₄₃] [ σ₃₄] [ σ₁₄ σ₂₄] [ σ₄₃ σ₂₃] [ σ₂₃ σ₁₃] [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : F →SL[σ₂₃] G) :
((e₁₂.arrow_congrSL e₄₃).to_linear_equiv.symm) L = (e₄₃.symm).comp (L.comp e₁₂)
@[simp]
theorem continuous_linear_equiv.arrow_congrSL_to_linear_equiv_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [ E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ σ₂₁] [ σ₁₂] [ σ₄₃] [ σ₃₄] [ σ₁₄ σ₂₄] [ σ₄₃ σ₂₃] [ σ₂₃ σ₁₃] [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : E →SL[σ₁₄] H) :
((e₁₂.arrow_congrSL e₄₃).to_linear_equiv) L = e₄₃.comp (L.comp (e₁₂.symm))
def continuous_linear_equiv.arrow_congrSL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [ E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ σ₂₁] [ σ₁₂] [ σ₄₃] [ σ₃₄] [ σ₁₄ σ₂₄] [ σ₄₃ σ₂₃] [ σ₂₃ σ₁₃] [ σ₃₄ σ₁₄] [ σ₃₄ σ₂₄] [ σ₂₄ σ₁₄] [ring_hom_isometric σ₁₂] [ring_hom_isometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
(E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G

A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.

Equations
def continuous_linear_equiv.arrow_congr {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [ E] [ F] [ G] [ H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) :
(E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G

A pair of continuous linear equivalences generates an continuous linear equivalence between the spaces of continuous linear maps.

Equations