Issues in !4#2788 (LinearAlgebra.Smodeq)

Stream: mathlib4

[Arien Malec]

I have no idea what's going on in this file.

We have declarations (f : M →ₗ[R] N) but every use of f applied to a module gives an error:

function expected at
  f
term has type
  M →ₗ[R] N

Nothing has changed here from Lean 3 -- is there some new thing that's required for linear maps to work?

(BTW -- Smodeq? SMODEq? )

[James Gallicchio]

(SModEq maybe?)

[Adam Topaz]

Something is clearly wrong here... even the definition of Smodeq is taking a really long time to elaborate.

[Adam Topaz]

well, maybe it's just an issue with linear maps:

import Mathlib

variable (R M N : Type _)
  [CommRing R]
  [AddCommGroup M]
  [AddCommGroup N]
  [Module R M]
  [Module R N]

example (m : M) (f : M →ₗ[R] N) : N := f m

^^^ that gives the same error at f m

[Adam Topaz]

Can someone remind me of the name of the option for typeclass instance tracing?

[Adam Topaz]

Well, I suppose trace.Meta.synthInstance is what I was looking for.

[Adam Topaz]

Well, looks like I won't have time to actually get anywhere in looking into this problem. But I think this is something that needs to be resolved ASAP.

[Adam Topaz]

The solution could just be as easy as adding an analogous FunLike instance for linear maps right next to this one
https://github.com/leanprover-community/mathlib4/blob/2941a8902b991e03a0bb57e4e5308ffc211a1439/Mathlib/Algebra/Module/LinearMap.lean#L225

[Adam Topaz]

It seems like @Anne Baanen was who ported the linear maps file... Anne do you have any idea what to do?

[Eric Wieser]

Adam Topaz said:

The solution could just be as easy as adding an analogous FunLike instance for linear maps right next to this one

That sounds like a good idea to me

[Arien Malec]

The second simplest thing that could work doesn't seem to. I tried adding:

instance : SemilinearMapClass (M →ₗ[R] M₂) (RingHom.id R) M M₂
    where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply FunLike.coe_injective'
    exact h
  map_add f := f.map_add'
  map_smulₛₗ := LinearMap.map_smul'

instance : FunLike (M →ₗ[R] M₂) M (λ _ ↦ M₂) :=
  { AddHomClass.toFunLike with }

to Algebra.Module.LinearMap

and still get the errors, as well as, confusingly:

failed to synthesize instance
  SemilinearMapClass (M →ₗ[R] N) ?m.106705 M ?m.106698

It's possible we also want a declaration for LinearMapClass for linear maps, but there's a lot of machinery there that needs someone familiar with it to assess.

[Eric Wieser]

What line do you get that error on?

[Eric Wieser]

set_option synthInstance.etaExperiment true in fixes most of the errors

[Eric Wieser]

change type at hyp seems to not work in that PR? The documentation for the change tactic says its legal though...

[Arien Malec]

Eric Wieser said:

What line do you get that error on?

Was every use of linear maps….

[Arien Malec]

Eric Wieser said:

change type at hyp seems to not work in that PR? The documentation for the change tactic says its legal though...

Every time I've seen that, it's been marked as unexpected syntax

[Mario Carneiro]

it's not implemented yet