Zulip Chat Archive

Stream: general

Topic: Bundled order_embedding from algebraic substructures


Junyan Xu (Nov 07 2022 at 07:08):

In #17401 I made algebra.to_submodule an order_embedding, and I think the same could be done for all forgetful maps between lattices of algebraic substructures and for set_like.coe, which would save some boilerplate. Would be wonderful if someone does it systematically. There are some such maps that come from extends (e.g. docs#subalgebra.to_subsemiring) which aren't bundled by default though, so a new name would need to be assigned to the bundled version.

Junyan Xu (Nov 07 2022 at 07:11):

@Yaël Dillies I think you might be interested in this.

Yaël Dillies (Nov 07 2022 at 08:32):

We should be able to provide that for all function.injective.something_ordered, right?


Last updated: Dec 20 2023 at 11:08 UTC