lattice_bot

Stream: general

[Yaël Dillies]

We don't have lattice_bot. It turns out it is the correct generality for the following definition:

/-- A finite partition of `a : α` is a pairwise disjoint finite set of elements whose supremum is
`a`. -/
@[ext] structure finpartition {α : Type*} [bounded_lattice α] (a : α) :=
(parts : finset α)
(disjoint : (parts : set α).pairwise_disjoint)
(sup_parts : parts.sup id = a)
(not_bot_mem : ⊥ ∉ parts)

[Yaël Dillies]

I could replace the final field by (not_bot_of_mem {b : α} : b ∈ parts → ¬ is_bot b), but that's pretty artificial and, most importantly, I still can't prove lemmas in terms of ⊥ . So do people mind if I define lattice_bot?

[Yaël Dillies]

My use case is finset α, which is indeed not a bounded_lattice.

[Kevin Buzzard]

finset α is a semilattice_sup_bot, right?

[Yaël Dillies]

Yep, but pairwise_disjoint needs a semilattice_inf_bot. I really need both sup and inf here

[Scott Morrison]

I wonder if we should consider breaking out has_top as a Prop valued mixin. When we have partial_order (rather than preorder) the bottom element is unique and we could nonconstructively provide it via ⊥.

[Scott Morrison]

(Thereby hopefully getting rid of semilattice_(sup|inf)_(top|bot), and avoiding the need here for lattice_(top|bot).

[Yaël Dillies]

Yeah, I was already thinking that when adding distrib_lattice_bot a while back.

[Yaël Dillies]

The question is how far we want to go that way. For example, what about decoupling has_inf and has_sup as well?

[Scott Morrison]

I think the problem will be that we'll no longer be able to write bounded_lattice, but instead some huge chain of [order_bot] [order_top] [semilattice_inf] [semilattice_sup]. Perhaps we should wait to see if [[lattice]] notation as discussed previously (i.e. automatically add all transitively required typeclass arguments) might be available in Lean4.

[Scott Morrison]

Then we could redefine bounded_lattice as a completely empty typeclass (no fields, no ancestors!), but that requires all these constituent parts.

[Yaël Dillies]

That's not the only obstacle, right? I thought there was this exponential explosion of underlying terms when computing the prod of the prod of the prod...

[Yaël Dillies]

Did we just decide that this doesn't come up enough in practice to bother?

[Scott Morrison]

I think this is the main previous discussion of this blow-up.

[Scott Morrison]

But I don't understand this well enough to guess how this would affect the bounded_lattice change discussed above.