Mono in partial order morphisms about math-comp HOT 7 CLOSED

substructure require strict monotonicity but it's "accidental", it happens to be non strict + injective

from math-comp.

@zstone1 thanks for pointing that out.

from math-comp.

@proux01 could we safely assume that this definition has not been used anywhere yet? Otherwise we need to consider a two-phase deprecation process (step 2. rename and deprecate the old name, have the right notion with a different name. step 2. rename the right notion with the original name)

from math-comp.

I'm probably the one who made the mistake. Order morphism where inspired by ring morphisms (in ssralg.v) and my goal was only to be able to transport order structures to subtypes. With all the work during the porting to hierarchy-builder, it probably didn't receive enough attention. So indeed I wouldn't be surprised if there is (a lot of) room for improvement here.

could we safely assume that this definition has not been used anywhere yet

No, it's used in dioid (for instance https://github.com/math-comp/dioid/blob/cf0cafea45c700230d97ddd9342baa1479a0c522/complete_lattice.v#L458 ), which I should probably add to CI. However it's only in master and I haven't released it, so I'm fine with skipping the deprecation process.

from math-comp.

With all the work during the porting to hierarchy-builder, it probably didn't receive enough attention.

Indeed, I accidentally discovered the existence of this structure last week, so I probably didn't pay enough attention to this addition, mea culpa.

However it's only in master and I haven't released it, so I'm fine with skipping the deprecation process.

Thanks that would be very helpful.

from math-comp.

iiuc, we need to keep the current order_morphism under a different name?

from math-comp.

Probably. I wonder whether we are not mixing two things (but maybe they are closely related) : monotonic functions (usually non strictly monotonic) and substructures for the order hierarchy (which require strict monotonicity ?).

from math-comp.