Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

# Documentation

class (Prd a, Lattice (Rep a)) => Yoneda a where Source #

Yoneda representation for lattice ideals & filters.

A subset *I* of a lattice is an ideal if and only if it is a lower set
that is closed under finite joins, i.e., it is nonempty and for all
*x*, *y* in *I*, the element *x vee y* is also in *I*.

*upper* and *lower* commute with *Down*:

lower x y == upper (Down x) (Down y)

lower (Down x) (Down y) == upper x y

*Rep a* is upward-closed:

upper x s && x y == upper y s

upper x s && upper y s ==> connl filter x / connl filter y >~ s

*Rep a* is downward-closed:

lower x s && x >~ y ==> lower y s

lower x s && lower y s ==> connl ideal x / connl ideal y ~< s

Finally *filter >>> ideal* and *ideal >>> filter* are both connections
on *a* and *Rep a* respectively.

See also: