# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: associates R -> ideal R

#### Kevin Buzzard (Sep 06 2020 at 16:59):

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.

Last updated: May 16 2021 at 05:21 UTC