Zulip Chat Archive

Stream: new members

Topic: finset ignorance


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:53):

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

view this post on Zulip Patrick Lutz (Aug 19 2020 at 03:54):

Sure

view this post on Zulip Patrick Lutz (Aug 19 2020 at 03:55):

But I get the same error when I do that

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:58):

why? what's the real setting

view this post on Zulip Patrick Lutz (Aug 19 2020 at 03:58):

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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:59):

Is X also a subset of a bigger type?

view this post on Zulip Patrick Lutz (Aug 19 2020 at 03:59):

Mario Carneiro said:

Is X also a subset of a bigger type?

Yeah

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:00):

is it a submodule or something like that?

view this post on Zulip Patrick Lutz (Aug 19 2020 at 04:00):

No

view this post on Zulip Patrick Lutz (Aug 19 2020 at 04:01):

Not all linear combinations, just a few of them

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Aug 19 2020 at 04:03):

and s and t are basically the roots of the polynomials

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:13):

and h is the proof that it's a subset

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 13 2021 at 05:21 UTC