nLab directed join

Directed joins

Directed joins

Idea

A directed join is simply a join of a directed set.

Definitions

More precisely, if PP is a poset and DD is a subset of PP, then we can consider the join D\bigvee D (if it exists) of DD in PP. Since DD is a poset in its own right, we can also consider whether DD is directed set. If so, then D\bigvee D (if it exists) is a directed join in PP. Sometimes one denotes that D\bigvee D is a directed join by making a little arrow out of the upper-right flank of the symbol (so it's a mix of ‘\bigvee’ and ‘\nearrow’). Unfortunately, I haven't found that symbol in LaTeX or Unicode. Possible workaround is D\bigvee{}^{\uparrow} D.

A codirected meet in PP is a directed join in P opP^\op, but people don't talk about those so much.

By default, we mean finitely directed sets, that is 0\aleph_0-directed. If instead we take the join of a κ\kappa-directed set (for some regular cardinal κ\kappa), then we have a κ\kappa-directed join.

Properties

If a join-semilattice (a poset with all finitary joins) has all directed joins, then it has all joins (and so is a suplattice, equivalently a complete lattice). More generally, if a poset has all joins of fewer than κ\kappa elements and all κ\kappa-directed joins, then it is a suplattice.

A topological space (or locale) XX is compact if and only if XX may be expressed as a directed join of open subsets only trivially. That is, whenever DD is a directed collection of opens, if X=DX = \bigcup D, then XDX \in D.

Directed colimits and filtered colimits are two slightly different categorifications of directed joins.

DCPOs

A poset which has all directed joins is called a directed-complete partial order, or dcpo. The homomorphisms of DCPOs are those functions that preserve directed joins; these are also called Scott-continuous because they are precisely the continuous maps relative to the Scott topology on the DCPOs.

A pointed dcpo is a DCPO with a bottom element (which is rather more specific than a pointed object in the category of DCPOs).

DCPOs are studied widely in domain theory.

Last revised on October 17, 2019 at 03:47:28. See the history of this page for a list of all contributions to it.