Quotient Lift Linear Order

Stream: new members

[Prathik Diwakar]

Is there some way to lift a linear order on a group (OrderedAddCommGroup) to a quotient?
Something similar to QuotientGroup.lift, which would a relation (an order) to the quotient group.

[Eric Wieser]

What would lifting the order on $\mathbb{R}$ to $\mathbb{R}/\mathbb{Z}$ (add_circle 1) mean?

[Reid Barton]

I assume the quotient is by a convex subgroup

[Eric Wieser]

I would guess that docs#quotient.rec_on_subsingleton₂' / docs4#Quotient.recOnSubsingleton₂' is the tool you need

[Eric Wieser]

Unfortunately neither of those links works because zulip drops the 2...

[Prathik Diwakar]

Eric Wieser said:

What would lifting the order on $\mathbb{R}$ to $\mathbb{R}/\mathbb{Z}$ (add_circle 1) mean?

Sorry for the confusion. What we actually have is a (total) preorder on an additive commutative group G such that the normal subgroup N contains precisely those elements that are both positive and negative. We wish to lift this to the quotient G/N where it would turn into a (total) order.
Is there anything we could use that would help us here?

[Eric Wieser]

quotient.rec_on_subsingleton₂' will let you lift the underlying relations (lt and le)

[Johan Commelin]

Probably docs#function.surjective.linear_order doesn't exist...

[Prathik Diwakar]

Thank you for the help

[Yaël Dillies]

You want docs#antisymmetrization

[Karthik 🦋]

Thanks, this looks like exactly what we want!

[Yaël Dillies]

I will write the instance Reid is mentioning. It turns out I need it to define the Picard group of a graph.