Lebesgue covering dimension for locales

Question

A space $(X,\tau)$ is said to have Lebesgue covering dimension $\leq n$ (for some $n\in\mathbb{N}$) if every open covering $\cal U$ has a refinement $\cal V$ such that for every $x\in X$ the set ${\cal V}_x := \{V\in \mathcal{V}: x\in V\}$ has at less than $n$ elements. (Note that $n$ is "globally fixed" for all open coverings $\cal U$.) If there is no $n\in\mathbb{N}$ such that $(X,\tau)$ has Lebesgue dimension $\leq n$ then $(X,\tau)$ is said to have infinite Lebesgue dimension.

Now, points are crucially involved in this definition (I am referring to the sets $\mathcal{V}_x$).

Can the definition of the Lebesgue covering dimension for topological spaces be extended to locales?

Answer 1

It is easy to see that a space $X$ has Lebesgue covering dimension less than or equal to $n$ if and only if whenever $\mathcal{U}$ is an open covering, there is some refinement $\mathcal{V}$ so that whenever $O_{0},...,O_{n+1}\in\mathcal{V}$ are distinct we have $O_{0}\cap...\cap O_{n+1}=\emptyset$. This notion can be extended to locales in the obvious way. In particular, we say that a frame $L$ has Lebesgue covering dimension at most $n$ if whenever $C\subseteq L$ and $\bigvee C=1$, there is some $D\subseteq L$ with $\bigvee D=1$, for all $d\in D$ there is some $c\in C$ with $d\leq c$, and where if $x_{0},...,x_{n+1}\in D$ are distinct, then $x_{0}\wedge...\wedge x_{n+1}=0$. I am not aware if the point-free version of the Lebesgue covering dimension has been studied already, but point-free topology has not been well developed, so it seems like someone would study the point-free Lebesgue covering dimension in the future.