Stream: maths

Topic: Inverse image in fin m is a finset

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


Kevin Buzzard (May 16 2018 at 14:38):

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

Kevin Buzzard (May 16 2018 at 14:39):

and you want something of type finset (fin m)

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)

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

Kevin Buzzard (May 16 2018 at 14:41):

oh and that doesn't look too good

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

Kevin Buzzard (May 16 2018 at 14:42):

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

Kevin Buzzard (May 16 2018 at 14:42):

which in this case will mean "other constructors"

Kevin Buzzard (May 16 2018 at 14:42):

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

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

Kevin Buzzard (May 16 2018 at 14:46):

oh -- finset.filter exists

Chris Hughes (May 16 2018 at 14:46):

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

I think you might need the finset namespace open.

Kevin Buzzard (May 16 2018 at 14:47):

aah, here's a finset expert

Aah, cool.

Kevin Buzzard (May 16 2018 at 14:47):

but I was seconds ahead of him ;-)

Johan Commelin (May 16 2018 at 14:47):

Yeah, congrats (-;

Johan Commelin (May 16 2018 at 14:47):

I'll look at filter!

Kevin Buzzard (May 16 2018 at 14:47):

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

Kevin Buzzard (May 16 2018 at 14:48):

but actually in retrospect I missed a trick

Kevin Buzzard (May 16 2018 at 14:48):

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

Kevin Buzzard (May 16 2018 at 14:48):

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

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

Kevin Buzzard (May 16 2018 at 14:49):

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

Johan Commelin (May 16 2018 at 14:49):

And I learned that today (-;

Johan Commelin (May 16 2018 at 14:49):

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

Johan Commelin (May 16 2018 at 14:50):

Chris's answer isn't working flawlessly here

Kevin Buzzard (May 16 2018 at 14:50):

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

Johan Commelin (May 16 2018 at 14:50):

My search continues

Kevin Buzzard (May 16 2018 at 14:50):

it'll be there somewhere

hmm

Kevin Buzzard (May 16 2018 at 14:50):

it's somehow not strictly speaking meaningful

Kevin Buzzard (May 16 2018 at 14:51):

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

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

right

Chris Hughes (May 16 2018 at 14:51):

sometimes (univ : finset (fin n)) helps

Kevin Buzzard (May 16 2018 at 14:52):

Johan -- why do you want to use finset?

Chris Hughes (May 16 2018 at 14:52):

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

Kevin Buzzard (May 16 2018 at 14:53):

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

Kevin Buzzard (May 16 2018 at 14:53):

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

Kevin Buzzard (May 16 2018 at 14:53):

"subset of a given type"

Kevin Buzzard (May 16 2018 at 14:53):

rather than "arbitrary set of anything"

Kevin Buzzard (May 16 2018 at 14:54):

This took me a while to get my head around

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".

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)

Johan Commelin (May 16 2018 at 14:56):

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

Johan Commelin (May 16 2018 at 14:56):

And finset's have all sorts of stuff for that

Kevin Buzzard (May 16 2018 at 14:56):

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

Kevin Buzzard (May 16 2018 at 14:56):

with all sorts of stuff

Kevin Buzzard (May 16 2018 at 14:57):

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

Johan Commelin (May 16 2018 at 14:57):

I couldn't find it for fin

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

Kevin Buzzard (May 16 2018 at 14:59):

hmm I don't know what a fintype is either

Kevin Buzzard (May 16 2018 at 14:59):

well, I just looked

Chris Hughes (May 16 2018 at 14:59):

It's only finsets that have sums.

Kevin Buzzard (May 16 2018 at 15:00):

but there's a coercion from fintype to finset?

Chris Hughes (May 16 2018 at 15:00):

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

It's called univ

Kevin Buzzard (May 16 2018 at 15:00):

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

Kevin Buzzard (May 16 2018 at 15:01):

that's a good start

Kevin Buzzard (May 16 2018 at 15:01):

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

Johan Commelin (May 16 2018 at 15:01):

Yes, it's working now

OK great

Johan Commelin (May 16 2018 at 15:01):

So now I can start mangling around with my sums

(-;

Kevin Buzzard (May 16 2018 at 15:02):

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

Johan Commelin (May 16 2018 at 15:02):

But first I need to catch a train

Johan Commelin (May 16 2018 at 15:02):

Yes, I am using big_ops

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

Patrick Massot (May 16 2018 at 15:08):

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

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