distrib_lattice_bot

Stream: general

[Yaël Dillies]

I saw the todo about disjoint_sup_left and similar. What do you think of me defining distrib_lattice_bot for these lemmas to be general enough? I just hit a point where I wanted to use them in a generalized_boolean_algebra.

[Yaël Dillies]

So I'm doing that on the branch distrib_lattice_botand I've encountered this TODO in order.boolean_algebra:

/- TODO: if we had a typeclass for distributive lattices with `⊥`, we could make an alternative
constructor for `generalized_boolean_algebra` using `disjoint x (y \ x)` and `x ⊔ (y \ x) = y` as
axioms. -/

[Yaël Dillies]

inf_inf_sdiff was easy, but I'm stuck on sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a.

[Yaël Dillies]

/me is writing a MWE

[Yaël Dillies]

if anyone has a paper proof already...

import order.boolean_algebra

/-- A `distrib_lattice_bot` is a distributive with a least element. -/
class distrib_lattice_bot α extends distrib_lattice α, semilattice_inf_bot α, semilattice_sup_bot α

def generalized_boolean_algebra_of_disjoint_sdiff_self_right_of_sup_sdiff_cancel_left {α : Type*}
  [dlb : distrib_lattice_bot α] [sd : has_sdiff α]
  (hdisjoint_sdiff_self_right : ∀ x y : α, disjoint x (y \ x))
  (hsup_sdiff_cancel_left : ∀ ⦃x y : α⦄, disjoint x y → (x ⊔ y) \ x = y) :
  generalized_boolean_algebra α :=
{ sup_inf_sdiff := λ x y, begin
    sorry
  end,
  inf_inf_sdiff := λ x y, disjoint.eq_bot ((hdisjoint_sdiff_self_right y x).mono_left inf_le_right),
  ..dlb,
  ..sd }

[Eric Rodriguez]

that mwe errors with "invalid 'structure' header, field 'le' from 'semilattice_inf_bot' has already been declared"

[Kevin Buzzard]

Guess: set_option old_structure_cmd true might fix it? This is precisely the sort of thing it fixes.

[Kevin Buzzard]

(Note that old structures are not in Lean 4 -- Leo is forcing us to build them manually because the way we've been using them in Lean 3 apparently creates massive objects behind the scenes. This will involve a re-think of the hierarchy but I am still hazy on the details and would rather not derail this thread.)

[Eric Rodriguez]

ahh yes, thanks :)

[Yaël Dillies]

Kevin Buzzard said:

This will involve a re-think of the hierarchy

Uh...

[Eric Rodriguez]

the note says x ⊔ (y \ x) = y unconditionally, but you wrote (x ⊔ y) \ x = y for disjoint x y; going to try the note's version

[Eric Rodriguez]

hmm, but to be fair the notes' version doesn't work in my mental model

[Eric Rodriguez]

(the unconditionalness anyways)

[Yaël Dillies]

I think that maybe you need to assume x \ y ≤ x. Also, (x ⊔ y) \ x = y gives you the result for all elements that can be written as the sup of a ⊓ a and a \ b for some a, b. But the only way I can think of to find these is precisely using \...

[Yaël Dillies]

Eric Rodriguez said:

the note says x ⊔ (y \ x) = y unconditionally, but you wrote (x ⊔ y) \ x = y for disjoint x y; going to try the note's version

Wait but unconditionnally that's wrong. We don't have (x ⊔ x) \ x = x

[Eric Rodriguez]

yes, so your version is wrong :b

[Eric Rodriguez]

x ⊔ (x \ x) = x is right to me

[Yaël Dillies]

Oh what I can't even bracket a statement properly.

[Yaël Dillies]

Ah yeah I had my mental priority for inf too high.

[Yaël Dillies]

And I thought it had to do with the following (spacially) lemma

theorem disjoint.sdiff_eq_of_sup_eq (hi : disjoint x z) (hs : x ⊔ z = y) : y \ x = z :=
have h : y ⊓ x = x := inf_eq_right.2 $ le_sup_left.trans hs.le,
sdiff_unique (by rw [h, hs]) (by rw [h, hi.eq_bot])

[Yaël Dillies]

But x ⊔ (y \ x) = y is still not true...

[Eric Rodriguez]

when is that not true? i live in a model of lattices where all lattices are like sets

[Eric Rodriguez]

wait nvm

[Eric Rodriguez]

yes of course

[Eric Rodriguez]

who wrote that note?

[Yaël Dillies]

@Bryan Gin-ge Chen

[Yaël Dillies]

Not long ago, actually!

[Eric Rodriguez]

I swear he was online more recently than two weeks ago...

[Yaël Dillies]

Yeah, he answered something today at 5 in the morning.

[Bryan Gin-ge Chen]

Hmm, I don't remember what I was thinking... let me see if I can dig up some notes later.

[Bryan Gin-ge Chen]

I can't find my notes, so I think you can just delete that TODO for now. If I ever figure out what I meant I'll come back to this. Thanks for #8507 by the way!