Question about induction(s)

Stream: maths

[Antoine Chambert-Loir]

Hi

I'd like to formalize a second lemma in topology.connected, namely that if you have a chain of connected topological spaces, each one meeting the next one, then the union is connected. This interacts with set theory machinery that I still don't understand to do in Lean, especially induction.

Here are my questions.
Bourbaki has only one such lemma, for a chain indexed by integers (ℕ), but it makes sense on finite chains as well, well ordered sets too, and also on other ordered sets which are not well ordered, such as ℤ.
And, in fact, for sets indexed by the vertices of a connected graph such that intersections of sets related by and edge are connected.

Both statements, chains indexed by well ordered sets and families indexed by vertices of a connected graph, are related, but they're not equivalent. Maybe both could be added.

Specific questions:
1) what type should one use for finite chains? fin n ?
2) where to look at examples of proof for finite induction, or well_founded induction?

Thanks

[Mario Carneiro]

Note that well ordered sets form a connected graph, because they are transitive so they have lots and lots of connections

[Johan Commelin]

Yes, but I think the condition on the topological spaces indexed by the graph is different from the condition for the well-ordered chains, if I understand @Antoine Chambert-Loir correctly.

[Mario Carneiro]

The connectedness graph condition can be stated as: for any nonempty disjoint sets A, B \sub G there exists R a b or R b a with a \in A and b \in B

[Mario Carneiro]

this is true for well ordered sets, or indeed any totally ordered set, since if A and B are nonempty with a : A and b : B, then a < b or b < a

[Mario Carneiro]

In this form, you don't need any induction to deduce the theorem, from connected graph relations to connected topological spaces

[Johan Commelin]

But I don't think mathlib has much about connected graphs. So I think going in that direction might require some work.

[Yaël Dillies]

It always boils down to the same thing... #8737

[Johan Commelin]

The version with chains might be a job for ordered indexing types, with a succ_order?

[Johan Commelin]

Is there some induction principle for succ_orders?

[Yaël Dillies]

mathlib has lots about conencted graphs on the wait.

[Yaël Dillies]

Johan Commelin said:

Is there some induction principle for succ_orders?

Nope, because you need some archimedean condition.

[Yaël Dillies]

I've thought about this already and I couldn't find any existing typeclass that would abstract this properly, so I might define succ_archimedean to mean that a < b implies b ≤ succ^[n] a for some n. And I might as well need to define pred_archimedean for the dual notion.

[Mario Carneiro]

Correct me if I'm wrong, but if we consider the long line as the vertices of a graph and connect vertices of distance less than 1, then we get a graph which is connected in my sense (no disconnection) but not connected in the sense of having a finite length path from any vertex to any other

[Antoine Chambert-Loir]

Regarding that PR #8737, I believe one should do general graphs (quivers, and orientations, etc.) rather than focusing straight away on simple graphs.

[Mario Carneiro]

the problem with generality in graph theory is that it completely changes the data structures

[Mario Carneiro]

which basically means that the specific theory is not a specialization of the general theory

[Yaël Dillies]

Welcome to stream#graph-theory, where everything needs to be done and hardly anything has been figured out :grinning_face_with_smiling_eyes:

[Sebastien Gouezel]

As a general rule of thumb, the right generality in mathlib is the one that suits the applications. So often a theorem is proved in the generality which is needed for the applications. And if later on it is needed in greater generality, then it will be extended at that time. This works pretty well, because refactoring theorems is not painful in general (one can state the very general version under a different name, then give a two-line proof of the original theorem based on the new general version, and all the applications don't need changing). And also it makes it possible to prove interesting theorems (otherwise, you get stuck on generalizing too much the basics, and you don't get anywhere). So, my advice would be to try to formalize your theorem indexed by $\mathbb{N}$ for now.

NB: the question of definitions is completely different, because refactoring definitions is much more painful. So those should be done in the right generality from the start. That's one of the reasons why formalizing definitions is much harder than formalizing theorems (and why we encourage newcomers to work on theorems first).

[David Wärn]

How about the following approach using relations instead of graphs. If you have a family of subspaces of X indexed by some type I, you get a relation on I saying "subspace i meets subspace j". The theorem says that if the quot by this relation has a unique element, then the union is connected.

[Reid Barton]

Right, and docs#eqv_gen is the inductive proposition you can induct on to prove it

[Johan Commelin]

I think that's a useful observation. But in some sense, it solves only half the problem. Because we still need to know that if you quot the naturals (or ℤ, or fin n) by the relation that relates n and n+1, that you get a type with a unique element.

[Yaël Dillies]

WHat do you think of succ_archimedean and pred_archimedean for that? I can get them PR-ready quickly.

[Kyle Miller]

Related to @David Wärn's approach, maybe you can set up the union as a colimit of topological spaces (as a functor from some indexing category to $\mathrm{Top}$) -- maybe there a general enough condition on when colimits are connected? (Finite) chains correspond to functors from the poset category ℕ or fin n (with a < b corresponding to a morphism a -> b). For the case of spaces indexed by a connected graph, you can consider functors from a category whose objects are the disjoint union of $V$ and $E$ and whose morphisms are $v\to e$ for $v\in V$ and $e\in E$ an incident edge.

This would be for topological spaces themselves. It sounds like you might want a version involving subspaces of some larger space.

[David Wärn]

It's true that a connected colimit (that is, where the index category is connected) of connected topological spaces is connected. This follows by considering the various images of inclusion maps, and applying the theorem about connected subspaces of an ambient space. But simply working with subspaces is surely easier

[David Wärn]

If you just want to prove the statement I sketched above, you don't really need eqv_gen or any form of induction, you just need quot.lift. The argument would go something like this: suppose X i are connected subspaces, and U is an open subset of their union. Since each X i is connected, either it's contained in U or it's disjoint from U. Whenever i is related to j, you get that X j is contained in U if X i is. So the function I -> Prop that says "X i is contained in U" factors through the quot. Hence if some X i is contained in U, then all of them are.

[Yaël Dillies]

#9714

[Yaël Dillies]

I will provide the instances for $\N$, $\Z$ and co in another PR.

[Johan Commelin]

Thanks, you got a bors d+ (-;

[Yaël Dillies]

And #9730, #9731 for you!