associates R -> ideal R

Stream: Is there code for X?

[Kevin Buzzard]

For a monoid R (e.g. a commutative ring) we have the monoid associates R, the quotient of R by units R, and this is preordered in mathlib by divisibility. For a commutative ring we have the semiring ideal R of ideals. This we have.

There's a natural map from associates R to ideal R and if R is an integral domain then this map is injective and, unfortunately, order-reversing (3 divides 6, but the ideal (6) is a subset of the ideal (3)). Do we have this map? If not then I would appreciate advice on whether it should just go from associates R to ideal R or whether I should insert an order_dual somewhere. The bare map has the good monoid hom properties, but it inverts the ordering. It would be much easier to say "this bare map satisfies x <= y -> f(y) <= f(x)" than start putting monoid structures on order_dual X given one on X. More and more I am seeing instances of order-reversing maps as we push on with algebra in Lean. If R is a PID then this map is simultaneously an isomorphism of monoids and an anti-isomorphism of orders.