Are CompleteDistribLattices completely distributive?

Stream: maths

[Gabriel Ebner]

The docstring says that a CompleteDistribLattice is a completely distributive lattice, which according to wikipedia means the following:

theorem iInf_iSup_eq {β : α → Sort v} [CompleteDistribLattice γ] {f : ∀ a _, γ} :
    (⨅ a, ⨆ b, f a b) = ⨆ g : ∀ a, β a, ⨅ a, f a (g a) :=
  sorry

Is that true though? This doesn't seem to (easily) follow from the axioms, which essentially only postulate the equality above if either α or β are finite.

[Junyan Xu]

Yeah I think counterexamples are given in this question.

[Damiano Testa]

This looks like it would be a great addition to counterexamples!

[Damiano Testa]

Or/and Counterexamples!

[Yaël Dillies]

Isn't it said in the docstring of docs#complete_distrib_lattice that it's complete distributive lattice, not a completely distributive complete lattice?

[Johan Commelin]

Nope, the ly is present in the docstring.

[Johan Commelin]

It's probably a typo.

[Yaël Dillies]

Hmm, indeed. And Wikipedia supports Gabriel's interpretation

[Yaël Dillies]

All current instances can be strengthened to this new definition, except maybe docs#complete_boolean_algebra.to_complete_distrib_lattice which I would have to think about. We current have surprisingly less instances than I thought (half of the instances I added very recently as well).

[Yaël Dillies]

(Boolean algebras embody LEM and completely distributive lattices embody choice, so a priori the instance can't be strengthened, but maybe making complete the boolean algebra suddenly increases its "axiomatic strength"?)

[Gabriel Ebner]

@Junyan Xu Thanks for the counterexample!

[Gabriel Ebner]

@Yaël Dillies If I understand the counterexample correctly, completely Boolean algebras are a strict subset of the complete Boolean algebras. (Because a complete Boolean algebra is completely distributive iff it is atomic.)

[Gabriel Ebner]

I don't have a strong opinion if we should strengthen the existing classes, or whether we should add new CompletelyDistribLattice and CompletelyBooleanAlgebra classes. Strengthening only the lattice one seems like a bad idea since we loose CompleteBooleanAlgebra.toCompletelyDistribLattice

[Yaël Dillies]

I assume the history of complete_distrib_lattice is that it was defined quite early on with no application in sight? In that case I see no problem with strengthening the definition.

[Gabriel Ebner]

How do you feel about strengthening CompleteBooleanAlgebra as well?

[Junyan Xu]

completely Boolean algebras are a strict subset of the complete Boolean algebras. (Because a complete Boolean algebra is completely distributive iff it is atomic.)

Maybe a more appropriate name is "completely distributive Boolean algebras" rather than "completely Boolean algebras", and these are just the boring powerset / atomic algebras, and I'm not sure if it deserves a separate typeclass.

• docs#complete_distrib_lattice doesn't seem to be a standard notion; in the MO link above it's just referred to as both a frame and a coframe. (It's tempted to call it "biframe" in analogy with docs#biheyting_algebra, but the name is used for a different notion.) If it's not used anywhere, I agree we should redefine it to be the actual completely distributive lattice (or remove it until we get to develop the theory of completely distributive lattices).
• On the other hand, the current docs#complete_boolean_algebra agrees with the standard notion of complete boolean algebras, so I don't think we need to change it. If we add the complete distributivity condition, then it becomes restricted to boring powerset/atomic algebras. However, I think the definition can be improved/streamlined, and here are my two cents (even though I'm not familiar with the order theory library to assess practicality/difficulty of my suggestions):
• docs#boolean_algebra should extend docs#heyting_algebra (I think currently they already have the same data fields)
• docs#order.frame should extend docs#heyting_algebra so that it has the data fields himp and compl, and we get le_himp_iff from which inf_Sup_le_supr_inf follows.
• Therefore inf_Sup_le_supr_inf can be removed from docs#order.frame, infi_sup_le_sup_Inf from docs#order.coframe, and both from docs#complete_boolean_algebra.

[Junyan Xu]

BTW, I was able to trace docs#complete_distrib_lattice to the commit refactor(*): import content from lean/library/data and library_dev 6 years ago by @Mario Carneiro but I have no idea where the content of the commit came from; I searched leanprover/lean and leanprover-community/lean but was unable to find complete_distrib_lattice.

[Gabriel Ebner]

I agree that complete Boolean algebras are a standard notion, and there are many nonatomic examples (even on the wikipedia page more than half of the examples are nonatomic). So we definitely shouldn't add any extra axioms to CompleteBooleanAlgebra.

[Yaël Dillies]

• I think it might be worth keeping this nonstandard notion as the common ancestor to complete_boolean_algebra and completely_distrib_lattice
• boolean_algebra already extends biheyting_algebra, which extends heyting_algebra
• Agreed. I didn't do the refactor because it involved adding a nice constructor to recover the current definitions, and I might also have completely forgotten about it.

[Gabriel Ebner]

just the boring powerset / atomic algebras, and I'm not sure if it deserves a separate typeclass.

Just because they're boring doesn't mean they don't deserve a type class. They are closed under pis, products, etc., and that type class would extend CompletelyDistribLattice. If you want to write code that is generic over Prop/Set α/β → Set α then that type class comes in handy.

[Gabriel Ebner]

Any suggestions for the name? CompleteAtomicBooleanAlgebra?

[Yaël Dillies]

What about CompletelyBooleanAlgebra?

[Yaël Dillies]

Actually, what do you think of DistribCompleteLattice/BooleanCompleteAlgebra CompleteDistribLattice vs CompleteBooleanAlgebra? Probably that's too cursed...

[Gabriel Ebner]

Junyuan didn't like completely Boolean algebra.

[Yaël Dillies]

Then maybe we don't actually need a new typeclass?

[Yaël Dillies]

We can use CompleteBooleanAlgebra + IsAtomic, right?

[Gabriel Ebner]

BooleanCompleteAlgebra

Complete Boolean algebras are a standard term in the literature, I don't think we should reorder the words here.

[Gabriel Ebner]

I didn't know about IsAtomic, we could indeed do [CompleteBooleanAlgebra α] [IsAtomic α].

[Mario Carneiro]

Junyan Xu said:

BTW, I was able to trace docs#complete_distrib_lattice to the commit refactor(*): import content from lean/library/data and library_dev 6 years ago by Mario Carneiro but I have no idea where the content of the commit came from; I searched leanprover/lean and leanprover-community/lean but was unable to find complete_distrib_lattice.

That is the "initial commit" of mathlib (not counting some earlier commits that were just setting up the project). Things at this stage were being imported from the lean 2 library, and leanprover-community/lean didn't even exist yet. If you want to keep tracing things back before that you need to go to https://github.com/avigad/library_dev

[Mario Carneiro]

the actual commit that adds it is https://github.com/avigad/library_dev/blob/f4a3afd4/algebra/lattice/complete_boolean_algebra.lean#L16-L18 but it's not too informative

[Junyan Xu]

boolean_algebra already extends biheyting_algebra, which extends heyting_algebra

Really? class BooleanAlgebra (α : Type u) extends DistribLattice , HasCompl , SDiff , HImp , Top , Bot docs4#BooleanAlgebra