[Merged by Bors] - feat(topology/category/Top): nonempty inverse limit of compact Hausdorff spaces

[kmill]

The limit of an inverse system of nonempty compact Hausdorff spaces is nonempty, and this can be seen as a generalization of Kőnig's lemma. A future PR will address the weaker generalization that the limit of an inverse system of nonempty finite types is nonempty.

This result could be generalized more, to the inverse limit of nonempty compact T0 spaces where all the maps are closed, but I think it involves an essentially different method.

---

[kmill]

For reference, this is roughly what the next PR would be:

universes u
variables {J : Type u} [directed_order J]
variables (F : Jᵒᵖ ⥤ Type u)

theorem konig [hf : Π (j : Jᵒᵖ), fintype (F.obj j)] [hne : Π (j : Jᵒᵖ), nonempty (F.obj j)] :
  F.sections.nonempty :=
begin
  let F' : Jᵒᵖ ⥤ Top := F ⋙ Top.discrete,
  haveI : Π (j : Jᵒᵖ), fintype (F'.obj j) := hf,
  haveI : Π (j : Jᵒᵖ), nonempty (F'.obj j) := hne,
  obtain ⟨⟨u, hu⟩⟩ := nonempty_limit_cone_of_compact_t2_inverse_system F',
  exact ⟨u, λ j j' f, hu f⟩,
end

[semorrison]

These cumbersome steps (the erw, and the by dec_trivial) are only necessary because we're missing some lemmas about hom_of_le and le_of_hom, and about iff_true_intro.

I've taken the liberty of pushing a commit with these additional lemmas, because they belong in two different files.

[semorrison]

Suggested change

	haveI := classical.dec_pred (λ (j' : Jᵒᵖ), j'.unop ≤ j.unop),
	classical,

?

[kmill]

In some earlier version classical was bringing in some conflicting instances so I pulled in the bare minimum, but it works fine now.

[semorrison]

Looks great!

bors d+

[bors]

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[kmill]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[b-mehta]

This looks amazing Kyle, exactly what I had in mind, thanks for working on this! Do you know if the result still holds if we generalise it to filtered colimits (rather than just directed colimits)? Since directed colimits are just a special case of filtered colimits it would great to have a more general version if it's true

[kmill]

@b-mehta If you mean filtered inverse limits, then I think this nonemptiness result should generalize (and it might not need the "equalizer" axiom of the cofiltered category -- I can't see where it would be used in the argument.)

For filtered colimits, aren't they nonempty if any of the spaces in the system are nonempty?

By the way, in Stacks tag 002Z, they have an argument for nonemptiness of inverse limits of nonempty finite sets (similar to the one used in the referenced Stone paper). They put a partial ordering on inverse systems of closed subsets and use Zorn's lemma to find a minimal one. Topologically, compactness gives nonemptiness of a minimal system, and Hausdorff gives that in a minimal system each set is a singleton, so you get a section. I think the idea with the T0 generalization is that if you have closed maps then if a given set in a minimal system weren't a singleton, you could find a closed point and reduce the system, since the image of a closed point through a closed map is a closed point. Maybe it would be nice to (eventually) redo everything in terms of this ordering on inverse systems.