Boolean algebras and sets

Stream: general

[Yaël Dillies]

There is tension in the import tree between file#order/boolean_algebra, file#order/hom/basic and file#data/set/basic, because each wants to import the next:

• docs#compl is an order isomorphism to the order dual (docs#order_iso.compl), and this provides many lemmas. For example, docs#compl_antitone
• We bundle set equivalences as order isos. For example, docs#order_iso.set.univ
• docs#set is a docs#boolean_algebra

At the moment, it works somehow, but any tweak (#14809 or branch#heyting_algebra) makes the tower of cards collapse.

[Yaël Dillies]

/poll What should we do?

• Move the set equivalences to data.set.basic
• Split a new file order.hom.set off order.hom.basic for the set equivalences
• Split a new file data.set.order off data.set.basic for the order properties
• Keep adding the lemmas derived from order_iso.compl to order.hom.basic
• Pray for content-addressing

[Yaël Dillies]

I would like to emphasize that these options are not mutually exclusive. I think 1 and 3 would make a great combo, by greatly reducing import stress and shrinking data.set.basic (which is one of mathlib's biggest files).

[Yaël Dillies]

cc @Peter Nelson because this will very soon block your matroid work (I was rewriting your branch in the style of your first PR and I hit this)

[Peter Nelson]

I like 1 and 3 as well. Thanks for all the thought you’ve given to this!

[Floris van Doorn]

What does 3 even mean? I don't think lemmas about ⊆ like docs#set.subset_union_left should go outside data.set.basic?

[Floris van Doorn]

I think we could go even further than 2, and move order_iso out of order.hom.basic to order.hom.equiv or something.

[Floris van Doorn]

(oh, but I guess that doesn't solve this particular problem)

[Yaël Dillies]

It would be moving the material about complements, which is what requires order.boolean_algebra in data.set.basic. But I agree that not moving the other order instances is somewhat dissatisfactory.

[Yaël Dillies]

I am now trying to implement 2 and I can't keep thinking that it would be easier to move docs#set.range, docs#set.image to move to a new file data.set.defs.

[Yaël Dillies]

The order files use set for its basic constructions, not for its order structure, but data.set.basic is a mix of it all.

[Yaël Dillies]

For reference, implementing 1 or 2 means moving stuff from file#logic/embedding, docs#order/rel_iso, docs#order/hom/basic to either one (or three?) new file(s) or dumping it into docs#data/set/basic.

[Floris van Doorn]

I'm definitely also happy with data.set.defs. I'm a bit surprised that all those files use constructions on sets, but no basic lemmas.

[Floris van Doorn]

I see e.g. function.injective.image_injective in file#logic/embedding. That should definitely not go in data.set.defs.

[Yaël Dillies]

If the name defs is putting you off, this brings me back to proposition 3.

[Floris van Doorn]

I think it would be good to keep the boolean_algebra instance in data.set.basic. I think it would be confusing if all binary set operations are defined in data.set.basic, but the complement is in another file.
I think it's good to follow the example of equiv, which also has file#logic/equiv/set separately. So we can separate embedding/rel_iso/order_hom interactions with set to separate files (i.e. option 2). If you don't want to create 3 new files, maybe you can do with moving embedding stuff into data.set.function (if that doesn't create issues) and have a single new file order.hom.set.

[Yaël Dillies]

But what if I also move the binary set operations to the new file data.set.order?

[Kevin Buzzard]

Apparently it's file#logic/equiv/set now BTW

[Floris van Doorn]

Thanks, fixed

[Floris van Doorn]

But if it makes your life a lot easier, I can live with a file data.set.compl where you move compl and diff. I think it would make the findability of some lemmas harder (e.g. docs#set.image_compl_eq for a random example), so I would prefer a different solution.