nLab locally connected locale

Definition

A locale $L$ is connected if $1\ne0$ and $1=A\cup B$ for disjoint opens $A$ and $B$ implies $A=0$ or $B=0$.

A locale $L$ is locally connected if its connected opens form a base (any open is a supremum of connected opens).

Properties

For a locally connected locale one can define its set of connected components.

See cosheaf of connected components for a parametrized version of this construction.

Related notions

• locally connected topos
• locally connected (∞,1)-topos?