LinearMap.ker congr lemmas

Stream: mathlib4

[Winston Yin (尹維晨)]

It is great that LinearMap.ker is defined to accommodate any type in SemilinearMapClass. However, in actual use, it appears to be missing a congr lemma, for when its argument may be of a different type but is the same underlying function. For example (#30595), I needed this additional line

have : ker (ContinuousLinearMap.fst 𝕜 E F) = ker (LinearMap.fst 𝕜 E F) := rfl

in order to apply a rewrite with LinearMap.ker_fst.

Adding congr lemmas for LinearMap.ker would also mean adding it for LinearMap.range, and perhaps their underlying Submodule.comap and Submodule.map. Since this is somewhat core to the algebra library, I'd like to make sure it's not an #xy problem.

[Yaël Dillies]

Winston Yin (尹維晨) said:

It is great that LinearMap.ker is defined to accommodate any type in SemilinearMapClass.

It is not so great at all for precisely the reason you mention! There's ongoing work to "ungeneralise" it

[Winston Yin (尹維晨)]

Oh thank you. In that case, I will leave my code the way it is?

[Winston Yin (尹維晨)]

And is there a thread that discusses this ungeneralisation?

[Yaël Dillies]

Yes there is, but in the secret reviewers stream unfortunately (we wanted to get all reviewers on board before discussing it more broadly)

[Darij Grinberg]

is this about "kernel (congruence)" vs "kernel (submodule)"?

[Ruben Van de Velde]

No

[Ruben Van de Velde]

It's about the kernel of a linear map, for multiple related but not identical formal interpretations of "linear map"

[Darij Grinberg]

ah