ordered pairs

Stream: new members

[Abhimanyu Pallavi Sudhir]

I'm defining a subset of the Cartesian product of two types, specifically:

def graph : set X × Y :=
    {(x : X, f x) | x : X}

(f is a function, x has not been separately defined) What's the right notation for this (the ordered pairs, and also the set builder itself)?

[Kenny Lau]

what do you mean by "right notation"?

[Abhimanyu Pallavi Sudhir]

A notation that works in Lean.

[Kenny Lau]

do you mean set (X × Y)?

[Kenny Lau]

oh

[Abhimanyu Pallavi Sudhir]

No, I mean for the ordered pairs.

[Kenny Lau]

universes u v
variables {X : Type u} {Y : Type v} (f : X → Y)
def graph : set (X × Y) :=
{ z | z.2 = f z.1 }

[Abhimanyu Pallavi Sudhir]

Ah.

[Abhimanyu Pallavi Sudhir]

Thanks.

[Kevin Buzzard]

It's kind of annoying that you can't write {⟨x,y⟩ : X × Y | y = f x}

[Kenny Lau]

you can't define that in ZFC either

[Kenny Lau]

you need to use specification and an existential

[Kevin Buzzard]

I guess you could use set.image or set.range, whatever it's called

[Kevin Buzzard]

def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩)

[Kevin Buzzard]

(after import data.set.basic)

[Kenny Lau]

import data.set.lattice
universes u v
variables {X : Type u} {Y : Type v} (f : X → Y)
def graph : set (X × Y) :=
⨆ x : X, {(x, f x)}

[Abhimanyu Pallavi Sudhir]

What's ⨆?

[Kevin Buzzard]

import data.set.basic

variables (X Y : Type) (f : X → Y)

def graph  : set (X × Y) := {z : X × Y | z.2 = f z.1}

def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩)

example : graph = graph' := sorry

[Kenny Lau]

set X is a complete lattice

[Kevin Buzzard]

Abhi: ⨆ is notation so you can start with #print notation ⨆

[Kevin Buzzard]

but if you don't want to go down the lattice rabbithole you could try my homework :-)

[Kevin Buzzard]

I'd be able to do the homework myself if I knew how to prove A = B iff B = A :-/

[Kevin Buzzard]

eq.symm only goes one way

[Kenny Lau]

eq_comm

[Abhimanyu Pallavi Sudhir]

I'm not sure how to interpret the results of #print notation. All I get is '⨆':1024 binders ',':0 (scoped 0) := #0 What's a binder?

[Kevin Buzzard]

oh oops

[Kevin Buzzard]

yes that is impossible to interpret

[Kevin Buzzard]

A binder is something like forall or exists or lambda I think

[Kevin Buzzard]

Kenny is using ⨆ in the same sort of way that one would use those things.

[Abhimanyu Pallavi Sudhir]

Yeah, I can tell it's something like forall, but I'm not sure what the difference is.

[Mario Carneiro]

I think you can click on the sup to go to definition

[Abhimanyu Pallavi Sudhir]

I get "no definition found"

[Mario Carneiro]

It's the analogue of \bigcup for lattices

[Kevin Buzzard]

It's in order/complete_lattice.lean

[Kevin Buzzard]

notation ⨆ binders , r:(scoped f, supr f) := r

[Kevin Buzzard]

I taught Abhi about bigcup today in lectures :-)

[Kevin Buzzard]

Glad to see my lectures are coming in handy in his day to day life

[Mario Carneiro]

"day to day life"

[Kevin Buzzard]

I don't understand that notation line at all. I think notation in Lean is somehow evil; most of it is fine and then there are some weird hacks which I don't get at all. The key point is supr somehow, and then everything else is some notation mantra I guess

[Kevin Buzzard]

def supr [complete_lattice α] (s : ι → α) : α := Sup {a : α | ∃i : ι, a = s i}

[Kevin Buzzard]

so supr s is the supremum of the range of s

[Abhimanyu Pallavi Sudhir]

Btw I'm trying def p1 (g : graph) : X := g.1 based on the earlier definition of graph, but it doesn't work:

