mathlib3 documentation

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 #

Main statements #

References #

TODO #

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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group 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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [ring_hom_surjective σ] [ring_hom_isometric σ] [topological_space F] [topological_add_group F] [has_continuous_smul 𝕜₂ F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (h𝔖₃ : (S : set E), S 𝔖 bornology.is_vonN_bounded 𝕜₁ S) :
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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group F] {ι : Type u_4} (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {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) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :
(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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [ring_hom_surjective σ] [ring_hom_isometric σ] [topological_space F] [topological_add_group F] [has_continuous_smul 𝕜₂ 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [uniform_space F] [uniform_add_group 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group F] [has_continuous_smul 𝕜₁ 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group F] {ι : Type u_3} {p : ι Prop} {b : ι set F} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (λ (Si : set E × ι), bornology.is_vonN_bounded 𝕜₁ Si.fst 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} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E] [topological_space F] [topological_add_group F] :
(nhds 0).has_basis (λ (SV : set E × set F), bornology.is_vonN_bounded 𝕜₁ SV.fst 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 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [ring_hom_surjective σ] [ring_hom_isometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) :
@[simp]
theorem continuous_linear_map.precomp_coe_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [ring_hom_surjective σ] [ring_hom_isometric σ] (L : E →SL[σ] F) (f : F →SL[τ] G) :
def continuous_linear_map.precomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] {E : Type u_4} {F : Type u_6} (G : Type u_8) [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [ring_hom_surjective σ] [ring_hom_isometric σ] (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 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group F] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] F) :
def continuous_linear_map.postcomp {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [normed_field 𝕜₁] [normed_field 𝕜₂] [normed_field 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group F] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₂ F] (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 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [ring_hom_comp_triple σ τ ρ] (E : Type u_4) {F : Type u_6} {G : Type u_8} [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [add_comm_group G] [module 𝕜₃ G] [topological_space E] [topological_space F] [topological_space G] [topological_add_group F] [topological_add_group G] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₂ F] (L : F →SL[τ] G) (f : E →SL[σ] 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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃] [nontrivially_normed_field 𝕜₄] [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃] [nontrivially_normed_field 𝕜₄] [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃] [nontrivially_normed_field 𝕜₄] [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃] [nontrivially_normed_field 𝕜₄] [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃] [nontrivially_normed_field 𝕜₄] [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄] [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃] [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄] [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} [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H] [nontrivially_normed_field 𝕜] [module 𝕜 E] [module 𝕜 F] [module 𝕜 G] [module 𝕜 H] [topological_space E] [topological_space F] [topological_space G] [topological_space H] [topological_add_group G] [topological_add_group H] [has_continuous_const_smul 𝕜 G] [has_continuous_const_smul 𝕜 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