Well behaved LinearOrder on Fintype

Stream: new members

[Igor Khavkine]

I'm want to use a well behaved linear order on a Fintype, but I'm confused about what typeclasses would ensure that. (Basically, I'd like to have an ordered indexing type that has the properties the integers from $1$ to $n$, like referring to smallest and largest elements.) I tried something, but I seem to have run into diamond issues in the typeclass hierarchy. Here's a #mwe:

import Mathlib.Data.Fintype.Order
import Mathlib.Order.CompletePartialOrder

theorem order_problem {ι : Type*} [hι : Fintype ι] [Nontrivial ι] [LinearOrder ι]
  (m : ι)
  (hm : IsBot m)  -- or this: (hm : ∀ i, m ≤ i)
    : ¬ IsMax m := by
  have hιclo := hι.toCompleteLinearOrderOfNonempty
  let M : ι := ⨆ i, i
  let Ms : Set ι := {M}
  exact IsBot.not_isMax hm  -- typeclass inference clash; interference from hιclo?
  -- really, I would like to show that m ∈ Msᶜ, but without hιclo already the definition of
  -- M complains about not being able to infer [SupSet ι]

What is the right combination of typeclasses to use in this case?

[Jz Pan]

This works:

import Mathlib.Data.Fintype.Order
import Mathlib.Order.CompletePartialOrder

theorem order_problem {ι : Type*} [Nontrivial ι] [PartialOrder ι]
    (m : ι) (hm : IsBot m) : ¬ IsMax m := by
  obtain ⟨n, hne⟩ := exists_ne m
  rw [not_isMax_iff]
  use n
  exact (hm n).lt_of_ne hne.symm

[Igor Khavkine]

Thanks for the quick reply! However, it doesn't really help me with the problem that I described in the comments in my mwe. If I had deleted hιclo and M, the code would have worked as is anyway. This is what I really want to do, but the typeclass inference system complains already at the attempt of specifying the goal type:

import Mathlib.Data.Fintype.Order
import Mathlib.Order.CompletePartialOrder

theorem order_problem {ι : Type*} [hι : Fintype ι] [Nontrivial ι] [LinearOrder ι]
    (m : ι) (hm : IsBot m) : m ∈ {⨆ i, i}ᶜ /- SupSet ι can't be inferred -/ := by
  sorry

My original mwe, I admit, was a bit artificially unfolded to show where the different problems appear.

[Kenny Lau]

@Igor Khavkine what you wrote makes no sense in pen-and-paper mathematics; what do you actually want to express?

[Kenny Lau]

uh... it looks like you just want to write \ne?

[Igor Khavkine]

What I want is to work (in a larger context) with indexed objects, say E : ι -> Type, where there are only finitely many index values i : ι and so that they have an order on them. Then I'd like do things like choose the least i (that would be m := ⨅ i, i), choose the greatest i (that would be M := ⨆ i, i), group the E i into subsets like {i <= k} and {i > k} for some k : ι, prove that these index subsets don't overlap, etc.

Now, a canonical choice for ι could be the integers from $1$ to $n$ (Fin n I guess), but as ι would appear in the hypotheses of a theorem, I'd like to abstract it to some Fintype ι with appropriate order properties. What I can't figure out is what typeclasses describe these order properties.

Intuitvely, Fintype ι and LinearOrder ι should be enough, because existence of minima, maxima, comparability should follow from that. I did find Fintype.toCompleteLinearOrderOfNonempty, which also uses Nonempty ι, but I had to invoke it manually as in my first mwe, and that also lead to incompatible typeclass inferences for simple expressions like ⨅ i, i and ⨆ i, i, or IsBot and IsMax.

The proposition m ∈ {M}ᶜ, where m is the minimum index, while M is the maximum index (when the index set has at least two elements) is just one of the simplest statements that I think I should be able to express and prove. Now all of this seems rather too complicated for what I'd like to do, so I'm quite certain that I'm taking a wrong approach somewhere...

[Kenny Lau]

@Igor Khavkine my question is, here m and M are two elements of ι right? so doesn't "m ∈ {M}ᶜ" just say m ≠ M?

[Igor Khavkine]

Yes, they are even definitionally equal, if I'm not mistaken. Sorry for the possibly over-complicated notation, I had reasons to use it where I copied it from, which are irrelevant here.

[Kenny Lau]

@Igor Khavkine

import Mathlib.Data.Fintype.Order
import Mathlib.Order.CompletePartialOrder

theorem order_problem {ι : Type*} [hι : Fintype ι] [Nontrivial ι] [LinearOrder ι]
    (m : ι) (hm : IsBot m) : letI := hι.toCompleteLinearOrderOfNonempty; m ∈ ({⨆ i, i}ᶜ : Set ι) := by
  letI := hι.toCompleteLinearOrderOfNonempty
  rw [iSup, Set.range_id', sSup_univ, hm.eq_bot]
  exact bot_ne_top

[Igor Khavkine]

@Kenny Lau Your example seems to be working for what I wanted to do. Thanks a lot!

The difference seems to be in using letI := hι.toCompleteLinearOrderOfNonempty(or wih let) vs have := hι.toCompleteLinearOrderOfNonempty as I was using. I didn't realize that it would make a difference here!

[Kenny Lau]

@Igor Khavkine have forgets the proof

[Kenny Lau]

which you don't want

[Kenny Lau]

because then you have no way to ensure that the two linear orders are the same

[Jz Pan]

You mean "have forgets the data"