Zulip Chat Archive

Stream: Is there code for X?

Topic: completion of boolean algebra

Kenny Lau (Dec 13 2020 at 07:51):

The completion of a docs#boolean_algebra is an embedding to a docs#complete_boolean_algebra with dense image. Do we have it in mathlib?

Adam Topaz (Dec 13 2020 at 14:22):

I would be surprised. Last time I checked I didn't even find morphisms of boolean algebras in mathlib

Adam Topaz (Dec 13 2020 at 14:24):

Flypitch might have something. Doesn't this come up in forcing?

Jesse Michael Han (Dec 13 2020 at 15:59):

we end up showing certain forcing posets are dense in certain boolean algebras but there's not a substantial API around the notion of completion/dense embedding

Last updated: Dec 20 2023 at 11:08 UTC