Left and right separated Alexandrov topologies

A data kind distinguishing the chirality of a Kan extension.

A pointed open set in a separated left or right Alexandrov topology.

The base point of a pointed lower set (i.e. an Inf).

The base point of a pointed upper set (i.e. a Sup).

Map over a pointed open set in either topology.

Create an upper set: \( X_\geq(x) = \{ y \in X | y \geq x \} \)

Upper sets are the open sets of the left Alexandrov topology.

This function is monotone:

x <~ y <=> inf x <~ inf y

by the Yoneda lemma for preorders.

Check for membership in an Inf.

Filter an Inf with an anti-filter.

The resulting set is open in the separated left Alexandrov topology.

Intersecting with an incomparable element cuts out everything larger than its join with the base point:

>>> p = inf pi :: Inf Double
>>> p .? 1/0
True
>>> filterL (0/0) p .? 1/0
False

An example w/ the set inclusion lattice: >>> x = Set.fromList [6,40] :: Set.Set Word8 >>> y = Set.fromList [1,6,9] :: Set.Set Word8 >>> z = filterL y $ inf x fromList [6,40] ... fromList [1,6,9,40] >>> z .? Set.fromList [1,6,40] True >>> z .? Set.fromList [6,9,40] True >>> z .? Set.fromList [1,6,9,40] False

Create a lower set \( X_\leq(x) = \{ y \in X | y \leq x \} \)

Lower sets are the open sets of the right Alexandrov topology.

This function is antitone:

x <~ y <=> sup x >~ sup y

by the Yoneda lemma for preorders.

Check for membership in a Sup.

Filter a Sup with an anti-ideal.

The resulting set is open in the separated right Alexandrov topology.

>>> p = sup pi :: Sup Double
>>> -1/0 ?. p
True
>>> -1/0 ?. filterR (0/0) p
False