Zulip Chat Archive

Stream: new members

Topic: finset ignorance


Patrick Lutz (Aug 19 2020 at 03:52):

I realized I don't understand how I am supposed to do the following with finsets. Suppose that I have a type X which I'd like to prove is finite. Suppose that I already have a proof of this which goes as follows: starting with some type Y and some subsets s and t of Y which I know are finite, I can construct a surjective map s × t → X. If I want to rewrite this proof to use some equivalent definition of s and t where they are finsets instead of just subsets of Y, how do I do that? When I try to write s × t → X, Lean complains to me about the type of s and t being finset Y rather than Type u.

Patrick Lutz (Aug 19 2020 at 03:52):

The situation where this came up is a little complicated so I have just tried to describe the source of my confusion. I can try to make a mwe if it would be helpful.

Mario Carneiro (Aug 19 2020 at 03:53):

is it possible to express the function as simply Y -> Y -> X?

Patrick Lutz (Aug 19 2020 at 03:54):

Sure

Patrick Lutz (Aug 19 2020 at 03:55):

But I get the same error when I do that

Patrick Lutz (Aug 19 2020 at 03:56):

I.e. when I write s → t → X, Lean tells me that it expected something of type Type u but got something of type finset Y instead

Mario Carneiro (Aug 19 2020 at 03:56):

so something like this?

example {X Y} (f : Y  Y  X) (s t : finset Y)
  (h :  z,  (x  s) (y  t), f x y = z) : fintype X := sorry

Patrick Lutz (Aug 19 2020 at 03:57):

Mario Carneiro said:

is it possible to express the function as simply Y -> Y -> X?

Oops, I misread this.

Patrick Lutz (Aug 19 2020 at 03:58):

It's probably possible to write it as Y -> Y -> X but it would be a bit annoying

Mario Carneiro (Aug 19 2020 at 03:58):

why? what's the real setting

Patrick Lutz (Aug 19 2020 at 03:58):

For instance I don't actually know whether X is nonempty

Mario Carneiro (Aug 19 2020 at 03:59):

Is X also a subset of a bigger type?

Patrick Lutz (Aug 19 2020 at 03:59):

Mario Carneiro said:

Is X also a subset of a bigger type?

Yeah

Patrick Lutz (Aug 19 2020 at 04:00):

This is not quite true, but it's basically the set of certain linear combinations of the roots of two polynomials

Mario Carneiro (Aug 19 2020 at 04:00):

is it a submodule or something like that?

Patrick Lutz (Aug 19 2020 at 04:00):

No

Patrick Lutz (Aug 19 2020 at 04:01):

Not all linear combinations, just a few of them

Patrick Lutz (Aug 19 2020 at 04:02):

Actually it's a little bit worse than that. I have two fields F and E and E is a field extension of F (expressed by saying E is an F-algebra) and X is the set of elements of F which can be written in a certain way as a linear combination of the roots of two polynomials over E

Patrick Lutz (Aug 19 2020 at 04:03):

and s and t are basically the roots of the polynomials

Patrick Lutz (Aug 19 2020 at 04:03):

The surjection is pretty easy to construct when I just define s and t directly as subsets of E. But I want to use polynomial.roots instead

Mario Carneiro (Aug 19 2020 at 04:04):

So like this then?

example {S Y} (s t : finset Y) (X : set S) (f : Y  Y  S)
  (h :  z  X,  (x  s) (y  t), f x y = z) : set.finite X := sorry

Mario Carneiro (Aug 19 2020 at 04:05):

I'm just trying to get a sense of what kind of hypothesis would be easiest for you to work with

Patrick Lutz (Aug 19 2020 at 04:10):

that's pretty close, but it's more like X is actually a subset of T and there's some injective map g : T -> S and the hypothesis is forall z \in X, \exists (x \in s) (y \in t), f x y = g z

Patrick Lutz (Aug 19 2020 at 04:10):

Mario Carneiro said:

So like this then?

example {S Y} (s t : finset Y) (X : set S) (f : Y  Y  S)
  (h :  z  X,  (x  s) (y  t), f x y = z) : set.finite X := sorry

I'd be happy to just know the best way to do this though

Mario Carneiro (Aug 19 2020 at 04:13):

I would express it as "the subset of the image of the product of finite sets is finite"

Mario Carneiro (Aug 19 2020 at 04:13):

and h is the proof that it's a subset

Mario Carneiro (Aug 19 2020 at 04:18):

example {S Y} (s t : finset Y) (X : set S) (f : Y  Y  S)
  (h :  z  X,  x y, (x  s  y  t)  f x y = z) : set.finite X :=
begin
  refine (set.finite.image (λ z:Y×Y, f z.1 z.2) (set.finite_mem_finset (s.product t))).subset _,
  simpa [set.subset_def] using h,
end

Kenny Lau (Aug 19 2020 at 06:52):

@Patrick Lutz it is an essential skill to be able to extract the essence of a lemma, i.e. remove all the noise about field extensions and state it as a lemma about sets and functions

Patrick Lutz (Aug 19 2020 at 06:52):

Kenny Lau said:

Patrick Lutz it is an essential skill to be able to extract the essence of a lemma, i.e. remove all the noise about field extensions and state it as a lemma about sets and functions

So I'm learning.

Kevin Buzzard (Aug 19 2020 at 08:56):

You can promote a finset to a set and then to a type if you want to take those products


Last updated: Dec 20 2023 at 11:08 UTC