English
A pair of continuous linear equivalences induces a canonical continuous linear equivalence between spaces of continuous linear maps.
Русский
Пара непрерывных линейных эквивалентностей порождает каноническое непрерывное линейное эквивалентное отображение между пространствами непрерывных линейных отображений.
LaTeX
$$$e_1 : E \\simeq_σ F, \\; e_4 : H \\simeq_τ G \\quad\\Rightarrow\\quad (E \\toSL[σ] H) \\simeqSL[τ] (F \\toSL[σ] G)$$$
Lean4
/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
spaces of continuous (semi)linear maps. -/
@[simps apply symm_apply toLinearEquiv_apply toLinearEquiv_symm_apply]
def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
{ e₁₂.arrowCongrEquiv e₄₃ with
-- given explicitly to help `simps`
toFun := fun L =>
(e₄₃ : H →SL[σ₄₃] G).comp
(L.comp (e₁₂.symm : F →SL[σ₂₁] E))
-- given explicitly to help `simps`
invFun := fun L => (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F))
map_add' := fun f g => by simp only [add_comp, comp_add]
map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ]
continuous_toFun :=
((postcomp F e₄₃.toContinuousLinearMap).comp (precomp H e₁₂.symm.toContinuousLinearMap)).continuous
continuous_invFun :=
((precomp H e₁₂.toContinuousLinearMap).comp (postcomp F e₄₃.symm.toContinuousLinearMap)).continuous }
