## 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?

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?

#### 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?

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: May 13 2021 at 05:21 UTC