Subobject correspondences

Stream: maths

[Aaron Anderson]

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]

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

[Aaron Anderson]

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]

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]

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]

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

[Aaron Anderson]

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]

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]

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]

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