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

Stream: maths

[Johan Commelin]

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]

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

[Kevin Buzzard]

and you want something of type finset (fin m)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

oh and that doesn't look too good

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

which in this case will mean "other constructors"

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

oh -- finset.filter exists

[Chris Hughes]

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

I think you might need the finset namespace open.

[Kevin Buzzard]

aah, here's a finset expert

[Johan Commelin]

Aah, cool.

[Kevin Buzzard]

but I was seconds ahead of him ;-)

[Johan Commelin]

Yeah, congrats (-;

[Johan Commelin]

I'll look at filter!

[Kevin Buzzard]

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

[Kevin Buzzard]

but actually in retrospect I missed a trick

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

And I learned that today (-;

[Johan Commelin]

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

[Johan Commelin]

Chris's answer isn't working flawlessly here

[Kevin Buzzard]

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

[Johan Commelin]

My search continues

[Kevin Buzzard]

it'll be there somewhere

[Kevin Buzzard]

hmm

[Kevin Buzzard]

it's somehow not strictly speaking meaningful

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

right

[Chris Hughes]

sometimes (univ : finset (fin n)) helps

[Kevin Buzzard]

Johan -- why do you want to use finset?

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

"subset of a given type"

[Kevin Buzzard]

rather than "arbitrary set of anything"

[Kevin Buzzard]

This took me a while to get my head around

[Kevin Buzzard]

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

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]

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

[Johan Commelin]

And finset's have all sorts of stuff for that

[Kevin Buzzard]

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

[Kevin Buzzard]

with all sorts of stuff

[Kevin Buzzard]

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

[Johan Commelin]

I couldn't find it for fin

[Kevin Buzzard]

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]

hmm I don't know what a fintype is either

[Kevin Buzzard]

well, I just looked

[Kevin Buzzard]

I know nothing about these finite gadgets

[Chris Hughes]

It's only finsets that have sums.

[Kevin Buzzard]

but there's a coercion from fintype to finset?

[Chris Hughes]

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

[Chris Hughes]

It's called univ

[Kevin Buzzard]

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

[Kevin Buzzard]

that's a good start

[Kevin Buzzard]

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

[Johan Commelin]

Yes, it's working now

[Kevin Buzzard]

OK great

[Johan Commelin]

So now I can start mangling around with my sums

[Johan Commelin]

(-;

[Kevin Buzzard]

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

[Johan Commelin]

But first I need to catch a train

[Johan Commelin]

Yes, I am using big_ops

[Patrick Massot]

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]

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

[Chris Hughes]

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