Diamond with ordered rings

Stream: general

[Wrenna Robson]

I'm getting something that looks quite a lot like a diamond when trying to prove something on a type that is both a conditionally_complete_linear_order and a linear_ordered_ring.

In particular, it looks as though I am getting these two instances of has_le:

  @has_le.le α
    (@preorder.to_has_le α
       (@partial_order.to_preorder α
          (@semilattice_inf.to_partial_order α
             (@lattice.to_semilattice_inf α
                (@conditionally_complete_lattice.to_lattice α
                   (@conditionally_complete_linear_order.to_conditionally_complete_lattice α _inst_3))))))

and

  @has_le.le α
    (@preorder.to_has_le α
       (@partial_order.to_preorder α
          (@ordered_add_comm_group.to_partial_order α
             (@ordered_ring.to_ordered_add_comm_group α (@linear_ordered_ring.to_ordered_ring α _inst_1)))))

And these are not, it seems, defeq. How can I avoid this problem: what is the right typeclass to use?

[Eric Rodriguez]

they both provide different les; you'd need to make a super-class that encompasses both

[Wrenna Robson]

Pfeh!

[Wrenna Robson]

So we don't have any way to talk about completeness properties of orders alongside orders on rings? (For context: was wanting to try and prove something like infi (fun x => floor (f x)) = floor (infi f).

[Junyan Xu]

You could mimic how src#conditionally_complete_linear_ordered_field is done.

[Yaël Dillies]

Aren't all conditionally complete linear ordered rings actually fields?

[Yaël Dillies]

Set a^-1 := infi (\la b, 1 <= a * b) for positive a.

[Kevin Buzzard]

Isn't the integers a counterexample?

[Adam Topaz]

Maybe some natural additional axiom is needed. A guess: add the condition that for all $a < b$ there exists some $c$ such that $a < c < b$

[Adam Topaz]

One might call that condition "non-locally-discrete" or something

[Yaël Dillies]

docs#densely_ordered

[Adam Topaz]

:)

[Adam Topaz]

you order theorists named everything

[Yaël Dillies]

Eheheh

[Kevin Buzzard]

How about $\Z[\sqrt{2}]$ then?

[Yaël Dillies]

Is that really conditionally complete?

[Kevin Buzzard]

Oh good point! I doubt it. So maybe you're right.

[Kevin Buzzard]

I'm still a bit worried about stuff like $\R[\epsilon]$ (a polynomial ring) with $\epsilon$ infinitely small but positive.

[Wrenna Robson]

Yaël Dillies said:

Set a^-1 := infi (\la b, 1 <= a * b) for positive a.

What if there is no such b?