Zulip Chat Archive

Stream: Is there code for X?

Topic: A boolean algebra is an ordered comm monoid


view this post on Zulip Kenny Lau (Jun 14 2020 at 09:33):

Boolean algebra: https://github.com/leanprover-community/mathlib/blob/master/src/order/boolean_algebra.lean
Ordered comm monoid: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_group.lean

view this post on Zulip Kenny Lau (Jun 14 2020 at 09:34):

Currently a Boolean algebra is not a ring

view this post on Zulip Kenny Lau (Jun 14 2020 at 09:34):

what should we do about this?

view this post on Zulip Scott Morrison (Jun 14 2020 at 10:28):

Sorry, @Kenny Lau, could you be less telegraphic? I'm not sure what it is you're worried about.

view this post on Zulip Kenny Lau (Jun 14 2020 at 10:28):

sorry for not expressing myself clearly, I'm just wondering whether we should define a ring structure on a boolean algebra

view this post on Zulip Kenny Lau (Jun 14 2020 at 10:29):

and then prove that any Boolean algebra is an ordered comm monoid

view this post on Zulip Scott Morrison (Jun 14 2020 at 10:55):

as in http://math.mit.edu/~jerison/103/handouts/rings.pdf

view this post on Zulip Scott Morrison (Jun 14 2020 at 10:55):

I guess I don't know how useful it is to do this...?

view this post on Zulip Kenny Lau (Jun 14 2020 at 10:57):

well, ordered_comm_monoid was introduced 5 days ago in #2844 and I thought it would be useful to have some examples

view this post on Zulip Scott Morrison (Jun 14 2020 at 10:58):

I just worry that allowing people to use + to mean "symmetric difference of sets" is unlikely to lead to clarity. :-)

view this post on Zulip Scott Morrison (Jun 14 2020 at 10:59):

But I guess if it's done with def and not instance it's fine for constructing examples.

view this post on Zulip Bryan Gin-ge Chen (Jun 14 2020 at 15:20):

I think adding boolean rings is a fine idea. Maybe we could get Stone's representation theorem too.

view this post on Zulip Yury G. Kudryashov (Jun 14 2020 at 22:39):

Please don't add this as a ring instance on prop/set.

view this post on Zulip Aaron Anderson (Jun 30 2020 at 06:47):

There are also times where you do want to have an additive or multiplicative structure on a lattice, which might conflict with a boolean_ring instance

view this post on Zulip Aaron Anderson (Jun 30 2020 at 06:49):

I would be interested in working on an implementation of the Stone representation theorem though, just with a function that takes a boolean algebra lattice instance to a boolean ring ordered ring instance


Last updated: May 16 2021 at 05:21 UTC