Lattice structure on partitions

Stream: maths

[Lua Viana Reis]

I'm trying to write the complete lattice structure on Partition s, but the definition of the infimum turned out to be a bit complicated.

Informally, if we were talking about partitions of a set $S$, they could be seen as functions $P \colon S \to \mathsf{2}^S$ satisfying certain things. Then, the infimum of a set $\mathcal{P}$ of partitions would be the function that takes a point to the intersection of all elements containing it:

$$\left(\bigwedge \mathcal{P} \right)(x) = \bigcap_{P \in \mathcal{P}} P(x).$$

Now, for lattices, this does not work directly because the definition is not in terms of points. I guess the most direct translation is to say that $P$ is an element of $\bigwedge \mathcal{P}$ if $P \neq \bot$ and there is a choice of sets $f \colon (Q : \mathcal{P}) \to Q$ such that $P = \bigwedge_{Q \in \mathcal{P}} f(Q)$. This is what I did below, but I wonder if there is a better way. I am wondering if it could be worth it to formulate partitions in terms of equivalence relation on atoms of the lattice, and then the infimum would just correspond to the conjunction of all relations. Perhaps such formulation could also bridge the gap with Mathlib.Data.Setoid.Partition, using the set of atoms. What do you think?

MWE:

import Mathlib

variable {α : Type*} {s : α}

variable [CompleteLattice α] {P : Partition s}

open Set

namespace Partition

lemma eq_of_le (P : Partition s) (hx : x ∈ P) (hy : y ∈ P) (hxy : x ≤ y) : x = y :=
  P.pairwiseDisjoint.eq_of_le hx hy (P.ne_bot_of_mem hx) hxy

section Lattice

instance : LE (Partition s) where
  le P Q := ∀ q ∈ Q.parts, ∃ p ∈ P.parts, q ≤ p

-- otherwise, it would use the instance from SetLike
instance : LT (Partition s) where
  lt := fun a b => a ≤ b ∧ ¬b ≤ a

instance : CompleteSemilatticeInf (Partition s) where
  le_refl := by tauto
  le_trans P Q R hPQ hQR r hr := by
    have ⟨q, hq, hrq⟩ := hQR r hr
    let ⟨p, hp, hqp⟩ := hPQ q hq
    exact ⟨p, hp, hrq.trans hqp⟩
  le_antisymm P Q hPQ hQP := by
    suffices ∀ {A B} (hAB : A ≤ B) (hBA : B ≤ A) {t : α} (ht : t ∈ A), t ∈ B from
      Partition.ext fun _ => ⟨this hPQ hQP, this hQP hPQ⟩
    intro A B hAB hBA t ht
    let ⟨b, hb, htb⟩ := hBA t ht
    let ⟨a, ha, hta⟩ := hAB b hb
    have : t = a := A.eq_of_le ht ha (htb.trans hta)
    have : t = b := le_antisymm htb (this ▸ hta)
    exact this ▸ hb
  sInf ι := {
    parts p := p ≠ ⊥ ∧ ∃ (k : ι → α), ∀ P, k P ∈ P.val ∧ iInf k = p
    sSupIndep' := _
    bot_notMem' p := p.1 rfl
    sSup_eq' := by
      rw [←isLUB_iff_sSup_eq]
      refine ⟨fun a ha => ?_, fun a ha => ?_⟩
      · done
      · done
  }
  sInf_le := _
  le_sInf := _

[Aaron Liu]

does that work?

[Aaron Liu]

I don't think they're sSupIndep

[Lua Viana Reis]

Well I have little idea, I was just assuming that they would work like the set ones

[Aaron Liu]

since every part of the original partitions is also an element of the infimum

[Aaron Liu]

the way you defined it

[Lua Viana Reis]

Aaron Liu said:

since every part of the original partitions is also an element of the infimum

no? they are intersections the infimum of one element of each, when it is nonempty non-bot

[Aaron Liu]

no? did I misread that?

[Aaron Liu]

oh yes I seem to have misread

[Lua Viana Reis]

