Zulip Chat Archive

Stream: Is there code for X?

Topic: distinct


view this post on Zulip Adam Topaz (Feb 19 2021 at 18:21):

Suppose I have a type α\alpha and three terms x,y,z:αx,y,z : \alpha. What's the idiomatic way to say that x,y,zx,y,z are distinct?

view this post on Zulip Adam Topaz (Feb 19 2021 at 18:25):

My inclination is to be tricky with matrices:

import data.matrix.notation

def distinct {α : Type*} (x y z : α) := function.injective ![x,y,z]

view this post on Zulip Kevin Buzzard (Feb 19 2021 at 18:31):

This came up on the discord and whatever the idiomatic way is, it was generally agreed that the most helpful way was just x \ne y \and y \ne z \and z \ne x. A more fun question: if alpha is linearly ordered and your goal is S_3-invariant, how do you now prove WLOG x<y<z?

view this post on Zulip Adam Topaz (Feb 19 2021 at 18:32):

Okay, but now what if I have 5 elements?

view this post on Zulip Adam Topaz (Feb 19 2021 at 18:32):

I don't want to write too many things

view this post on Zulip Eric Wieser (Feb 19 2021 at 18:32):

Possibly [x,y,z].pairwise (≠)

view this post on Zulip Eric Wieser (Feb 19 2021 at 18:33):

Which should still give you helpful induction principles

view this post on Zulip Adam Topaz (Feb 19 2021 at 18:35):

I would still like a smaller proof, but this isn't too bad:

import data.matrix.notation

example {α : Type*} {a b c d e f g : α} (cond : function.injective ![a,b,c,d,e,f,g]) : c  g :=
cond.ne $ show (2 : fin 7)  6, by dec_trivial

view this post on Zulip Kevin Buzzard (Feb 19 2021 at 19:26):

Do you ever really have 5 elements in practice?

view this post on Zulip Adam Topaz (Feb 19 2021 at 19:27):

https://en.wikipedia.org/wiki/Complete_quadrangle

view this post on Zulip Adam Topaz (Feb 19 2021 at 19:28):

I can get by with 3, but I might need 5 in the future :)

view this post on Zulip Adam Topaz (Feb 19 2021 at 19:28):

I don't think I'll ever need 6 though.

view this post on Zulip Adam Topaz (Feb 19 2021 at 19:31):

This all started with the following lemma which I'm working on for some stuff with projective geometry:

lemma exists_unique_rep_of_colinear {x y z : proj K V} {v : V} :
  x.is_rep v  colinear x y z  (function.injective ![x,y,z]) 
  ∃! (w : V), y.is_rep w  z.is_rep (v + w) := sorry

view this post on Zulip Adam Topaz (Feb 19 2021 at 19:31):

(in some sense, this is the key lemma that makes the fundamental theorem of projective geometry actually work.)


Last updated: May 16 2021 at 05:21 UTC