Zulip Chat Archive

Stream: maths

Topic: Inverse image in `fin m` is a `finset`


view this post on Zulip Johan Commelin (May 16 2018 at 14:32):

The following code is (obviously) not typechecking. How do I make this work?

definition finvj {m n : } (f : fin m  fin n) (j : fin n) : finset (fin m) :=
begin
exact {i // f i = j}
end

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:38):

Well, I guess {i // f i = j} has type Type

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:39):

and you want something of type finset (fin m)

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:40):

so I guess you'd better find a way of constructing something of type finset (fin m)

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:40):

I don't know the first thing about finsets so I guess I start with #print finset

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:41):

oh and that doesn't look too good

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:41):

you seem to have to supply a multiset and a proof that this multiset has no duplicates

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:42):

but fortunately finset is in mathlib so there will probably exist a good interface

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:42):

which in this case will mean "other constructors"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:42):

so next I guess I'd have a look at finset.lean

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:43):

or maybe I could look for other constructors by typing finset. in VS code and then hitting ctrl-space a while

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:46):

oh -- finset.filter exists

view this post on Zulip Chris Hughes (May 16 2018 at 14:46):

univ.filter (\la i, f i = j)

I think you might need the finset namespace open.

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:47):

aah, here's a finset expert

view this post on Zulip Johan Commelin (May 16 2018 at 14:47):

Aah, cool.

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:47):

but I was seconds ahead of him ;-)

view this post on Zulip Johan Commelin (May 16 2018 at 14:47):

Yeah, congrats (-;

view this post on Zulip Johan Commelin (May 16 2018 at 14:47):

I'll look at filter!

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:47):

I was just showing you how I think about these things of course

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:48):

but actually in retrospect I missed a trick

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:48):

Instead of saying "I wonder what's there -- let's take a look at everything"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:48):

I should have said "let's assume everything is there -- what do I actually want?"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:49):

and what I want is (1) fin n is a finset and (2) a subset of a finset defined by a predicate being true is a finset

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:49):

and I should by now know that (2) is called filter

view this post on Zulip Johan Commelin (May 16 2018 at 14:49):

And I learned that today (-;

view this post on Zulip Johan Commelin (May 16 2018 at 14:49):

I did not yet find out (1)...

view this post on Zulip Johan Commelin (May 16 2018 at 14:50):

Chris's answer isn't working flawlessly here

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:50):

@Chris Hughes How does one prove fin n is a finset?

view this post on Zulip Johan Commelin (May 16 2018 at 14:50):

My search continues

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:50):

it'll be there somewhere

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:50):

hmm

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:50):

it's somehow not strictly speaking meaningful

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:51):

fin n is not a finset -- fin n and something of type finset are different things

view this post on Zulip Chris Hughes (May 16 2018 at 14:51):

fin n is not a finset. It is a fintype, and that should be automatically deduced as an instance

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:51):

right

view this post on Zulip Chris Hughes (May 16 2018 at 14:51):

sometimes (univ : finset (fin n)) helps

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:52):

Johan -- why do you want to use finset?

view this post on Zulip Chris Hughes (May 16 2018 at 14:52):

because otherwise it doesn't know the intended type. Also import data.fintype

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:53):

"set" doesn't mean what mathematicians think it means

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:53):

"set" in Lean means "subset of a set"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:53):

"subset of a given type"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:53):

rather than "arbitrary set of anything"

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:54):

This took me a while to get my head around

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:54):

"X : set N" doesn't mean "X is a proof that N is a set", it means "X is a subset of N". I sometimes read "set" as "subset_of".

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:56):

Because fin n is a type, and you have a predicate on that type, the natural thing to make is either a subtype or a set (fin m)

view this post on Zulip Johan Commelin (May 16 2018 at 14:56):

Kevin, I want to use finset, because I want to sum a function over it.

view this post on Zulip Johan Commelin (May 16 2018 at 14:56):

And finset's have all sorts of stuff for that

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:56):

My guess is that any type with a reasonable finiteness property will have sums

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:56):

with all sorts of stuff

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:57):

but on the other hand maybe finsets have the stuff you need

view this post on Zulip Johan Commelin (May 16 2018 at 14:57):

I couldn't find it for fin

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:57):

In which case I think Chris' answer sounds best. Why not do the dirty work with fintype (which presumably also has filter) and then turn it into a finset

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:59):

hmm I don't know what a fintype is either

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:59):

well, I just looked

view this post on Zulip Kevin Buzzard (May 16 2018 at 14:59):

I know nothing about these finite gadgets

view this post on Zulip Chris Hughes (May 16 2018 at 14:59):

It's only finsets that have sums.

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:00):

but there's a coercion from fintype to finset?

view this post on Zulip Chris Hughes (May 16 2018 at 15:00):

There is a function from fintype to finset. It's not a coercion.

view this post on Zulip Chris Hughes (May 16 2018 at 15:00):

It's called univ

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:00):

example (m : ℕ) : fintype (fin m) := by apply_instance

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:01):

that's a good start

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:01):

type class inference will tell you that (fin m) is a fintype

view this post on Zulip Johan Commelin (May 16 2018 at 15:01):

Yes, it's working now

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:01):

OK great

view this post on Zulip Johan Commelin (May 16 2018 at 15:01):

So now I can start mangling around with my sums

view this post on Zulip Johan Commelin (May 16 2018 at 15:02):

(-;

view this post on Zulip Kevin Buzzard (May 16 2018 at 15:02):

Now it's Patrick you want to talk to :-)

view this post on Zulip Johan Commelin (May 16 2018 at 15:02):

But first I need to catch a train

view this post on Zulip Johan Commelin (May 16 2018 at 15:02):

Yes, I am using big_ops

view this post on Zulip Patrick Massot (May 16 2018 at 15:06):

Actually I currently focused on non-commutative operations. That's why I can't work with finite sets. I'm summing (or multiplying or composing or whatever) elements of (ordered!) lists

view this post on Zulip Patrick Massot (May 16 2018 at 15:08):

That's why I can't use algebra.big_operators

view this post on Zulip Chris Hughes (May 16 2018 at 15:14):

@Johan Commelin algebra.big_operators is probably better than Patrick's big operators in this case.


Last updated: May 11 2021 at 16:22 UTC