Zulip Chat Archive

Stream: Is there code for X?

Topic: linear_map congr

Antoine Labelle (Apr 29 2022 at 14:10):

Do we have the following, or something similar when R is a commutative semiring and M, N, P, Q are R-module? 

linear_map.congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (M →ₗ[R] N) ≃ₗ[R] (P →ₗ[R] Q)

Antoine Labelle (Apr 29 2022 at 14:11):

Or a variant with another semiring S and some smul_comm_class R S _ in the case where R is not commutative.

Eric Rodriguez (Apr 29 2022 at 14:15):

docs#linear_equiv.arrow_congr ?

Eric Rodriguez (Apr 29 2022 at 14:15):

found with judicious regex

Antoine Labelle (Apr 29 2022 at 14:32):

What does regex mean? :sweat_smile:

Johan Commelin (Apr 29 2022 at 14:34):

regular expression

Oliver Nash (Apr 29 2022 at 14:35):

https://xkcd.com/208/

Antoine Labelle (Apr 29 2022 at 15:49):

I'd still also like a version that doesn't assume commutativity. Would that exist?

Eric Rodriguez (Apr 29 2022 at 15:52):

I have a feeling that if you follow the rabbit-hole of generalisations from https://gist.github.com/riccardobrasca/725a5a8c1390cc8add3f31d43cf2881c (specifically line 5948 and downish) you'll be able to get this

Eric Rodriguez (Apr 29 2022 at 15:56):

in fact, this seems to work already:

def arrow_congr {R M₁ M₂ M₂₁ M₂₂ : Sort*} [semiring R]
  [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid M₂₂]
  [module R M₁] [module R M₂] [module R M₂₁] [module R M₂₂] [smul_comm_class R R M₂₂]
  [smul_comm_class R R M₂₁]
  (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
  (M₁ →ₗ[R] M₂₁) ≃ₗ[R] (M₂ →ₗ[R] M₂₂) :=
{ to_fun := λ f : M₁ →ₗ[R] M₂₁, (e₂ : M₂₁ →ₗ[R] M₂₂).comp $ f.comp (e₁.symm : M₂ →ₗ[R] M₁),
  inv_fun := λ f, (e₂.symm : M₂₂ →ₗ[R] M₂₁).comp $ f.comp (e₁ : M₁ →ₗ[R] M₂),
  left_inv := λ f, by { ext x, simp only [symm_apply_apply, comp_app, coe_comp, coe_coe]},
  right_inv := λ f, by { ext x, simp only [comp_app, apply_symm_apply, coe_comp, coe_coe]},
  map_add' := λ f g, by { ext x, simp only [map_add, add_apply, comp_app, coe_comp, coe_coe]},
  map_smul' := λ c f, by { ext x, simp only [smul_apply, comp_app, coe_comp, map_smulₛₗ, coe_coe]} }

(I just changed the types a little)

Eric Rodriguez (Apr 29 2022 at 15:57):

I'm surprised the linter didn't pick this up, maybe this is beyond the scope (cc @Alex J. Best )

Antoine Labelle (Apr 29 2022 at 16:00):

I think the most general version should probably involve another semiring S and e₂ should be both R-linear and S linear (I don't even know if we have a way to talk about such doubly linear maps/equivs).

Antoine Labelle (Apr 29 2022 at 16:08):

For the application I have in mind I think I'll just state it with the explicit e₂.to_linear_map ∘ₗ f ∘ₗ e₁.symm.to_linear_map.

Last updated: Dec 20 2023 at 11:08 UTC