finset ignorance

Stream: new members

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

Sure

[Patrick Lutz]

But I get the same error when I do that

[Patrick Lutz]

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]

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]

Mario Carneiro said:

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

Oops, I misread this.

[Patrick Lutz]

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

[Mario Carneiro]

why? what's the real setting

[Patrick Lutz]

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

[Mario Carneiro]

Is X also a subset of a bigger type?

[Patrick Lutz]

Mario Carneiro said:

Is X also a subset of a bigger type?

Yeah

[Patrick Lutz]

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

[Mario Carneiro]

is it a submodule or something like that?

[Patrick Lutz]

No

[Patrick Lutz]

Not all linear combinations, just a few of them

[Patrick Lutz]

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]

and s and t are basically the roots of the polynomials

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

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]

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]

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

[Mario Carneiro]

and h is the proof that it's a subset

[Mario Carneiro]

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]

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

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]

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