User:Leigh.Samphier/Topology/Definition:Locale (Lattice Theory)

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\mathbf{Loc}$ denote the category of locales.

An object of $\mathbf{Loc}$ is called a locale.


That is, a locale is a complete lattice $\struct {L, \preceq}$ satisfying the infinite join distributive law:

  \(\ds \forall a \in L, S \subseteq L:\) \(\ds a \wedge \bigvee S = \bigvee \set {a \wedge s : S \in S} \)      

where $\bigvee S$ denotes the supremum $\sup S$.


Frames vs Locales vs Complete Heyting Algebras

If we are only concerned with category theoretic objects, the terms frame and locale and complete Heyting algebra are synonymous. (See Characterization of Locale)


It is only when we consider the associated morphisms that they become different:


Also see


Sources