continuous_linear_map.arrow_congr

Stream: maths

[Yury G. Kudryashov]

I'm going to add continuous_linear_map.arrow_congr (eE : E₁ ≃L[R] E₂) (eF : F₁ ≃L[R] F₂) : (E₁ →L[R] F₁) ≃L[R] (E₂ →L[R] F₂). If someone wants this definition to respect semilinear maps/equivalences, then please tell me what are the correct assumptions on various σs that should appear in the signature.

[Frédéric Dupuis]

My guess is that something like continuous_linear_map.arrow_congr (eE : E₁ ≃SL[σ₁₂] E₂) (eF : F₁ ≃SL[σ₁₂] F₂) : (E₁ →L[R₁] F₁) ≃SL[σ₁₂] (E₂ →L[R₂] F₂) with {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] should work.

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I'll try it later tonight.