disjoint decomposition

Stream: maths

[Johan Commelin]

I want to index over all disjoint (finite) decompositions of a (profinite) topological space into pairwise disjoint clopen sets:

$$S = U₁ ⊔ U₂ ⊔ … ⊔ Uₙ$$

I guess we have the lattice of clopen sets. So now I need to know how to say that a certain family of elements in a lattice is pairwise disjoint and has ⊤ as its Sup. Is there already a bundled notion for this? Or should I just handroll this?

[Anatole Dedecker]

We don't have a definition for both I think, but we have docs#complete_lattice.independent for the first one

[Anatole Dedecker]

Oh no actually, this is not the same as pairwise disjoint

[Kevin Buzzard]

There is docs#discrete_quotient

[Yaël Dillies]

If you have finitely many of those, you can use docs#finpartition.

[Yaël Dillies]

Precisely, you will want a finpartition (⊤ : clopens α).

[Kevin Buzzard]

By compactness there's only finitely many

[Johan Commelin]

Thanks!

[Johan Commelin]

Kevin Buzzard said:

There is docs#discrete_quotient

Yeah, I know, but I guess it's a bit ugly to talk about inverse images of points of the natural map to a discrete quotient all the time.

[Johan Commelin]

finpartition looks good

[Adam Topaz]

There is some api for constructing a discrete quotient from a clopen partition.