invalid field notation, type is not of the form (C ...) where C is a constant
  g
has type
  ⁇

universe u
variable {X : Type u}
variable {Y : Type u}
variable {f : X → Y}
def graph : set (X × Y) := { g | g.2 = f g.1 }
def p1 (g : graph) : X := g.1

I guess part of the problem is that G is not a type -- I tried coercing it as ↑G, but that just produces more errors.

[Reid Barton]

I think the bigger problem is Lean doesn't know what you want to take the graph of

[Mario Carneiro]

I can't make sense of that definition

[Reid Barton]

I would make f an explicit argument and then pass it in p1

[Mario Carneiro]

what does g : graph mean?

[Mario Carneiro]

it's not a type

[Abhimanyu Pallavi Sudhir]

what does g : graph mean?

Yeah, I realise that, but I want to show (separately from the definition) it's a bijection from graph to X.

[Abhimanyu Pallavi Sudhir]

I would make f an explicit argument and then pass it in p1

Indeed that removes the first error. How, though?

[Mario Carneiro]

Keep in mind that graph fis not a type either, it's a set

[Mario Carneiro]

lean knows to coerce from a set to a type, but maybe you want the subtype instead?

[Kevin Buzzard]

a set is a term not a Type Abhi. Did you come to my lecture today?

[Abhimanyu Pallavi Sudhir]

a set is a term not a Type Abhi. Did you come to my lecture today?

I realise that -- but how else would I later show it to be a bijection from graph to X?

[Kevin Buzzard]

If X is a type and p : X -> Prop then in Lean there are two very different ways to express what in set theory is just "the subset of X consisting of elements a for which p a is true"

[Kenny Lau]

it did took me some time to figure out that Kevin wants us to prove that the two big big functions graph and graph' are equal

[Kenny Lau]

so you should start with ext X Y f

[Kevin Buzzard]

One is the set {x : X | p x} and one is the subtype {x : X // p x}

[Kevin Buzzard]

I am in the middle of showing my graph is Kenny's supr thing

[Kenny Lau]

I bet example : graph = graph' := isn't what Kevin wanted us to prove

[Kevin Buzzard]

I proved that using eq.comm

[Kenny Lau]

example : graph X Y f = graph' X Y f :=

[Kevin Buzzard]

import data.set.basic
import data.set.lattice

variables (X Y : Type) (f : X → Y)

def graph  : set (X × Y) := {z : X × Y | z.2 = f z.1}

def graph' : set (X × Y) := set.range (λ x, ⟨x,f x⟩)

def graph'' : set (X × Y) := ⨆ x : X, {(x, f x)}

example : graph = graph' := sorry

example : graph = graph'' := sorry

I did them both :-)

[Kevin Buzzard]

I am not proud of the second one though.

[Abhimanyu Pallavi Sudhir]

Re:the bijection, I can write def p1 (g : graph f) := g.1(still defining graph as a set because subtype gives me even more errors), but then p1 for some reason has the wrong type. Apparently g.1 isn't processed correctly (it still has type X × Y and not X).

[Mario Carneiro]

that has to do with the fact that it is a subtype

[Mario Carneiro]

g is a pair of an element of X x Y and a proof that this element satisfies z.2 = f z.1

[Abhimanyu Pallavi Sudhir]

Is the notation for ordered pairs different for subtypes?

[Mario Carneiro]

so the X value is g.1.1

[Abhimanyu Pallavi Sudhir]

That works, but I don't get why.

[Abhimanyu Pallavi Sudhir]

(deleted)

[Reid Barton]

or g.val.fst

[Abhimanyu Pallavi Sudhir]

Ok, I get the argument, but I'm not sure why it's defined that way (to include a proof).

[Reid Barton]

If you didn't have to provide a proof when constructing a value of the subtype, then it would just be the same as the entire original type.

[Abhimanyu Pallavi Sudhir]

Why does the same convention not apply to sets?

[Reid Barton]

I don't really understand the question. A set is not a type; perhaps that's the answer