## 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: May 16 2021 at 05:21 UTC