Finite partitions #
In this file, we define finite partitions. A finpartition of a : α
is a finite set of pairwise
disjoint parts parts : Finset α
which does not contain ⊥
and whose supremum is a
.
Finpartitions of a finset are at the heart of Szemerédi's regularity lemma. They are also studied purely order theoretically in Sperner theory.
Constructions #
We provide many ways to build finpartitions:
Finpartition.ofErase
: Builds a finpartition by erasing⊥
for you.Finpartition.ofSubset
: Builds a finpartition from a subset of the parts of a previous finpartition.Finpartition.empty
: The empty finpartition of⊥
.Finpartition.indiscrete
: The indiscrete, aka trivial, aka pure, finpartition made of a single part.Finpartition.discrete
: The discrete finpartition ofs : Finset α
made of singletons.Finpartition.bind
: Puts together the finpartitions of the parts of a finpartition into a new finpartition.Finpartition.ofSetoid
: WithFintype α
, constructs the finpartition ofuniv : Finset α
induced by the equivalence classes ofs : Setoid α
.Finpartition.atomise
: Makes a finpartition ofs : Finset α
by breakings
along all finsets inF : Finset (Finset α)
. Two elements ofs
belong to the same part iff they belong to the same elements ofF
.
Finpartition.indiscrete
and Finpartition.bind
together form the monadic structure of
Finpartition
.
Implementation notes #
Forbidding ⊥
as a part follows mathematical tradition and is a pragmatic choice concerning
operations on Finpartition
. Not caring about ⊥
being a part or not breaks extensionality (it's
not because the parts of P
and the parts of Q
have the same elements that P = Q
). Enforcing
⊥
to be a part makes Finpartition.bind
uglier and doesn't rid us of the need of
Finpartition.ofErase
.
TODO #
The order is the wrong way around to make Finpartition a
a graded order. Is it bad to depart from
the literature and turn the order around?
A finite partition of a : α
is a pairwise disjoint finite set of elements whose supremum is
a
. We forbid ⊥
as a part.
- parts : Finset α
The elements of the finite partition of
a
- supIndep : self.parts.SupIndep id
The partition is supremum-independent
- sup_parts : self.parts.sup id = a
The supremum of the partition is
a
- not_bot_mem : ⊥ ∉ self.parts
No element of the partition is bottom
Instances For
The partition is supremum-independent
The supremum of the partition is a
No element of the partition is bottom
Equations
- instDecidableEqFinpartition = decEqFinpartition✝
A Finpartition
constructor which does not insist on ⊥
not being a part.
Equations
- Finpartition.ofErase parts sup_indep sup_parts = { parts := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
A Finpartition
constructor from a bigger existing finpartition.
Equations
- P.ofSubset subset sup_parts = { parts := parts, supIndep := ⋯, sup_parts := sup_parts, not_bot_mem := ⋯ }
Instances For
Changes the type of a finpartition to an equal one.
Equations
- P.copy h = { parts := P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
Transfer a finpartition over an order isomorphism.
Equations
- Finpartition.map e P = { parts := Finset.map (↑e).toEmbedding P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
The empty finpartition.
Equations
- Finpartition.empty α = { parts := ∅, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
Equations
- Finpartition.instInhabitedBot α = { default := Finpartition.empty α }
The finpartition in one part, aka indiscrete finpartition.
Equations
- Finpartition.indiscrete ha = { parts := {a}, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
Equations
- Finpartition.instUniqueBot = { toInhabited := inferInstance, uniq := ⋯ }
There's a unique partition of an atom.
Equations
- ha.uniqueFinpartition = { default := Finpartition.indiscrete ⋯, uniq := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Refinement order #
We say that P ≤ Q
if P
refines Q
: each part of P
is less than some part of Q
.
Equations
- Finpartition.instLE = { le := fun (P Q : Finpartition a) => ∀ ⦃b : α⦄, b ∈ P.parts → ∃ c ∈ Q.parts, b ≤ c }
Equations
- Finpartition.instPartialOrder = PartialOrder.mk ⋯
Equations
- Finpartition.instOrderTopOfDecidableEqBot = OrderTop.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- Finpartition.instMin = { min := fun (P Q : Finpartition a) => Finpartition.ofErase (Finset.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) ⋯ ⋯ }
Equations
- Finpartition.instSemilatticeInf = SemilatticeInf.mk min ⋯ ⋯ ⋯
Given a finpartition P
of a
and finpartitions of each part of P
, this yields the
finpartition of a
obtained by juxtaposing all the subpartitions.
Equations
Instances For
Adds b
to a finpartition of a
to make a finpartition of a ⊔ b
.
Equations
Instances For
Restricts a finpartition to avoid a given element.
Equations
- P.avoid b = Finpartition.ofErase (Finset.image (fun (x : α) => x \ b) P.parts) ⋯ ⋯
Instances For
Finite partitions of finsets #
The part of the finpartition that a
lies in.
Equations
Instances For
Equivalence between a finpartition's parts as a dependent sum and the partitioned set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⊥
is the partition in singletons, aka discrete partition.
Equations
- Finpartition.instBotFinset s = { bot := { parts := Finset.map { toFun := singleton, inj' := ⋯ } s, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ } }
Equations
A setoid over a finite type induces a finpartition of the type's elements, where the parts are the setoid's equivalence classes.
Equations
- Finpartition.ofSetoid s = { parts := Finset.image (fun (a : α) => Finset.filter (fun (b : α) => s a b) Finset.univ) Finset.univ, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }
Instances For
Cuts s
along the finsets in F
: Two elements of s
will be in the same part if they are
in the same finsets of F
.
Equations
- Finpartition.atomise s F = Finpartition.ofErase (Finset.image (fun (Q : Finset (Finset α)) => Finset.filter (fun (i : α) => ∀ t ∈ F, t ∈ Q ↔ i ∈ t) s) F.powerset) ⋯ ⋯