Compact locale 2026-10-14
A locale is compact when every directed family of opens whose join is contains . Equivalently every open cover has a finite subcover. The truth-valued test is a preframe homomorphism exactly when the locale is compact.
Connected locale 2026-10-14
Under classical logic a positive locale is connected when it cannot be written as the union of two disjoint nonzero opens. Equivalently its only complemented opens are and . An open sublocale uses this criterion relative to its own top element. Positivity of the whole locale excludes the empty locale. This definition is stated with its logical convention; replacing positivity by negated nonemptiness is not a constructive step.
Dense sublocale 2026-10-14
A sublocale is dense when its closure is the whole locale. For a map , its image is dense when implies . Classically, a dense point belongs to every nonzero open.
A locale is extremally disconnected when the closure of every open is open. Equivalently its regular open elements are complemented, or double negation preserves binary joins, or its Booleanization of a locale is a flat sublocale.
For a compact regular locale , put and . This locale is extremally disconnected. Its natural surjection to has inverse image
The Joyal extension lemma gives the frame homomorphism; its injectivity follows by recovering as the join of the regular opens in this ideal.
Hausdorff locale 2026-10-14
A locale is Hausdorff when its diagonal into its localic square is a closed sublocale. Its complement is the join of rectangles with . This is stronger than the underlying space being a Hausdorff space, because the localic square need not be spatial.
A geometric morphism is localic when is, over , the topos of sheaves on an internal locale of . Equivalently, subobjects of the objects , with , form a separating family in .
Nucleus on a frame 2026-10-14
A nucleus is an inflationary, idempotent, finite-meet-preserving map on a frame. Its fixed elements form a frame, whose joins are obtained by applying to ambient joins. The induced locale is a sublocale. The nuclei on a frame themselves form a frame in pointwise order; their meets are pointwise, but their joins usually are not.
Open locale 2026-10-14
An open, or overt, locale has a positivity map left adjoint to the scalar inverse image , satisfying Frobenius reciprocity. Thus and positivity preserves arbitrary joins. Classically every locale is overt, with positivity meaning .
A localic geometric morphism presents , over , as sheaves on an internal locale of . Equivalently, subobjects of inverse images form a separating family. A hyperconnected geometric morphism has a full faithful inverse image whose essential image is closed under subobjects. In particular, it induces bijections
For this definition, subobject-closed means every subobject of is isomorphic, over , to the inverse image of a subobject of .
Here is the construction and proof of the hyperconnected-localic factorization. Given , its right adjoint gives natural bijections
Let be the internal locale whose frame of opens is . The frame operations are determined by these bijections: intersections are intersections of represented subobjects; the join of a family is its image under the projection from the parameter-indexed family. For an internal index object , evaluation of the family over becomes a subobject of , and its direct image to represents the join. Pullback stability of images makes this natural in , and distributivity follows from the corresponding subobject identity in . This explicitly constructs the internal frame rather than asserting it from the existence of alone.
Set , with its localic projection to . We construct . A basic open family is a map ; its represented object in is the subobject corresponding to . Meets and covering joins of open families become intersections and jointly epic families of these subobjects.
An internal sheaf on is presented by its local sections with their open domains and restrictions. Pull these domains back to the corresponding and identify two sections wherever their restrictions agree. This is an effective equivalence relation in , so its quotient defines of the sheaf. More concretely, if is the object of sections and gives their domains, start with . For two sections, the join of the opens on which they agree gives an -valued relation on , hence a subobject of . Restricted to , this is the germ equivalence relation used for the quotient. The restriction and sheaf axioms guarantee reflexivity, symmetry and transitivity. This construction is functorial. Products and equalizers are obtained by meeting domains and equalizing restrictions, so it preserves finite limits. A right adjoint is obtained by taking, over each open family , the parameterized maps for . These maps satisfy the sheaf condition because a covering join gives an effective gluing of the ; their parameter objects are supplied by the original adjunction and exponentials. The map bijection on basic open families, followed by gluing, proves this is right adjoint to . Thus is a geometric morphism.
We must check hyperconnectedness, not just construct a factorization. A map has a graph which is a subobject of . The represented-subobject bijection turns it into an -valued relation on . Its totality and single-valuedness say exactly that this relation is a map between the corresponding basic sheaf objects: totality uses the covering join, and single-valuedness uses intersections and the diagonal of . Thus maps between basic open families are precisely their maps in . Applying this to the local sections of arbitrary sheaves, compatible maps glue uniquely on both sides. Hence is full and faithful. Likewise a subobject of pulls back to subobjects of its basic ; each is again represented by an open family, and their compatibility glues to a subsheaf of . The essential image is therefore subobject-closed, proving that is hyperconnected.
The inverse image is the constant family over the whole locale. The construction sends it to , so ; taking right adjoints gives the required factorization
This argument uses the usual effective quotient and local-section constructions in a topos; it also explains why the relevant internal opens are relative subobjects of , not just global subobjects of the terminal object.
For uniqueness, suppose with hyperconnected and localic. Then for every ,
If is sheaves on an internal locale , the right side is represented by its frame . These identifications preserve intersections, joins and parameter change, so the representing internal frames are isomorphic: . The locale and its sheaf topos are therefore equivalent over . Under this equivalence the basic open families have the same images in , and their local-section presentations determine all other images and maps. Thus the two hyperconnected parts agree up to the same equivalence. The factorization is unique up to equivalence.
Finally suppose with a geometric embedding and hyperconnected. Let be the local operator on presenting the inclusion. For a subobject of , take the -closure of in . Hyperconnectedness makes it the inverse image of a unique subobject of . This defines a closure operation on ; its extensivity, idempotence, intersection preservation and pullback stability descend from the -closure. Let be its local operator.
Hyperconnectedness also gives , by the represented-subobject bijections. The direct image is the closed-truth object , and hence
This follows either by taking the equalizer of and the identity or by representing closed subobjects in the preceding closure construction. The internal locale with frame is the sublocale of the terminal locale determined by : covering joins are exactly closure by . Its sheaves are the -sheaves in , and its projection is their geometric inclusion. Applying the just-proved factorization to therefore gives
This supplies the requested reordered factorization.
A preframe has finite meets and joins of nonempty directed sets, with finite meets distributing over these joins. A preframe homomorphism preserves both operations. Its preframe tensor product has generators and relations making a homomorphism separately in each variable. Equivalently,
In particular . The tensor unit is the free preframe on one generator: classically it is , and constructively it is the frame of truth values, with generator .
Regard a frame as a commutative monoid object in preframes, with multiplication and unit . Binary join preserves finite meets and directed joins separately. Conversely take a commutative monoid object in preframes and put
This set contains and , since preservation of the empty meet gives . If , then , and
Thus finite meets are inherited. If is nonempty and directed, separate preservation of directed joins gives
because a common upper bound gives . Directed joins are inherited too. Associativity and commutativity show that is idempotent; it is the least idempotent upper bound of . Therefore is the bottom and is binary join on . Arbitrary joins are directed joins of finite products, including the empty product . Finally
so binary distributivity, together with directed distributivity, proves that is a frame.
A homomorphism from a frame join monoid to sends every element to an idempotent above and therefore factors uniquely through . The factor preserves finite joins and directed joins, hence arbitrary joins. Conversely the inclusion preserves the preframe and monoid operations. Also a preframe monoid homomorphism between frames is automatically a frame homomorphism. This proves the full embedding and its right adjoint: is a coreflective subcategory of , with coreflector .
The coproduct of commutative monoid objects in a symmetric monoidal category is their tensor: the maps are , , and a pair induces . For two frames , the induced multiplication on pure generators is
Every pure generator is idempotent and above . Those properties are preserved by finite meets and directed joins, as just proved, so hold throughout the generated preframe. It is therefore already a frame, rather than requiring a further coreflection. Consequently
Rectangles in the localic product are instead .
For a filtered colimit in a category of frames, form the colimit in preframes, with stage maps . It can be presented by stage elements, all their finite-meet and directed-join relations, and the transition relations. Since tensoring is a left adjoint, it preserves colimits. Filteredness makes the diagonal diagram cofinal in the product index diagram, so the stage multiplications induce . The units agree. Each stage element is idempotent above the common unit; generation again implies . The resulting frame is the filtered colimit in a category in ; its binary join is induced by computing two representatives at a common later stage. Thus binary coproducts and filtered colimits of frames are computed in preframes, with the indicated induced join operation.
We now prove compactness. For a compact locale, its frame has a top test , , preserving finite meets and directed joins. For compact , tensor the tests and use the unit isomorphism to obtain a preframe map with
It reflects top on every pure generator. The property is closed under finite meets and directed joins: for a directed join, preservation of the join says that its truth value is the existential disjunction of the individual truth values, so some term has value . Since pure generators generate the preframe, reflects top everywhere. Applying to a directed cover of therefore shows that a term of that cover is . This proves compactness of the binary coproduct frame, hence of the binary product locale.
For a filtered diagram of compact frames, define on stage
These truth-valued maps preserve finite meets: witnesses can be taken to a common later stage, using filteredness. They preserve directed joins: compactness at the witnessing later stage selects a member of the directed family. They are compatible with transitions, again by filteredness, so induce a preframe map . On stage generators, implies . The same generation argument proves that reflects top throughout . Thus the filtered colimit frame is compact.
Finally the arbitrary coproduct of the frames is the filtered colimit of their finite coproducts, indexed by finite subsets of the index set; the empty finite coproduct is , itself compact. Finite coproducts are compact by the binary argument, and their filtered colimit is compact by the preceding paragraph. Opposing the categories gives
This proves the localic Tychonoff theorem through preframes, without choosing points or invoking the axiom of choice.
Use the order on locale maps in which means for every open . A Hausdorff locale has a closed diagonal in its localic square. A totally unordered locale, or locale, has discretely ordered hom-sets: every comparable pair of maps with any common domain is equal.
In the localic square of , let
This is the largest open disjoint from the diagonal: inverse image along the diagonal sends the rectangle to . Hence is the complement of its closure. If , then
for every summand of . Thus factors through the closure of the diagonal. For a Hausdorff locale that closure is the diagonal itself, so . This proof of Hausdorff implies does not require classical logic.
Here is an explicit classical counterexample to the converse implication from spatial Hausdorffness. Give the topology generated by the usual opens and by . Every open has the form , where are usual open sets and we may arrange . The topology is finer than the usual one, so the space is Hausdorff. Put , the complete Boolean algebra of ordinary regular open elements, and write . Restriction from this space to its rational and irrational subspaces, followed by Booleanization, gives frame homomorphisms
To justify these formulas, each subspace has its ordinary subspace topology and is dense in the ordinary real line. Regular-open algebras of a space and a dense subspace are isomorphic: restrict a regular open and take its interior-closure, with inverse obtained by taking interior-closure in the ambient space. Restriction is a frame homomorphism, and double negation is a frame homomorphism into its fixed-element frame. These observations also show independence of the chosen representation of . Since , we have , but and . Thus this Hausdorff space fails as a locale.
For the remaining arguments about connected locales, use the classical-logic option: positive opens of a locale are exactly the nonzero opens. There is a necessary positivity qualification. The empty locale has no positive opens, so the printed condition on those opens holds vacuously, although no point exists. The point assertions therefore require to be positive. This qualification is automatic if “totally connected” includes nonemptiness; otherwise it must be added explicitly.
Let be positive and satisfy the condition on its positive opens of a locale. Put . It contains , excludes , and is upward closed. If had , their union would be a positive open of a locale with a decomposition into two disjoint nonzero opens, contradicting its being a connected locale. Thus . If , not all can be zero; classical logic supplies a nonzero summand. Hence is a completely prime filter, and its characteristic frame homomorphism defines a point .
The point is dense. Indeed implies by the definition of . In nucleus language the image of has nucleus ; its value at is , so the image is a dense sublocale.
Conversely suppose an open locale has a dense point . Density means only if , and classically this implies for every positive open of a locale. If a positive open split as with and both summands nonzero, then , contradicting preservation of their meet. Thus every positive open of a locale is a connected locale, proving the converse under the declared logical convention.
Let be the terminal map. For a positive totally connected locale , the point above satisfies
because the right side is when and both sides are otherwise. Hence . If and is a totally unordered locale, composition gives , so . Therefore
which is the required constant factorization. For the empty source the factorization need not exist: the unique map does not factor through . Thus the positivity qualification matters for this assertion too.
For a Boolean algebra , write for its principal lattice ideal. The ideal frame of a Boolean algebra has intersections as meets and ideals generated by unions as joins. The pseudocomplement of an ideal is
In particular , so every principal ideal is complemented and regular.
If is complete, put . Then and . Thus all regular ideals are principal and complemented, so the corresponding locale is extremally disconnected.
Conversely, if the ideal frame of a Boolean algebra is extremally disconnected, each is complemented. Any complemented ideal is principal: if and , the fact that their generated join contains supplies with . Then , so ; every is disjoint from and therefore . Thus . Write . Since , bounds . If is another upper bound, implies , so . An arbitrary subset has the same upper bounds as the lattice ideal it generates, so every subset of has a supremum. Hence
Now put and . This is a complete Boolean algebra, with arbitrary Boolean joins , so the preceding result makes extremally disconnected. We construct its map to using the permitted Joyal extension lemma.
The map , , is a frame homomorphism, with right adjoint . Thus is a nucleus on a frame whose fixed frame is . It preserves finite joins: both and equal , and . Consequently the locale with frame is a flat sublocale of . It is also the Booleanization of a locale , so it has its inclusion map to .
The Joyal extension lemma says that a map from a flat sublocale to a compact locale that is a regular locale extends uniquely to the ambient locale. Apply it to this inclusion. Its frame formula gives
where is the well-inside relation . This also proves directly that the map is surjective. Indeed implies : meet with . Every member of the ideal is therefore at most in , since a finite Boolean join of its generators is below ; the last inequality follows because . Regularity gives
Thus can be recovered from , so is injective. A locale map with injective inverse-image frame homomorphism is a surjection. We have obtained an extremally disconnected and a surjection .
A propositional geometric theory has primitive propositions and sequents between formulas built with finite conjunction and arbitrary set-indexed disjunction. Start with the free frame on the primitives, identify conjunction with meet and disjunction with join, and impose each sequent as an inequality. The resulting quotient frame is . In the sheaf topos , interpret each primitive as the subterminal sheaf corresponding to its generating open. Operations on these subterminal sheaves are precisely the frame operations, so every imposed sequent is valid. This constructs the canonical model.
For a commutative ring , denote the generator attached to by . The presentation implies
The product equality uses the multiplication implication in one direction and both factor implications in the other; the latter follow by commuting . A ring homomorphism sends these relations to the corresponding ones in . It therefore gives a frame homomorphism and hence a map of locales.
If , then
so the two opens cover. Conversely let and pull back a putative cover along . Both generators become , so in . The allowed degeneracy criterion gives in , equivalently . Thus
This necessity argument never selects a prime ideal.
Finite intersections of the generating opens are again generators, so they form a basis. Assign to . The localization of a ring carries its ordinary addition and multiplication of fractions; equality of and means that some power of annihilates the cross-multiplied difference. On , restriction is further localization.
We also justify restriction for any inclusion of basic opens. Adding the condition to the presentation of gives the open and the presentation of : the generator for corresponds to . This is well-defined since equality of fractions, after multiplication by a power of the now-invertible , makes the two membership propositions equivalent. More explicitly, implies . If , this gives . If is killed by a power of , then (since ), and the additive inequalities for and give . A zero element in the localized ring has false membership, multiplication gives intersections, and the additive relation follows by clearing denominators. The reverse assignment on proves that these maps are inverse. Thus . If , then in this localized theory . Apply the quotient argument above, with the second generator , to conclude in . Therefore is invertible there, and the universal property of localization gives the restriction . These restrictions compose uniquely.
It remains to glue, and the allowed basis criterion reduces this to a whole-locale cover . Let and have equal restrictions to . Choose a common initial exponent , writing , . Equality on the overlap supplies with
Set , and . Then
with the last equality in itself. This clearing step is necessary when the commutative ring has zero divisors.
Since , also . Choose . For , expand ; each term contains either or , producing with . For choose . Define
In ,
and similarly in ,
Thus glues the matching pair. If is another gluing, some and annihilate . The same binomial argument gives , so . This proves uniqueness without cancellation or a domain assumption.
The exactness of the unit-ideal localization Čech complex proves the sheaf axiom for the required basic covers, and hence the assignment with its restrictions defines a sheaf of rings with . On the empty basic open, localization is the zero ring, whose underlying set has one section, as required. The construction and proof remain valid for the zero ring.