fintype

Stream: Berkeley Lean Seminar

[Kyle Miller]

For a project I'm working on, the last thing to prove is the following, which seems like it should be easy enough, but I've been having a hard time finishing it off:

instance list_sep_fintype {A} [fintype A] (n : ℕ) (p : list A → Prop)
: fintype {x : list A | x.length = n ∧ p x}

The best strategy I can think of is to show this set is equivalent to filtering the type of length-n vectors by p, since I think I can show that's a fintype.

[Thomas Browning]

if I'm understanding things correctly, isn't this true without the "∧ p x" ?

[Kevin Buzzard]

fintype is hard to work with because it's data. Ask this on the main chat if you want an expert opinion. If it's not in the library it might be tricky to get it there. I agree that the filter approach should work.

[Kevin Buzzard]

Thomas Browning said:

if I'm understanding things correctly, isn't this true without the "∧ p x" ?

Sure, but you'll still have to locate the proof that a subthing of a finite thing is finite. Finiteness is a nightmare if you have to prove things yourself because it's been made in a computable manner.

[Kyle Miller]

Thomas Browning said:

if I'm understanding things correctly, isn't this true without the "∧ p x" ?

Yeah, that's true, and it just happens to be the fintype instance I need in the end. (There's already basically an instance of fintype {x : list A | x.length = n}, but for vectors.)

[Kyle Miller]

The approach of constructing an equivalence with vector types worked out, though I had to add noncomputable to my instance for some reason.

So, I submit my first project, a proof of the countable version of the De Bruijn–Erdős theorem, that if a graph with countably many vertices has the property that every finite subgraph can be n-colored, then the graph can be n-colored. This involved proving a weak version of Kőnig's lemma, that the inverse limit of an ℕ-indexed family of finite sets is nonempty.

Coloring statement: https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean#L347

Kőnig's lemma: https://github.com/kmill/lean-graphcoloring/blob/master/src/konig.lean#L153

The proofs are terrible, but, hey, it's proved. (While any hints to clean things up would be appreciated, I don't want to harm any of your eyes with its very hacky state.)

(I plan on cleaning some things up and eventually submitting PRs for some of the lemmas, since some seem to be useful.)

[Patrick Lutz]

probably worth mentioning this on the maths stream

[Kyle Miller]

By the way, some math commentary: I'm not sure how Konig's lemma is usually proved, but here's what I did. Suppose your inverse system consists of nonempty finite sets $S_n$ and functions $f_n:S_{n+1}\to S_n$, for all $n\in\mathbb{N}$. Each element $x\in S_n$ might or might not be extendable, in the sense that it might or might not be in the image of $f_n$. Call an element $k$-extendable if it comes from an element in $S_{n+k}$, in the sense that it is the iterated image of such an element, and call an element very extendable if it is $k$-extendable for all $k$. It turns out finiteness implies every $S_n$ has at least one very extendable element, and furthermore the restriction to the very extendable elements yields a new inverse system where every function is surjective. From here, you can use choice to construct an element of the inverse limit.

(This might be interesting for counting the numbers of n-colorings for certain families of graphs. You might be able to get exponential lower bounds by considering only the very extendable colorings. That is, by looking at colorings of the inverse limit of the family of graphs and how they restrict.)

[Patrick Lutz]

What you describe is more or less the standard way to prove Konig's lemma: always stay in the infinite part of the tree.

[Kyle Miller]

A fancy way to prove it is to take the product $X$ of the $S_n$ sets. Giving these sets the discrete topology, $X$ with the product topology is compact (the Tychonoff theorem). Letting $C_n\subseteq X$ denote the set of sequences such that indices $0,1,\dots,n$ satisfy the inverse system's constraint, then one may show these are closed and nonempty. This family $\{C_n\}_n$ has the finite intersection property, so the intersection is nonempty due to the compactness of $X$. (This idea extends to inverse systems in the category of topological spaces where the $S_n$ sets are nonempty and compact, rather than nonempty and finite.)