Documentation

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:

• https://en.wikipedia.org/wiki/Filter_(mathematics)
• https://en.wikipedia.org/wiki/Ideal_(order_theory)