nLab preuniform locale



The functor 𝒪:OLoc opFrm\mathcal{O}:OLoc^\op \to Frm from the opposite category of overt locales to the category of frames is a regular hyperdoctrine. This means that it has an internal logic, where given an overt locale LL, we can define the composition of open relations E,F𝒪(L×L)E, F \in \mathcal{O}(L \times L) as

FE{(x,z):L×L|y:L.(x,y)E(y,z)F}F \circ E \coloneqq \{(x, z):L \times L \vert \exists y:L.(x, y) \in E \wedge (y, z) \in F\}

A preuniform locale is a overt locale LL equipped with a filter \mathcal{E} on the frame of opens 𝒪(L×L)\mathcal{O}(L \times L) such that for each EE \in \mathcal{E},

  • (x,x)E(x, x) \in E

  • there exists an E oE^o \in \mathcal{E} such that (x,y)E(x, y) \in E entails and is entailed by (y,x)E o(y, x) \in E^o

  • there exists an FF \in \mathcal{E} such that FFEF \circ F \leq E

 See also


  • Graham Manuell, Uniform locales and their constructive aspects, (arXiv:2106.00678)

Created on November 16, 2022 at 21:29:00. See the history of this page for a list of all contributions to it.