RingHomSurjective instance on linear equivalences

Stream: new members

[Alena Gusakov]

Hi all,
I'm running into this problem where Lean doesn't seem to recognize a RingHomSurjective instance on linear equivalences. Strangely enough, it works if I plug in e.toLinearMap, but not when I just plug in the equivalence directly. Here is my MWE, the error appears at the definition of h2:

import Mathlib.LinearAlgebra.Prod

universe u v

namespace Submodule

lemma thing (K : Type*) (V W : Type v) [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V]
  [Module K W] (p : Submodule K V) (e : V ≃ₗ[K] W) :
  map e.symm (map e p) = p := by
    have h2 := map_comp e.symm e p
    sorry

end Submodule

[Kenny Lau]

yeah that's one drawback of our XxxClass approach, which is that the coercions tend to get stuck a bit (here it's coercing from a LinearEquiv to LinearMap

[Kenny Lau]

the incongruence here is because map itself takes any SemilinearMapClass, but comp in your lemmas is specifically about linear maps

[Kenny Lau]

it works if you explicitly coerce them to LinearMap first:

import Mathlib.LinearAlgebra.Prod

universe u v

namespace Submodule

lemma thing (K : Type*) (V W : Type v) [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V]
    [Module K W] (p : Submodule K V) (e : V ≃ₗ[K] W) :
    map e.symm (map e p) = p := by
  rw [← map_coe_toLinearMap e.symm, ← map_coe_toLinearMap e]
  rw [← map_comp]
  sorry

end Submodule

[Alena Gusakov]

Yeah I figured out the coercion, but it doesn't match what I'm trying to prove

[Alena Gusakov]

Lemme get a better mwe, I did go down that road already and got stuck there too

[Kenny Lau]

the other thing is that .toLinearMap is the fastest way to convert it to a linear map but sadly it is not the canonical form, the canonical form is actually LinearMapClass.linearMap f

[Alena Gusakov]

Here is something closer to what I'm working with:

import Mathlib.LinearAlgebra.Prod

universe u v

namespace Submodule

lemma thing (K : Type*) (V W : Type v) [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V]
  [Module K W] (p q : Submodule K V) (e : V ≃ₗ[K] W) (hpq : map e p = map e q) :
  map e.symm (map e p) = q := by
    have h2 := map_comp e.toLinearMap e.symm.toLinearMap p
    sorry

end Submodule

[Kenny Lau]

there's no error for me

[Alena Gusakov]

Not for the linearmap coercion

[Alena Gusakov]

When I try to use h2 is where I run into problems

[Alena Gusakov]

My proof attempt is stuck at the following:

import Mathlib.LinearAlgebra.Prod

universe u v

namespace Submodule

lemma thing (K : Type*) (V W : Type v) [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V]
  [Module K W] (p q : Submodule K V) (e : V ≃ₗ[K] W) (hpq : map e p = map e q) :
  map e.symm (map e p) = q := by
    rw [← map_symm_eq_iff] at hpq
    have h2 := map_comp e.toLinearMap e.symm.toLinearMap p
    sorry

end Submodule

[Kenny Lau]

that's because the canonical coercion is not .toLinearMap, but rather LinearMapClass.linearMap, but luckily there's a lemma that rewrites exactly that, and afterwards you can use map_coe_toLinearMap as normal:

import Mathlib.LinearAlgebra.Prod

universe u v

namespace Submodule

lemma thing (K : Type*) (V W : Type v) [Field K] [AddCommGroup V] [AddCommGroup W] [Module K V]
  [Module K W] (p q : Submodule K V) (e : V ≃ₗ[K] W) (hpq : map e p = map e q) :
  map e.symm (map e p) = q := by
    have h2 := map_comp e.toLinearMap e.symm.toLinearMap p
    simp_rw [LinearEquiv.toLinearMap_eq_coe, map_coe_toLinearMap] at h2
    sorry

end Submodule

[Alena Gusakov]

Ah, perfect. Thanks!