Characterisation of connectedness using continuous maps

Stream: Is there code for X?

[Dagur Ásgeirsson]

Consider the following theorem:

Let X be a topological space and A a nonempty subset of X. Then A is connected if and only if every continuous map to a discrete space is constant on A.

Is it somewhere in mathlib? I couldn't find it in topology/connected.lean but maybe I'm overlooking something.

Anyway, if it's not in mathlib I would like to contribute my proof. My current version, which needs to be cleaned up quite a lot before I can contribute it to mathlib, can be found here: https://github.com/dagurtomas/nobelings-thm/blob/master/src/connected_characterisation.lean (as you can probably see I'm a Lean beginner).

The "only if" direction is only stated with a two-element target, but this should be easy to generalise to any discrete target.

Any help on how to get my code up to mathlib standards would be appreciated (and I'll also be happy if it's already somewhere in mathlib)!

[Johan Commelin]

I'm not aware of this being in mathlib.

[Adam Topaz]

We have a somewhat extensive API for the space of connected components. It would be great to integrate that result into that part of mathlib! See e.g. docs#connected_components

[Anatole Dedecker]

I’m actually surprised that we don’t have this, because this is one of the most efficient characterizations of connectedness. So it would be a really nice addition, and we could probably golf quite a few proofs using it 😜

[Dagur Ásgeirsson]

Thanks for the quick responses!

@Adam Topaz Do you mean that we should state the result as something like "the space of connected components is discrete"? I would be happy to contribute this mathlib. How does this work in practice?

[Adam Topaz]

we have docs#connected_components.totally_disconnected_space (which is the best you can hope for in general)

[Dagur Ásgeirsson]

Ah yes I see. This should imply the result

[Adam Topaz]

Anyway, I'll second what Johan and Anatole said -- we should definitely have that result in mathlib :)

[Anatole Dedecker]

Imo this characterization (or at least the two elements case) should not depend on connected components, I would really expect it to be one of the first lemmas we prove after the definition. But connected components are defined just a few hundred lines later IIRC so this is not really a big deal if it does depend on it

[Vincent Beffara]

Do we already have that a set is connected iff (relatively) clopen subsets are either empty or full ?

[Vincent Beffara]

Then, looking at preimages of singletons would bring most of the characterization in terms of maps to a discrete space

[Anatole Dedecker]

I can’t find that :scared:

[Vincent Beffara]

Yeah I couldn't find it either last time I looked, it would have helped for the uniqueness theorem. And it should be even closer to the definition than most other lemmas.

[Anatole Dedecker]

Yes. That looks like a great first project though, so we can probably leave that to Dagur if he wants!

[Vincent Beffara]

BTW Do we have API for relatively open, closed and clopen sets within a set? We likely have induced topology on a subtype but that will not be very enjoyable to use here

[Anatole Dedecker]

No we don’t. I’ve already thought about that, and the conclusion I came to was that if we don’t have a very good reason to do it, we probably shouldn’t spend too much time on duplicating all of this API. I’d say the most efficient way to talk about these currently is as set of the whole type whose preimage by coe is open/closed/clopen.

[Junyan Xu]

Note that Prop is the docs#sierpinski_space by default. If you use bool then you won't have to override the existing topological_space instance on Prop.
Interestingly in category theory we do define connectedness using functors to discrete categories: docs#category_theory.is_preconnected. I'm not sure why it doesn't just use a discrete category with two objects. Quantifying over a universe would better be avoided when possible IMO.

[Dagur Ásgeirsson]

Yes I noticed that! It will definitely be cleaner with bool if that has the discrete topology by default. Thanks for pointing that out.

[Junyan Xu]

docs#bool.topological_space define the topology to be the discrete topology ⊥. (I find this a bit unintuitive BTW that t₁ ≤ t₂ means t₂ ⊆ t₁; it's contrary to the usual notation

[Anatole Dedecker]

