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*

[Yury G. Kudryashov]

I've tried to give it a go. So far, the main inconvenience is that Lean can't automatically coerce f : M →L[R] N to an unknown semilinear map, so p.map f requires an explicit type annotation.

[Yury G. Kudryashov]

Can we change Coe* instances somehow to make it "just work"?

[Yaël Dillies]

This is the "functorial coercion" business we have been talking about for a while, no?

[Yury G. Kudryashov]

I think I've missed the discussions because of my day job.

[Yury G. Kudryashov]

Is there any consensus about what should we do?

[Yaël Dillies]

Once #mathlib4 > Mathlib's morphism hierarchy is done, you will be able to write f.toLinearMap without fearing for simp normal form. For coercions however, no concrete plan was ever given.

[Monica Omar]

I'm confused, is this about LinearMap.ker/range? or something else?

[Yury G. Kudryashov]

More specifically, it's about Submodule.map. I don't want to write p.map f.toLinearMap. I want to write p.map f and let Lean find *.toLinearMap as a coercion.

[Yury G. Kudryashov]

I've redefined LinearMap.ker, LinearMap.range, Submodule.map, and Submodule.comap to take LinearMaps, and I'm gettings lots of these errors.

[Monica Omar]

Let's start with ker and range for now. We can deal with Submodule.co(map) separately?

[Monica Omar]

Specifically for the range and kernel, I don't think we mind doing .toLinearMap.ker/range do we?

[Monica Omar]

it's basically the same amount of effort as LinearMap.range f

[Yury G. Kudryashov]

For ker and range, we can write f.ker.

[Yury G. Kudryashov]

If we don't do Submodule.map/comap in the same PR, then we need to do map_top and comap_bot for different types.

[Monica Omar]

Ah, I see. Okay, obviously in the same PR then.

[Monica Omar]

for continuous linear maps, do you also need to do p.map f.toLinearMap or does p.map f work? nvm, I just reread the first message

[Yury G. Kudryashov]

I need f.toLinearMap or (f : explicit_type).

[Yury G. Kudryashov]

f.ker works because Lean allows us to call methods of a parent structure from an instance of a child structure via dot notation.

[Monica Omar]

If we don't do Submodule.map/comap in the same PR, then we need to do map_top and comap_bot for different types.

Can you not just use docs#LinearMapClass.linearMap?

[Monica Omar]

Can you draft-PR what you got so far so we can all have a look?

[Eric Wieser]

Monica Omar said:

Can you not just use docs#LinearMapClass.linearMap?

This is precisely the thing that we were converging on declaring a bad design, I think

[Yury G. Kudryashov]

#33241

[Eric Wieser]

Yury G. Kudryashov said:

I need f.toLinearMap or (f : explicit_type).

I wonder if we can use unification hints or extra coercion instances to make this better-behaved

[Monica Omar]

This is precisely the thing that we were converging on declaring a bad design, I think

The coercion from LinearMapClass to LinearMap is also bad design, right?

[Yury G. Kudryashov]

I guess that Eric missed "not" in your message. At least, I did first time I've read it.

[Yury G. Kudryashov]

Note that we can no longer have generic span_image etc lemmas.

[Yury G. Kudryashov]

Eric Wieser said:

Yury G. Kudryashov said:

I need f.toLinearMap or (f : explicit_type).

I wonder if we can use unification hints or extra coercion instances to make this better-behaved

I'm bad at this kind of metaprogramming (at least, for now).

[Aaron Liu]

Eric Wieser said:

Monica Omar said:

Can you not just use docs#LinearMapClass.linearMap?

This is precisely the thing that we were converging on declaring a bad design, I think

I thought this was fine, taking the morphism class into the concrete morphism

[Eric Wieser]

Yury G. Kudryashov said:

I guess that Eric missed "not" in your message. At least, I did first time I've read it.

"Can you not just use X?" to me means "let's use X it should be fine?". I guess what was meant was "Can you just not use X at all".

[Eric Wieser]

It's fine to have that helper definition to use in proofs, but it isn't the preferred form and so doesn't belong in theorem statements.

[Yury G. Kudryashov]

So, not only I misread this, but also failed to understand when I saw all the words :man_facepalming:

[Andrew Yang]

cc @Christian Merten who has a PR on this as well.

[Monica Omar]

That PR is about RingHom not LinearMap right?

[Monica Omar]

Yeah it is: #25138

[Yury G. Kudryashov]

I've fixed compile issues.