Zulip Chat Archive

Stream: general

Topic: frames


view this post on Zulip Johan Commelin (Oct 10 2018 at 18:26):

Are frames in mathlib? https://ncatlab.org/nlab/show/frame

view this post on Zulip Johan Commelin (Oct 10 2018 at 19:02):

I quote:

A frame O is a poset that has
all small coproducts, called joins ⋁
all finite limits, called meets ∧
and which satisfies the infinite distributive law:
x∧(⋁iyi)≤⋁i(x∧yi)
for all x,{yi}i in A
(Note that the converse holds in any case, so we have equality.)

view this post on Zulip Johan Commelin (Oct 10 2018 at 19:02):

Seems like we have all the ingredients.

view this post on Zulip Johan Commelin (Oct 10 2018 at 19:04):

Note that the notion dual to a frame is called a locale and these are the gadgets that people use to do topology without points. It seems that mathlib is also fond of doing topology without points, so maybe there is a general interest for these things.


Last updated: May 16 2021 at 05:21 UTC