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_topologyis the topology mentioned above for an arbitrary𝔖.continuous_linear_map.topological_spaceis the topology of bounded convergence. This is declared as an instance.
Main statements #
continuous_linear_map.strong_topology.topological_add_groupandcontinuous_linear_map.strong_topology.has_continuous_smulshow that the strong topology makesE →L[𝕜] Fa topological vector space, with the assumptions on𝔖mentioned above.continuous_linear_map.topological_add_groupandcontinuous_linear_map.has_continuous_smulregister these facts as instances for the special case of bounded convergence.
References #
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)
[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)) :
topological_space (E →SL[σ] F)
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)) :
uniform_space (E →SL[σ] F)
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)) :
uniform_add_group (E →SL[σ] F)
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)) :
topological_add_group (E →SL[σ] F)
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) :
has_continuous_smul 𝕜₂ (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)
[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) :
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 𝔖) :
@[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] :
topological_space (E →SL[σ] 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] :
topological_add_group (E →SL[σ] 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] :
has_continuous_smul 𝕜₂ (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}
[add_comm_group E]
[module 𝕜₁ E]
[add_comm_group F]
[module 𝕜₂ F]
[topological_space E]
[uniform_space F]
[uniform_add_group F] :
uniform_space (E →SL[σ] 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] :
uniform_add_group (E →SL[σ] 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) :
@[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] :
@[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) :
⇑(continuous_linear_map.precomp G L) f = 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 𝕜₃]
{σ : 𝕜₁ →+* 𝕜₂}
{τ : 𝕜₂ →+* 𝕜₃}
{ρ : 𝕜₁ →+* 𝕜₃}
[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) :
⇑↑(continuous_linear_map.precomp G L) f = f.comp L
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) :
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.
@[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) :
⇑(continuous_linear_map.postcomp E L) f = L.comp 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) :
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.
@[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) :
⇑↑(continuous_linear_map.postcomp E L) 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}
[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) :
@[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) :
@[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) :
A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.
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) :
A pair of continuous linear equivalences generates an continuous linear equivalence between the spaces of continuous linear maps.
Equations
- e₁.arrow_congr e₂ = e₁.arrow_congrSL e₂