Zulip Chat Archive

Stream: maths

Topic: from le to ge by duality?


view this post on Zulip Jalex Stark (May 07 2020 at 17:44):

I have a theorem about mins for an arbitrary linear order MM. I'd like to get the dual theorems about max by applying the first theorem to MopM^{op} and then reinterpreting them in MM. Is there any particular machinery to make this easier or should I just do it?

import tactic

import data.finset
import data.finsupp
import data.nat.basic


universes u
open_locale classical

open function

class DLO (α : Type u) extends decidable_linear_order α :=
(dense :  a b : α, (a < b)   c, a < c  c < b)
(without_top :  a : α,  b, a < b)
(without_bot :  a : α,  b, b < a)

variables {M N : Type u} [DLO M] [DLO N] [inhabited M] [inhabited N]
open pfun

example

-- given a finset in a DLO, produce an element below or above everything

def min_of_finset' (X : finset M) (X_nonempty : finset.nonempty X) :  l  X,  x  X, l  x := finset.exists_min X id X_nonempty

def lb_of_finset (X : finset M) :  l,  x X, l < x := begin
by_cases finset.nonempty X,
swap,
{   use arbitrary M,
    intro x, intro hx,
    unfold finset.nonempty at h, push_neg at h,
    exfalso, exact h x hx},
-- maybe using have and contradiction is mathier in the above
have m := min_of_finset' _ h,
cases m with m hm,
cases hm with m_in_X hm,
have key := DLO.without_bot m,
cases key with l hl,
use l,
intros x hx,
apply lt_of_lt_of_le hl,
apply hm, assumption,
end

view this post on Zulip Jalex Stark (May 07 2020 at 17:46):

Hmm I guess the answer is going to be that the machinery is in the category_theory library, so maybe I'll just do it "by hand" for now

view this post on Zulip Chris Hughes (May 07 2020 at 17:47):

You can use order_dual

view this post on Zulip Chris Hughes (May 07 2020 at 17:50):

The proof of the dual of lb_of_finset should be @lb_of_finset (order_dual M) _ _. You have to put the right DLO instance on order_dual M for this to work. Put an instance for the recerse order on it.

view this post on Zulip Chris Hughes (May 07 2020 at 17:50):

There should already be a linear_order instance.

view this post on Zulip Jalex Stark (May 07 2020 at 17:52):

hmm I don't know how to break up DLO so that I can give the linear_order and without_* instance separately

view this post on Zulip Jalex Stark (May 07 2020 at 17:53):

In other words, I don't understand what the constructor is for typeclass that's made via extends
so probably I can answer this by reading TPiL

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 17:59):

BTW, we already have class no_top_order

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:00):

Moreover, we have classes no_top_order, no_bot_order and densely_ordered

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:01):

So if you're writing for mathlib, then you can use [linear_order α] [no_bot_order α] [densely_ordered α]

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:02):

See also directed.finset_le and finset.exists_le in algebra/big_operators.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:03):

So, for finset.exists_lt you just need [nonempty α] [directed_order α] [no_bot_order α]

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:04):

Note that we don't have a dual to directed_order

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 18:05):

And we don't have any good instance for directed_order. You can easily add semilattice_inf.directed_order.

view this post on Zulip Jalex Stark (May 07 2020 at 18:22):

is there a way to bundle linear_order, no_top_order, no_bot_order and densely_ordered into one class?

view this post on Zulip Jalex Stark (May 07 2020 at 18:24):

I can do this but then I'm carrying around new names? I really want to chain the extends

class DLO' (α : Type u) extends decidable_linear_order α :=
(dense : densely_ordered α)
(without_top : no_top_order α )
(without_bot : no_bot_order α )

view this post on Zulip David Wärn (May 07 2020 at 19:42):

I had this issue a while ago (working on the same kata!) (link). Mario recommended the solution you describe. My understanding is that chaining all the extends is problematic because densely_ordered is parametrised by the order. You could at least combine no_top_order, no_bot_order and densely_ordered into one class?

In the end I decided against defining a new class, and just did the back-and-forth argument with assumptions decidable_linear_order, no_top_order, ... for both types.

view this post on Zulip David Wärn (May 07 2020 at 19:43):

Btw, I think you might want finset.max' / finset.min'?


Last updated: May 14 2021 at 18:28 UTC