topology on `Prop`

Stream: mathlib4

[Aaron Liu]

Why is docs#sierpinskiSpace the default topological space on Prop? This makes the topology on Prop different from the topology on Bool. This just seems to me like a bad idea.

In Prop, {True} is open and {False} is closed. univ and ∅ are clopen.
In Bool, all sets are clopen.

[Aaron Liu]

docs#continuous_empty_function right next to it is weird too. It assumes the codomain is empty, when the same result holds assuming the domain is empty.

[Kyle Miller]

The sierpinski topology is the one where the continuous sets (as indicator functions) are the open sets.

[Kyle Miller]

I think the topology on Bool is instead the one that makes its recursor continuous (at least the non-dependent one).

[Kevin Buzzard]

Is there any part of the library which is using either of these topologies?

[Kyle Miller]

I can't remember the use of it, but docs#TopologicalSpace.productOfMemOpens_isEmbedding is kind of neat. Each T0 space X embeds into Opens X -> Prop, where, thinking of Opens X -> Prop as Set (Opens X), the embedding sends each point to its open neighborhood filter.

[Kyle Miller]

(It would be nice if there were a way to query for all direct uses of the topology on Prop.)

[Johan Commelin]

The Sierpinski topology is also the correct one from the point of view of the Alexandrov topology associated with the preorder on Prop

[Kevin Buzzard]

Perhaps the difference between Prop and Bool is that -> has type Prop -> Prop -> Prop but there seems to be no booly analogue of this, and this gives an asymmetry in Prop which is not so well reflected in the Bool world.

[Trebor Huang]

Maybe it's counterintuitive and I have never seen it used in programming, but we do have a Boolean analogue, both in Lean and general programming languages. It's just spelled like ≤ (decidable and coerced to Bool in Lean). A similar counterintuitive operator is Xnor, which is spelled like==...

[Kevin Buzzard]

<= on Bool is Prop-valued, so you also need to apply the coercion, which is what made me claim that the Bool analogue didn't really exist.

[Aaron Anderson]

The Sierpinski topology is useful on occasion, but I can't help but think the best setup would be to have both topologies available, and only used as instances locally. The other (discrete) topology would make it very easy to talk about several of the constructions in Stone duality, for instance.

[Johan Commelin]

But couldn't we use the "type alias" Bool for the latter application?

[Filippo A. E. Nuccio]

Pinning @Sam van G who might have an opinion!

[Sam van G]

Hi! I am not quite sure what the question is, but as some of the messages
above also indicate, the Sierpinski topology on the two element set classifies
open sets while the discrete topology classifies clopen sets. In Stone
duality, Sierpinski can be used as the dualizing object for obtaining a dual
adjunction between frames and topological spaces, while discrete gives a dual
equivalence between Boolean algebras and Boolean spaces (= profinite sets). So
yes, both topologies on the two element set are sometimes useful.