Order on partitions

Stream: maths

[Yaël Dillies]

If I tell you that P and Q are two partitions of a set, what do you expect P ≤ Q to mean? In particular, which of P and Q should have the most parts?

[Kevin Buzzard]

I would expect it to mean "there's a map from P to Q" so I would expect it to mean "if you're related by the P relation then you're related by the Q relation" so I'd expect P to have more parts

[Reid Barton]

This is also the convention on wikipedia

[Adam Topaz]

With this convention, the discrete partition is bot, just like the discrete topology.

[Adam Topaz]

You are aware or docs#setoid.partition.complete_lattice right?

[Yaël Dillies]

Hmm... That's annoying. Because if P ≤ Q means "there's a map from Q to P", then we can make it into a graded order with grade function the number of parts $- 1$ and state this theorem: image.png.

[Kevin Buzzard]

P ≤ Q iff there's a map from P to Q seems to be a mathlib-wide convention. For example with topologies T1 <= T2 iff the identity is a continuous map from T1 to T2, and with filters F1 <= F2 iff F1 tends to F2 along the identity map

[Kevin Buzzard]

I don't see the relevance of your screenshot. Theorems about maximal pairwise incomparable partitions won't care about which way the order is

[Yaël Dillies]

The convention for graded functions is for the grade function to go from α → ℕ and be monotone. This is not possible with the convention on partitions as that would mean the grade goes arbitrarily low.

[Kevin Buzzard]

For a general partial order it's not going to be nat-valued

[Yaël Dillies]

Yeah, so maybe I'll have to make a $\Z$-valued version too...

[Yaël Dillies]

It's sad because partitions would fit the $\N$ framework great were they ordered the other way.

[David Wärn]

Isn't the lattice of partitions of a finite type both "graded and cograded"? It has both top and bottom elements

[Yaël Dillies]

"of a finite type", yes. I'm talking in general. Even when the type is finite, your grade function won't ever be as nice as the number of parts minus 1.

[David Wärn]

But on a general type you have to restrict to finite partitions to get a grading, no? Or to cofinite partitions to get a cograding

[Yaël Dillies]

Yes, and we have #9795 which defines finite partitions. What's a cofinite partition?

[David Wärn]

I just made it up, but you would have to look at partitions where each part is finite and all but finitely many are singletons

[Yaël Dillies]

Oh, that's a funny one

[David Wärn]

On a finite type S the grade of a partition P will be card S - card P. Arguably this is even nice than card P - min(1, card S)

[Yaël Dillies]

Why not just card P - 1?

[Yaël Dillies]

An empty type is graded wrt to any grade function.

[David Wärn]

Actually card P - 1 does work with truncated nat subtraction. My point was that if S is empty then there is a unique partition and it has cardinality 0

[David Wärn]

Anyway I agree it would be nice to be able to talk about the graded lattice of finite partitions of a general type. But I don't think there's a strong reason to prefer either ordering over the other

[Yaël Dillies]

Btw #11308 for graded orders