LocallyFiniteOrderBot instance for Fintype

Stream: Is there code for X?

[Michael Rothgang]

I need this for a piece of code in differential geometry. (I'm applying the Gram-Schmidt algorithm to a set of basis vectors: finiteness means my manifolds are finite-dimensional, which is fine.) Gram-Schmidt has certain hypotheses on the index set, and boom, I'm in order theory instance hell. Any help is appreciated.

MWE, importing Classical just to be sure:

import Mathlib
variable {α : Type*} [Fintype α] [Preorder α]
open Classical
#synth LocallyFiniteOrderBot α -- fails

I have found e.g. docs#Fintype.toLocallyFiniteOrder - it would suffice to have docs#OrderBot and docs#LinearOrder instances. The latter exists for Fin, but not for fintypes; the forder seems completely missing.

[Aaron Liu]

We have docs#Fintype.toOrderBot

[Aaron Liu]

Then you can use docs#Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot
not sure why it's in the finset namespace as the corresponding order top one isn't

[Michael Rothgang]

Thanks I had not seen this!

[Michael Rothgang]

So, is there also something for Fintype having some LinearOrder?

[Aaron Liu]

I'm not sure what you want

[Aaron Liu]

can you state it in Lean?

[Michael Rothgang]

Sure:

import Mathlib
variable {α : Type*} [Fintype α] [Preorder α]
open Classical -- just out of paranoia
#synth LinearOrder α

[Yaël Dillies]

Wait, how would this work? Not all finite preorders are linear!

[Michael Rothgang]

Right; I was imprecise:

import Mathlib
variable {α : Type*} [Fintype α]
open Classical -- just out of paranoia
#synth LinearOrder α -- just give me any linear order, please

[Aaron Liu]

docs#AsLinearOrder

[Aaron Liu]

hmm, not this one

[Aaron Liu]

docs#LinearExtension

[Aaron Liu]

yes, this one seems correct

[Aaron Liu]

just instantiate your type with any old partial order and then do the linear extension

[Yaël Dillies]

More down to earth: pull back along docs#Fintype.equivFin

[Michael Rothgang]

I can't find "pull back an order along an Equiv" using loogle. Do you have a hint?

[Yaël Dillies]

Tough luck, it doesn't seem to exist!

[Yaël Dillies]

We have docs#Equiv.addCommGroup, but not docs#Equiv.linearOrder

[Michael Rothgang]

Thanks! So let me add that definition. Progress so far:

protected abbrev preorder [Preorder β] : Preorder α where
  le a b := (e a) ≤ (e b)
  le_refl a := le_refl (e a)
  le_trans a b c h h' := Preorder.le_trans (e a) (e b) (e c) h h'

protected abbrev linearOrder [instβ: LinearOrder β] : LinearOrder α where
  toPreorder := e.preorder
  le_antisymm a b h h' := by
    rw [← e.left_inv a, ← e.left_inv b, toFun_as_coe, instβ.le_antisymm _ _ h h']
  le_total a b := instβ.le_total (e a) (e b)
  toDecidableEq := sorry
  toDecidableLE := sorry

[Michael Rothgang]

(To be continued...)

[Michael Rothgang]

I'm done except for one sorry: help with that is appreciated; then I'm happy to make a PR.

import Mathlib
variable {α β : Type*} (e : α ≃ β)

protected abbrev _root_.Equiv.preorder [Preorder β] : Preorder α where
  le a b := (e a) ≤ (e b)
  le_refl a := le_refl (e a)
  le_trans a b c h h' := Preorder.le_trans (e a) (e b) (e c) h h'

def foo {α β : Type*} {a b : α} (f : α → β) (h : Decidable (a = b)) : Decidable (f a = f b) := by
  sorry

protected abbrev _root_.Equiv.linearOrder [instβ: LinearOrder β] : LinearOrder α where
  toPreorder := e.preorder
  le_antisymm a b h h' := by
    rw [← e.left_inv a, ← e.left_inv b, _root_.Equiv.toFun_as_coe, instβ.le_antisymm _ _ h h']
  le_total a b := instβ.le_total (e a) (e b)
  toDecidableEq a b := by
    rw [← e.left_inv a, ← e.left_inv b]
    apply foo e.symm (instβ.toDecidableEq ..)
    -- exact Classical.propDecidable ... works, but is inelegant
  toDecidableLE a b := instβ.toDecidableLE ..

[Aaron Liu]

Can you transfer all the other fields of LinearOrder too?

[Aaron Liu]

also foo is false not possible to make computable

[Aaron Liu]

import Mathlib

variable {α β : Type*} (e : α ≃ β)

protected abbrev Equiv.preorder [Preorder β] : Preorder α :=
  Preorder.lift e

protected abbrev Equiv.partialOrder [PartialOrder β] : PartialOrder α :=
  PartialOrder.lift e e.injective

protected abbrev Equiv.linearOrder [instβ : LinearOrder β] : LinearOrder α where
  __ := e.partialOrder
  le_total a b := instβ.le_total (e a) (e b)
  toDecidableEq := e.injective.decidableEq
  toDecidableLE a b := instβ.toDecidableLE (e a) (e b)
  toDecidableLT a b := instβ.toDecidableLT (e a) (e b)
  min a b := e.symm (min (e a) (e b))
  max a b := e.symm (max (e a) (e b))
  compare a b := compare (e a) (e b)
  min_def a b := e.symm_apply_eq.2 ((min_def (e a) (e b)).trans (apply_ite e (e a ≤ e b) a b).symm)
  max_def a b := e.symm_apply_eq.2 ((max_def (e a) (e b)).trans (apply_ite e (e a ≤ e b) b a).symm)
  compare_eq_compareOfLessAndEq a b :=
    let := e.injective.decidableEq
    compare_of_injective_eq_compareOfLessAndEq a b e e.injective

[Eric Wieser]

docs#LinearOrder.lift' is what you need here

[Eric Wieser]

Michael Rothgang said:

I can't find "pull back an order along an Equiv" using loogle. Do you have a hint?

As usual, this is because you don't need an Equiv for it to be true; Injective suffices

[Aaron Liu]

Eric Wieser said:

Michael Rothgang said:

I can't find "pull back an order along an Equiv" using loogle. Do you have a hint?

As usual, this is because you don't need an Equiv for it to be true; Injective suffices

You do need an Equiv to lift the max and min fields

[Kevin Buzzard]

You only need surjective to do that ;-)

[Michael Rothgang]

Fair enough, I'll take this into account :-)

[Aaron Liu]

Kevin Buzzard said:

You only need surjective to do that ;-)

So you need both injective and surjective, so you need bijective, and Function.surjInv is always inferior to an explicit inverse, so throw in an explicit inverse too, and whoops it's turned into an Equiv.

[Michael Rothgang]

So I would only add this one, right? (If so, I can make a PR soon.)

[Michael Rothgang]

noncomputable instance Fintype.instLinearOrder {α : Type*} [Fintype α] : LinearOrder α :=
  LinearOrder.lift' _ (Fintype.equivFin α).injective

[Michael Rothgang]

Is this an instance we'd want to have, given it's noncomputable?

[Aaron Liu]

definitely don't make that a global instance

[Aaron Liu]

we don't want arbitrary linear orders on every Fintype

[Kevin Buzzard]

It would probably create a diamond for Fin n as well.

[Eric Wieser]

It would probably create a diamond for every finite type

[Eric Wieser]

Eg Prod (Fin 2) (Fin 2) would get the wrong order

[Eric Wieser]

What you have above is rarely what you want I think? What I think is more common is to want to construct a LinearOrder that is compatible with an existing preorder, such that related elements in the original have the same relation in the extended order

[Aaron Liu]

Eric Wieser said:

What you have above is rarely what you want I think? What I think is more common is to want to construct a LinearOrder that is compatible with an existing preorder, such that related elements in the original have the same relation in the extended order

that is docs#LinearExtension

[Aaron Liu]

but of course you need a partial order

[Michael Rothgang]

In my case, there's no canonical preorder either... but I agree this may be the exceptional case

[Bhavik Mehta]

While I prefer Yaël's approach above, you could also take the empty preorder (x <= x and nothing else), then use the extension theorem above to get a linear order. Another approach still is to use the well-ordering theorem to put a well-order on your type, which will be a linear order!

[Aaron Liu]

The best part is, you can't prove any of these approaches give the same result in the nontrivial case (this is why it shouldn't be a global instance)

[Michael Rothgang]

PRed as #27020