Zulip Chat Archive

Stream: Is there code for X?

Topic: Ordered groups have no top element


Heather Macbeth (Aug 14 2020 at 18:26):

Does this exist in some form? Also, is there a typeclass for not having a maximal element, the way that has_top is for having a maximal element?

import order.filter.at_top_bot
variables {β : Type*} [decidable_linear_ordered_add_comm_group β]

lemma exists_pos [nontrivial β] :  b : β, 0 < b :=
begin
  obtain a, ha :  a : β, a  0 := exists_ne 0,
  cases lt_or_gt_of_ne ha,
  { exact ⟨-a, neg_pos.mpr h },
  { exact a, h },
end

lemma not_has_top [nontrivial β] (c : β) :  c', c < c' :=
begin
  obtain b, hb :  b : β, 0 < b := exists_pos,
  exact c + b, lt_add_of_pos_right c hb
end

Reid Barton (Aug 14 2020 at 18:30):

For the second question, docs#no_top_order

Heather Macbeth (Aug 14 2020 at 18:37):

Ah good. So to rephrase, it seems I'm asking about the existence of

instance foo [decidable_linear_ordered_add_comm_group β] [nontrivial β] : no_top_order β

Heather Macbeth (Aug 14 2020 at 19:01):

By looking to see how one gets no_top_order ℤ, I discovered linear_ordered_semiring.​to_no_top_order.

The instance I wrote would supersede linear_ordered_semiring.​to_no_top_order. Should I make this replacement? on second thoughts, I guess not all linear ordered semirings are decidable. If there were a preexisting typeclass linear_ordered_add_comm_group, that would be the right way to do a grand unified theory.

Aaron Anderson (Aug 14 2020 at 19:58):

This exists for linear_ordered_fields, and apparently separately for linear_ordered_(semi)ring

Aaron Anderson (Aug 14 2020 at 20:01):

Is there a reason not to have all the classes just be linear_ordered_thingy and then have a mixin for the order being decidable?

Heather Macbeth (Aug 14 2020 at 20:13):

I completely agree. I think there are a lot of similar issues in the order hierarchy, actually. For example, this.

Heather Macbeth (Aug 14 2020 at 20:15):

But that'd be a big refactor. Maybe for now I will just PR a documentation comment to linear_ordered_semiring and linear_ordered_field, so that when (someday) a typeclass linear_ordered_add_comm_group is created, the person doing it remembers to prove this theorem for it.


Last updated: Dec 20 2023 at 11:08 UTC