Properties on `fintype_inverse_systems`

Stream: maths

[Rémi Bottinelli]

Hey, so there is code here dealing with some properties of fintype_inverse_systems.
Mathlib has a lemma stating that such a system has a section, but I needed some finer-grained facts about it.

I'd like to have all these things in mathlibs, in some form or another. Could I get some guidance on whether and how I should proceed to get them merged? There is obviously a lot of golfing to be done, but beyond that, I'm not even sure how to correctly name things and where they would fit.

Thanks!

[Rémi Bottinelli]

I have a thoroughly cleaned-up (still far from perfect) version here and would still welcome some hints as to where to include this.
The obvious first guess would be in topology.category.Top.limits since that's where nonempty_sections_of_fintype_inverse_system is proved, but it's also obvious that it does not belong there…

[Adam Topaz]

What is the precise mathematical statement you need? There may be a way to deduce it from what's already in mathlib.

[Adam Topaz]

This assertion is in the topology folder because it comes from a general fact about cofiltered limits of compact Hausdorff spaces

[Rémi Bottinelli]

Well, this is meant to be used to talk about the ends of a simple graph.
Things I need:

• The sections are the same thing as sections of the "surjective" part (which translates to the ends being defined equivalently as the sections over connected components obtained by removing finsets, or infinite such components).
• Injectivity of the evaluation map of sections given some conditions on the system (so that I can put an upper bound on the number of ends)
• The sections can be decomposed, for any index i, as a sum of the sections having each possible value at index i (so that I can describe the ends of a graph as the sum of the ends of subgraphs).

[Rémi Bottinelli]

@Junyan Xu mentioned the Mittag-Leffner condition, and suggested that I generalize as much as possible to cofiltered systems.

[Rémi Bottinelli]

I feel like no matter whether or not the the lemmas I have can be obtained by more direct means, they would fit somewhere in mathlib.

[Junyan Xu]

Yeah I think the correct approach is probably to work with the Mittag-Leffler condition, and separately show that a directed inverse system of finite types automatically satisfies the condition.

[Junyan Xu]

The nonempty result, however, doesn't have much to do with the Mittag-Leffler condition; even if all objects are nonempty and all maps are surjective, the limit (section) could still be empty, see MO question and explicit example. If the directed set is countable, however, the limit is always nonempty (stacks#0597).

[Junyan Xu]

Both this SE answer and the nLab page say something about pro-objects and I wonder whether there's anything relevant done in LTE.

[Rémi Bottinelli]

Are "Mittag-Leffler" and "cofiltered system" essentially two incompatible way to generalize what I want? In case they are, which one should I try for?
Well, I'll just toy a bit with it all and see what can be proved.

[Rémi Bottinelli]

OK, I've got a PR here introducing Mittag-Leffler.
It has two lemmas that should go somewhere else, but otherwise I'm pretty happy with it (beside the fact that it's yet another mathlib3 PR ;) )