algebra hom morphism refactor

Stream: general

[Jireh Loreaux]

@Yaël Dillies and @Anne Baanen: what's the current word on algebra homomorphisms in relation to the morphism refactor? I would like to define star algebra homomorphisms, but I'm hesitant because algebra homomorphisms haven't yet been done.

[Yaël Dillies]

Work is ongoing at branch#linear_map_class. Not sure whether Anne needs help or time.

[Yaël Dillies]

Actually, don't algebra homs and star algebra homs bear the same relation as linear maps and semilinear maps?

[Anne Baanen]

Yaël Dillies said:

Work is ongoing at branch#linear_map_class. Not sure whether Anne needs help or time.

I haven't had much time in the past weeks to work on this. There are a few complications because the generic map_smul\_sl lemmas aren't being picked up by the simplifier for some reason. Any help would be very much appreciated!

[Jireh Loreaux]

No, star algebra homs are not analogous to semilinear maps. A star algebra hom is just an algebra hom which is star-preserving. A star algebra hom has a coercion to a linear map. It's the star operation itself that is semilinear (in most familiar cases).

[Jireh Loreaux]

I'll have a look at that branch, but I'm not sure I'll be able to be any help. :sad:

[Anne Baanen]

I pushed a new version with some merge conflicts fixed (hopefully...). Let's see what breaks.

[Jireh Loreaux]

This might be a bad analysis, but it seems to me like the lift.tprod bit on which it's stuck now is because of a confluence of two issues. The first is that the underlying ring for the module is now a metavariable and has to be inferred, which is normally not a problem since it is an out_param. However, in this case, we are also dealing with the pi-type instance issue, and it's having trouble reconciling the two (I think because each is looking to the other to tell it what the underlying ring should be?).

[Frédéric Dupuis]

I managed to get this branch (i.e. branch#linear_map_class) to compile locally! @Anne Baanen is it OK with you if I just push the result?

[Anne Baanen]

Nice work, thank you! Please do push your changes, I'm excited to see it working :)

[Frédéric Dupuis]

Pushed! Let's see what CI has to say...

[Anne Baanen]

Oh no, build failed :(

[Frédéric Dupuis]

I just merged master. I think we're getting close to a PR!

[Anne Baanen]

Thanks! The code is looking good so I'll go ahead and open a PR: #13939

[Anne Baanen]

The code is up to date and builds again!