Zulip Chat Archive

Stream: maths

Topic: Subobject correspondences


Aaron Anderson (Dec 30 2020 at 19:35):

I'd like to refactor the functions of the form sub____.(co)map to be preorder_homs. This does, however, remove the nice syntax of s.map f, so it'd have to be sub____.map f s. Does anyone have an issue with this?

Bryan Gin-ge Chen (Dec 30 2020 at 19:37):

Would it be possible to add aliases that enable dot notation?

Aaron Anderson (Dec 30 2020 at 19:37):

I'd also like to make some special cases of these (dealing with injective or surjective homomorphisms) into order_embeddings, and even order_isos onto intervals, but at the moment, the preorder_homs might not help as much as I might guess in defining order_embeddings and order_isos, because the latter are defined in terms of rel_homs.

Aaron Anderson (Dec 30 2020 at 19:38):

Bryan Gin-ge Chen said:

Would it be possible to add aliases that enable dot notation?

I'm not sure why not, but I don't know how to go about that.

Aaron Anderson (Dec 30 2020 at 19:39):

I also might start by directly creating the special case order_embeddings and order_isos, and try to integrate them into a better picture of order-preserving maps later

Bryan Gin-ge Chen (Dec 30 2020 at 19:40):

You can use command#alias to add copies of declarations with different names.

Aaron Anderson (Dec 30 2020 at 19:54):

So basically define something like submodule.map_preorder_hom with use case submodule.map_preorder_hom f s, which processes as (submodule.map_preorder_hom f) s where submodule.map_preorder_hom f goes through a coe_to_fn, and then make an alias submodule.map such that submodule.map f s = submodule.map_preorder_hom f s?

Aaron Anderson (Dec 30 2020 at 19:54):

Aaron Anderson said:

I'd also like to make some special cases of these (dealing with injective or surjective homomorphisms) into order_embeddings, and even order_isos onto intervals, but at the moment, the preorder_homs might not help as much as I might guess in defining order_embeddings and order_isos, because the latter are defined in terms of rel_homs.

(I'm seeing that the fastest route to these doesn't go through the regular preorder_hom at all, but through the Galois (co)insertions that are already defined)

Bryan Gin-ge Chen (Dec 30 2020 at 19:58):

Aaron Anderson said:

So basically define something like submodule.map_preorder_hom with use case submodule.map_preorder_hom f s, which processes as (submodule.map_preorder_hom f) s where submodule.map_preorder_hom f goes through a coe_to_fn, and then make an alias submodule.map such that submodule.map f s = submodule.map_preorder_hom f s?

It does look kind of complicated when written out like that, but if we can still write s.map f then I think it's worth it.

Eric Wieser (Dec 31 2020 at 08:41):

alias is not reducible, so I imagine you want abbreviation here


Last updated: Dec 20 2023 at 11:08 UTC