Disjoint subset in Boolean algebra?

Stream: maths

[David Loeffler]

I'm struggling to find a nice way of proving the following: if I have a finite family U of elements in a Boolean algebra L, I can find a (possibly smaller) family V of non-trivial, pairwise-disjoint elements whose supremum is the same as that of U, and such that each of the V's is bounded above by one of the U's.

More precisely, I'm trying to prove this:

lemma disjointify {ι L : Type*} [Fintype ι] [DecidableEq L] [BooleanAlgebra L] {U : ι → L} :
    ∃ (J : Finset ι) (V : J → L), (∀ j, V j ≠ ⊥ ∧ V j ≤ U j)
    ∧ (Finset.univ.sup V = Finset.univ.sup U) ∧ Pairwise (Disjoint on V) := by sorry

I have a proof which works – the idea is to fix an ordering on ι, define V i := U i \ (⋃ j < i, U j), and then throw away the i's for which V i is empty – but it's very long and ugly (~60 lines). So I strongly suspect someone must have done this before, and probably done it better! Is there anything like this in the library?

[Yaël Dillies]

docs#disjointed ?

[Yaël Dillies]

It's not exactly what you ask for because it doesn't throw away the ⊥ terms, but that should likely be a distinct operation anyway

[Yaël Dillies]

Annoyingly, disjointed hasn't yet been generalised away from sequences

[David Loeffler]

This does indeed look useful! If I drop the "nonempty" requirement then it can be done in 30 lines using disjointed:

lemma disjointify2 {ι L : Type*} [Fintype ι] [DecidableEq L] [BooleanAlgebra L] {U : ι → L} :
    ∃ V : ι → L, (∀ j, V j ≤ U j) ∧ Finset.univ.sup V = Finset.univ.sup U
    ∧ Pairwise (Disjoint on V) := by
  rcases isEmpty_or_nonempty ι with h | h
  · refine ⟨fun j ↦ ⊤, fun j => h.elim j, ?_, ?_⟩
    · simp only [Finset.top_eq_univ, Finset.univ_eq_empty, Finset.sup_empty]
    · exact fun i j hij ↦ (hij (Subsingleton.elim i j)).elim
  let R := Fintype.equivFin ι
  let U' : ℕ → L := U ∘ R.symm ∘ (↑)
  refine ⟨disjointed U' ∘ (↑) ∘ R, ?_, ?_, fun i j hij ↦ disjoint_disjointed U' ?_⟩
  · intro j
    simpa [U'] using (Pi.le_def.mp <| disjointed_le U') ↑(R j)
  · have : U' ∘ Fin.val ∘ R = U := by ext; simp [U']
    rw [← this]
    let RR : ι ↪ ℕ := ⟨Fin.val ∘ R, Fin.val_injective.comp R.injective⟩
    show Finset.univ.sup (disjointed U' ∘ RR) = Finset.univ.sup (U' ∘ RR)
    simp_rw [← Finset.sup_map, RR, Finset.map_eq_image, Function.Embedding.coeFn_mk]
    rw [← Finset.image_image, Finset.image_univ_equiv]
    have h : partialSups (disjointed U') (Fintype.card ι - 1) =
      partialSups U' (Fintype.card ι - 1) := by rw [partialSups_disjointed]
    simp only [partialSups_eq_sup_range, Nat.sub_add_cancel NeZero.one_le] at h
    suffices Finset.range (Fintype.card ι) = Finset.image Fin.val Finset.univ by
      rwa [this] at h
    · ext i
      simp only [Finset.mem_range, Finset.mem_image, Finset.mem_univ, true_and]
      constructor
      · intro hi
        use Fin.mk i hi
      · exact fun ⟨a, ha⟩ ↦ ha ▸ Fin.is_lt a
  · simpa only [Function.comp_apply, Fin.val_injective.ne_iff, R.injective.ne_iff]

I can add this to the library – maybe calling it Fintype.disjointed or something.

(I think I've only encountered "to disjoint", as a verb, in the context of cutting up meat for roasting. Do Christmas turkeys take values in a Boolean algebra?)