That’s because the usual notation is bad. What we want is that the identity is continuous from t1 to t2 iff t1 <= t2 (sorry, I’m on mobile). Moreover, the whole « filters generalize subsets » intuition forces this order on filter, and we wouldn’t want nhds to be order-reversing

[Patrick Massot]

Junyan Xu said:

I find this a bit unintuitive BTW that t₁ ≤ t₂ means t₂ ⊆ t₁; it's contrary to [the usual notation](https://en.wikipedia.org/wiki/Comparison_of_topologies#Definition.

No, it isn't. The usual notation is never t₁ ≤ t₂. Where do you see that on this wikipedia page? This page very clearly says that people can't decide what is the order relation and use both.

[Junyan Xu]

Where does the page say people can't decide? At least the lattice structure is contrary to what we have.

[Junyan Xu]

Are you referring to

There are some authors, especially analysts, who use the terms weak and strong with opposite meaning

[Junyan Xu]

I think the notation ⊆ should be pretty unambiguous. I recall some authors use ⪯ but I don't remember who and whether it's the finer-than or coarser-than relation.

[Dagur Ásgeirsson]

When I try to define the characteristic function of a set with values in bool, Lean complains that it doesn't find an instance of dedcidable x ∈ U. I can fix the problem by defining it as the composition of the Prop-valued characteristic function and the map Prop → bool. However, this requires a noncomputable in front, whereas everything I did before was computable according to Lean

[Kevin Buzzard]

So you are saying "I'm doing something noncomputable and I'm annoyed that I have to say it's noncomputable"? You can add the hypothesis [decidable_pred (∈ U)], or you can write noncomputable theory at the top of your file. Or you can use Prop instead of bool.

[Junyan Xu]

Note that we have docs#set.indicator and it's noncomputable (uses the classical decidable instance).

[Kevin Buzzard]

Note that most of mathlib does not care at all if something is noncomputable, we are not trying to make a constructive mathematics library, we're trying to make a classical mathematical library.

[Junyan Xu]

however bool doesn't have zero. If you use zmod 2 then you'd need to define the topology unfortunately...

[Junyan Xu]

Using if-then-else is short enough I guess; so maybe you can mimic src#set.indicator to define a noncomputable function to bool, or better, if you're only constructing the function within a proof, you can just use the classical tactic to get the desired decidable instance.

[Kevin Buzzard]

Probably fin 2 has a topology -- after all it has an addition, multiplication etc ;-) If it doesn't I'm sure nobody would mind if one were added! ;-)

[Anatole Dedecker]

Yes you should probably use fin 2 to be able to use docs#set.indicator, but we don’t have a topology on it

[Yaël Dillies]

Using bool or fin 2 will result in the same noncomputability issues, right?

[Anatole Dedecker]

Yes yes, we are talking about the ability to use docs#set.indicator

[Anatole Dedecker]

Tbh the fact that it’s computable if the codomain is Prop should really not be a decision factor, because you’ll lose it as soon as you want to escape from Prop anyway

[Yaël Dillies]

Yeah. I am just trying to understand what 2-points space you're looking for.

[Yaël Dillies]

Morally, unit ⊕ unit looks better because the topology you want of it is is the one coming from the order.

[Anatole Dedecker]

One with both has_zero and topological_space instances

[Anatole Dedecker]

And discrete_topology

[Yaël Dillies]

What do you need the zero for?

[Anatole Dedecker]

Which I believe doesn’t exist

[Anatole Dedecker]

To use docs#set.indicator

[Yaël Dillies]

What do you need set.indicator for? To avoid noncomputability issues scaring Dagur away?

[Yaël Dillies]

Can you not state the lemma for all [nontrivial α] [topological_space α] [discrete_topology α]?

[Anatole Dedecker]

No the set.indicator was because Dagur mentioned redefining the characteristic function of a set but valued in his two point space, whatever he chooses. But I agree it’s probably not worth making contorsions to use it, an inlined if-then-else will do

[Anatole Dedecker]

