Zulip Chat Archive

Stream: maths

Topic: continuous_linear_map.arrow_congr


Yury G. Kudryashov (Oct 19 2021 at 20:19):

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 (Oct 19 2021 at 20:55):

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 (Oct 19 2021 at 23:51):

Thank you!

Yury G. Kudryashov (Oct 19 2021 at 23:51):

I'll try it later tonight.


Last updated: Dec 20 2023 at 11:08 UTC