alg_hom from intermediate_field le

Stream: Is there code for X?

[Adam Topaz]

If I have A B : intermediate_field K L and A ≤ B, what's the idiomatic way to construct an algebra hom (over K) from A to B? I don't see an analogue of docs#subalgebra.inclusion

[Eric Wieser]

Does just using subalgebra.inclusion work?

[Eric Wieser]

I think they might be defeq

[Adam Topaz]

Oh maybe

[Eric Wieser]

Which isn't to say it's not worth adding the def you describe

[Adam Topaz]

Maybe after adding to_subalgebras

[Eric Wieser]

As types coe_sort A.to_subalgebra and coe_sort A are defeq

[Eric Wieser]

But you're right, the elaborator may need help