Sorry, I should probably stop answering from my phone and actually look at Dagur’s code before commenting, this would be more helpful

[Dagur Ásgeirsson]

I guess I was just confused that the computability of the result I'm proving depends on which discrete two-element space I choose. So what Kevin is saying is that if I use Prop, the result is still noncomputable but I just don't have to tell Lean (or Lean just won't know)?
I don't care either if something is noncomputable, by the way. I guess I'll just add noncomputable theory at the top.

[Junyan Xu]

I guess I was just confused that the computability of the result I'm proving depends on which discrete two-element space I choose. So what Kevin is saying is that if I use Prop, the result is still noncomputable but I just don't have to tell Lean (or Lean just won't know)?

The point is that set X is defined to be X → Prop and to convert a Prop to bool you need decidability of the proposition. In your mem_setProp, you invoke LEM (law of excluded middle) via by_cases. Without LEM you can't show Prop has exactly two elements and its powerset has four elements.

If you use set.indicator, you won't have to prove the mem_setProp lemma, and can directly use docs#set.indicator_const_preimage. Since we don't want to add a has_zero instance to bool, you may consider declare a has_zero instance within a proof, like letI : has_zero bool := ⟨ff⟩.

[Dagur Ásgeirsson]

Oh that's excellent! Thank you for this helpful answer. I'll try to use set.indicator then.

[Dagur Ásgeirsson]

I've completed the proof, with bool as the target and with any discrete target. See here: https://github.com/dagurtomas/nobelings-thm/blob/master/src/preconnected_characterisation.lean. I'm fairly happy with it but comments and suggestions are very welcome.

Should I post this in a different stream to get access to a branch of mathlib where I can submit a PR? My github username is dagurtomas

[Kevin Buzzard]

@maintainers

[Bryan Gin-ge Chen]

@Dagur Ásgeirsson Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Dagur Ásgeirsson]

Thanks! It's PR'ed, see #16974

[Junyan Xu]

Patrick Massot said:

Junyan Xu said:

I find this a bit unintuitive BTW that t₁ ≤ t₂ means t₂ ⊆ t₁; it's contrary to [the usual notation](https://en.wikipedia.org/wiki/Comparison_of_topologies#Definition.

No, it isn't. The usual notation is never t₁ ≤ t₂. Where do you see that on this wikipedia page? This page very clearly says that people can't decide what is the order relation and use both.

Let me note that mathlib has the (un-namespaced!) docs#tmp_order on topologies which is the subset order but not an instance. However, it's a local instance for a part of the file, so some lemma like docs#tmp_order gets the subset order instance rather than the default superset order, which can be confusing.

I'd advocate to adopt the subset order everywhere, as I think the reason for not doing so are not good enough, even though I agree with the order on filters. @Anatole Dedecker pointed out two monotonicities (like docs#le_of_nhds_le_nhds) that would become antitonic for the subset order, but it's not as strong a reason IMO as in the case of filters, where the viewpoint that filters are generalized subsets imposes the superset order.

[Jireh Loreaux]

issues with the fact that docs#tmp_order is un-namespaced aside, I disagree. I think reverse inclusion makes sense for exactly the reason Anatole mentioned before: t₁ ≤ t₂ is the order that makes the identity map from t₁ to t₂ continuous. So, this is the "covariant" way.

[Patrick Massot]

Lemmas that use that temporary order aren't meant to be used outside of a tiny fragment of that file. Where did you see a lemma that you wanted to use?

[Patrick Massot]

About the namespace, I guess the correct thing to do is to mark everything about that temporary order relation as private.

[Junyan Xu]

I use docs#generate_from_mono in #17133

[Junyan Xu]

I think reverse inclusion makes sense for exactly the reason Anatole mentioned before: t₁ ≤ t₂ is the order that makes the identity map from t₁ to t₂ continuous. So, this is the "covariant" way.

Why do we prefer src#is_open.mono being antitone over src#le_of_nhds_le_nhds being antitone?