LinearMap.ker / range not taking FunLike

Stream: mathlib4

[Alex Meiburg]

In response #33107, @Monica Omar suggested that LinearMap.ker and LinearMap.range should be changed to take a LinearMap itself instead of a SemilinearMapClass -- and that we should start a thread on Zulip.

I seem to recall a larger conversation about avoiding the use of functions taking these bundled FunLike and FooHomClass things, but I can't find it now...?

[Monica Omar]

here’s another related recent thread I just found: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/LinearMap.2Erange.20for.20ContinuousLinearMap/with/564194232

[Artie Khovanov]

@Yaël Dillies

[Aaron Liu]

#mathlib4 > Mathlib's morphism hierarchy

[Yaël Dillies]

Please do so!

[Yury G. Kudryashov]

I wonder if Lean will simplify inside (LinearMap.ker (ContinuousLinearMap.toLinearMap f) : Type _) to {x | f x = 0}.

[Yury G. Kudryashov]

See also #mathlib4 > Coercion of SetLike to Type*