the question is I think the Partition s could be equivalentely defined as an equivalence relation on {a // IsAtom a}, perhaps someone has a better idea on that

[Aaron Liu]

what if there are no atoms

[Kenny Lau]

@Lua Viana Reis does the function you described (Partition s -> Set (Set s)) make it a complete sublattice? ah, no, it isn't, because the bottom element is not preserved

[Kenny Lau]

but from another angle, which (complete) lattice operations are preserved via that map?

[Kenny Lau]

ok this is tricky, it doesn't seem like any operation is preserved, please ignore my comments

[Lua Viana Reis]

Kenny Lau said:

function you described (Partition s -> Set (Set s))

do you mean, taking an element of the partition to a set of atoms? (Partition s -> Set {a // IsAtom a}?)

[Kenny Lau]

ah, sorry i was just looking at the sets (e.g. partitioning {a,b,c} into {a} and {b,c} would correspond to the set {{a},{b,c}}).

if we look at the function you described it would have type Partition s -> (s -> Set s) and this time top is in the image luckily

[Lua Viana Reis]

if you mean, if the meet/join of two partitions is somehow related to the union/intersection of their carrier sets, then not at all I think

[Kenny Lau]

image.png

[Kenny Lau]

i think i'm just restating this fact from your top message

[Kenny Lau]

which means it preserves arbitrary infimum

[Lua Viana Reis]

Aaron Liu said:

what if there are no atoms

perhaps the fact Partition s requires a CompleteLattice makes it work?

[Aaron Liu]

oh right

[Aaron Liu]

no you can still have atomless complete boolean algebras

[Aaron Liu]

found it https://gist.github.com/GSheaf/7f51c73ec64a473c420720ce95bcfe73

[Lua Viana Reis]

can you define a non-trivial partition on it?

[Aaron Liu]

yes

[Aaron Liu]

well, depends on what you mean by "nontrivial"

[Lua Viana Reis]

Aaron Liu said:

well, depends on what you mean by "nontrivial"

I mean, different from {⊤}

well the regular open algebra examples make a lot of sense, so the atom idea does not work at all. Do the partitions still form a complete lattice? I don't think so anymore

[Aaron Liu]

yes this atomless boolean algebra gives you nontrivial partitions

[Lua Viana Reis]

For a non-example, the infimum of a family of partitions $P_i$ in the regular open algebra of, say, $[0,1]$, such that the diameter of the elements of $P_i$ tends to 0, would certainly not exist

[Aaron Liu]

oh since it's not regular anymore

[Aaron Liu]

yeah I can see that

[Lua Viana Reis]

Is a [CompleteLattice L] such that all l : Lcontains an atom $a \le l$, isomorphic to Set {a // IsAtom a}? :innocent:

[Aaron Liu]

atom meaning a minimal non-bot element?

[Aaron Liu]

the answer is no

[Aaron Liu]

consider Filter Nat

[Aaron Liu]

it's a complete coheyting algebra but not a heyting algebra

[Aaron Liu]

atoms are ultrafilters

[Aaron Liu]

everything having an atom beneath it is the ultrafilter lemma

[Aaron Liu]

but the atoms are not docs#sSupIndep

[Lua Viana Reis]

I think the lattice structure could still be defined for general Partition s, and then I can prove that the Set one is complete

[Aaron Liu]

I could believe that for a distributive lattice

[Aaron Liu]

I guess a complete distributive lattice since the definition of Partition requires a complete lattice

[Lua Viana Reis]

well I should think and/or try first before posting more nonsense here :upside_down:

[Lua Viana Reis]

Aaron Liu said:

the answer is no

The algebra of open sets of the Sierpiński topology is a smaller counterexample

[Aaron Liu]

ah yes

[Aaron Liu]

Fin 3

[Lua Viana Reis]

@Aaron Liu in any case, thanks for the examples!

I'm not familiar with this algebra stuff, my goal is to have partitions to use in dynamics. But this is very interesting. I'm now reading about congruence lattices, and I have no idea if they are the same thing as the partitions of mathlib, but look very close to that

[Aaron Liu]

what's a congruence lattice

[Lua Viana Reis]

(nevermind)

[Lua Viana Reis]

Is this desirable for Mathlib?

namespace Partition

lemma eq_of_le (P : Partition s) (hx : x ∈ P) (hy : y ∈ P) (hxy : x ≤ y) : x = y :=
  P.pairwiseDisjoint.eq_of_le hx hy (P.ne_bot_of_mem hx) hxy

section PartialOrder

instance : LE (Partition s) where
  le P Q := ∀ q ∈ Q.parts, ∃ p ∈ P.parts, q ≤ p

-- otherwise, it would use the instance from SetLike
instance : LT (Partition s) where
  lt := fun a b => a ≤ b ∧ ¬b ≤ a

instance : PartialOrder (Partition s) where
  le_refl := by tauto
  le_trans P Q R hPQ hQR r hr := by
    let ⟨q, hq, hrq⟩ := hQR r hr
    let ⟨p, hp, hqp⟩ := hPQ q hq
    exact ⟨p, hp, hrq.trans hqp⟩
  le_antisymm P Q hPQ hQP := by
    suffices ∀ {A B} (hAB : A ≤ B) (hBA : B ≤ A) {t : α} (ht : t ∈ A), t ∈ B from
      Partition.ext fun _ => ⟨this hPQ hQP, this hQP hPQ⟩
    intro A B hAB hBA t ht
    let ⟨b, hb, htb⟩ := hBA t ht
    let ⟨a, ha, hta⟩ := hAB b hb
    have : t = a := A.eq_of_le ht ha (htb.trans hta)
    have : t = b := le_antisymm htb (this ▸ hta)
    exact this ▸ hb

end PartialOrder

[Aaron Liu]

I feel like it's gonna cause a diamond with the setlike instance

[Aaron Liu]

yet another reason why the setlike instance is a bad idea

[Lua Viana Reis]

Ugh, I just realized that ergodic theory apparently uses the dual of the order on the partitions everyone else in mathematics does (that's why the order I wrote above is the opposite of the existing one on Finpartition)...