Partitions generated by functions and by families

The partition of a finite type generated by a function s : ι → β has the fibres of s as its blocks, i and j sharing a block when s i = s j; every partition of ι is generated by the function sending each element to its block (ofFun_part). A finite family φ : ι → α in a Boolean algebra generates a partition of ⊤ whose parts are its nonzero minterms, the meets ±φ i over all i. Permutations of ι act on its partitions by relabelling, and the multiset of block sizes is invariant.

Main definitions

• Finpartition.ofFun s: the partition of ι generated by s.
• minterm φ σ: the meet of φ i for the i with σ i true and of (φ i)ᶜ for the others.
• Finpartition.minterms φ: the partition of ⊤ into the nonzero minterms of φ.
• Finpartition.equivPartsMinterms φ: the nonzero minterms correspond to the polarity assignments at which the minterm does not vanish.
• Finpartition.partSizes P: the multiset of the sizes of the blocks.
• The action of Equiv.Perm ι on Finpartition (univ : Finset ι).

Main results

• Finpartition.ofFun_congr: the partition depends only on which values coincide.
• Finpartition.ofFun_le_ofFun_iff, Finpartition.le_iff_factorsThrough_part: one partition refines another exactly when the generator or block map of the second factors through that of the first.
• Finpartition.sum_parts_eq_sum_preimage_part: a sum over the parts is a sum over the fibres of the block map.
• disjoint_minterm, sup_minterm: distinct minterms are disjoint and the minterms join to ⊤.
• Finpartition.minterms_sumElim: the minterms of a union of two families are the meet of the two partitions.
• Finpartition.ofFun_part: every partition is generated by its blocks.
• Finpartition.partSizes_ofFun: the block sizes are the multiplicities of the values.
• Finpartition.partSizes_smul: relabelling a partition by a permutation keeps its block sizes.

[UPSTREAM] candidates for Mathlib.Order.Partition.Finpartition.

Minterms

def minterm {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] (φ : ι → α) (σ : ι → Bool) : α

The minterm of φ at σ is the meet of φ i for the i with σ i true and of (φ i)ᶜ for the others.

Equations

• minterm φ σ = Finset.univ.inf fun (i : ι) => if σ i = true then φ i else (φ i)ᶜ

theorem minterm_le_of_true {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} {σ : ι → Bool} {i : ι} (h : σ i = true) : minterm φ σ ≤ φ i

theorem minterm_le_compl_of_false {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} {σ : ι → Bool} {i : ι} (h : σ i = false) : minterm φ σ ≤ (φ i)ᶜ

theorem minterm_le_iff {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} {σ : ι → Bool} {i : ι} (h : minterm φ σ ≠ ⊥) : minterm φ σ ≤ φ i ↔ σ i = true

A nonzero minterm lies below φ i exactly when its polarity assignment makes i true.

theorem disjoint_minterm {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] {φ : ι → α} {σ τ : ι → Bool} (h : σ ≠ τ) : Disjoint (minterm φ σ) (minterm φ τ)

theorem minterm_sumElim {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [BooleanAlgebra α] [Fintype ι] [Fintype κ] (φ : ι → α) (ψ : κ → α) (σ : ι ⊕ κ → Bool) : minterm (Sum.elim φ ψ) σ = minterm φ (σ ∘ Sum.inl) ⊓ minterm ψ (σ ∘ Sum.inr)

theorem minterm_comp_equiv {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [BooleanAlgebra α] [Fintype ι] [Fintype κ] (e : κ ≃ ι) (φ : ι → α) (σ : κ → Bool) : minterm (φ ∘ ⇑e) σ = minterm φ (σ ∘ ⇑e.symm)

theorem sup_minterm {α : Type u_1} {ι : Type u_2} [BooleanAlgebra α] [Fintype ι] (φ : ι → α) [DecidableEq ι] : Finset.univ.sup (minterm φ) = ⊤

The minterms of a family join to ⊤.

def Finpartition.partSizes {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (P : Finpartition s) : Multiset ℕ

The multiset of the sizes of the blocks.

Equations

• P.partSizes = Multiset.map Finset.card P.parts.val

@[simp]

theorem Finpartition.sum_partSizes {ι : Type u_1} [DecidableEq ι] {s : Finset ι} (P : Finpartition s) : P.partSizes.sum = s.card

The block sizes add up to the size of the partitioned set.

theorem Finpartition.part_bot {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∈ s) : ⊥.part i = {i}

In the discrete partition every element is alone in its block.

def Finpartition.ofFun {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] (s : ι → β) : Finpartition Finset.univ

The partition of ι generated by s puts two elements in one block when s takes the same value at both.

Equations

• Finpartition.ofFun s = Finpartition.ofSetoid (Setoid.ker s)

theorem Finpartition.parts_ofFun {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] (s : ι → β) : (ofFun s).parts = Finset.image (fun (i : ι) => {j : ι | s i = s j}) Finset.univ

theorem Finpartition.mem_part_ofFun {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] {s : ι → β} {i j : ι} : j ∈ (ofFun s).part i ↔ s i = s j

theorem Finpartition.ofFun_congr {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] {γ : Type u_3} [DecidableEq γ] {s : ι → β} {t : ι → γ} (h : ∀ (i j : ι), s i = s j ↔ t i = t j) : ofFun s = ofFun t

The partition generated by a function depends only on which of its values coincide.

theorem Finpartition.ofFun_part {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : Finpartition Finset.univ) : ofFun P.part = P

Every partition of ι is generated by the function sending each element to its block.

theorem Finpartition.sum_parts_eq_sum_preimage_part {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_3} [AddCommMonoid M] (P : Finpartition Finset.univ) {F : Set ι → M} (hF : F ∅ = 0) : ∑ c ∈ P.parts, F ↑c = ∑ c : Finset ι, F (P.part ⁻¹' {c})

Summing a function of the parts that vanishes at ∅ is summing it over the fibres of the block map.

theorem Finpartition.partSizes_ofFun {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] (s : ι → β) : (ofFun s).partSizes = Multiset.map (fun (v : β) => {i : ι | s i = v}.card) (Finset.image s Finset.univ).val

The block sizes of the partition generated by s are the multiplicities of its values.

@[simp]

theorem Finpartition.card_partSizes_ofFun {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] (s : ι → β) : (ofFun s).partSizes.card = (Finset.image s Finset.univ).card

The partition generated by s has one block per value.

theorem Finpartition.part_ofFun_eq_part_ofFun_iff {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] {s : ι → β} {i j : ι} : (ofFun s).part i = (ofFun s).part j ↔ s i = s j

theorem Finpartition.ofFun_le_ofFun_iff {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] {γ : Type u_3} [DecidableEq γ] {s : ι → β} {t : ι → γ} : ofFun s ≤ ofFun t ↔ Function.FactorsThrough t s

One generated partition refines another exactly when the second generator factors through the first.

theorem Finpartition.le_iff_factorsThrough_part {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P Q : Finpartition Finset.univ} : P ≤ Q ↔ Function.FactorsThrough Q.part P.part

A partition refines another exactly when the block map of the second factors through that of the first.

theorem Finpartition.ofFun_part_ofFun_comp {ι : Type u_1} {β : Type u_2} [Fintype ι] [DecidableEq ι] [DecidableEq β] (s : ι → β) (g : ι → ι) : ofFun ((ofFun s).part ∘ g) = ofFun (s ∘ g)

Composing the block map of a generated partition with g generates the same partition as composing the generator with g.

Relabelling by permutations

@[instance_reducible]

instance Finpartition.instMulActionPermFinsetUniv_linglib {ι : Type u_1} [Fintype ι] [DecidableEq ι] : MulAction (Equiv.Perm ι) (Finpartition Finset.univ)

A permutation σ of ι relabels a partition of ι, moving each block B to σ '' B.

Equations

• Finpartition.instMulActionPermFinsetUniv_linglib = { smul := fun (σ : Equiv.Perm ι) (P : Finpartition Finset.univ) => Finpartition.ofFun (P.part ∘ ⇑σ⁻¹), mul_smul := ⋯, one_smul := ⋯ }

theorem Finpartition.smul_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) (P : Finpartition Finset.univ) : σ • P = ofFun (P.part ∘ ⇑σ⁻¹)

theorem Finpartition.partSizes_smul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : Equiv.Perm ι) (P : Finpartition Finset.univ) : (σ • P).partSizes = P.partSizes

Relabelling preserves the block sizes.

The partition into minterms

def Finpartition.minterms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} [BooleanAlgebra α] [DecidableEq α] (φ : ι → α) : Finpartition ⊤

The partition of ⊤ generated by a family has its nonzero minterms as parts.

Equations

• Finpartition.minterms φ = Finpartition.ofErase (Finset.image (minterm φ) Finset.univ) ⋯ ⋯

theorem Finpartition.mem_minterms_parts {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} [BooleanAlgebra α] [DecidableEq α] {φ : ι → α} {a : α} : a ∈ (minterms φ).parts ↔ a ≠ ⊥ ∧ ∃ (σ : ι → Bool), minterm φ σ = a

noncomputable def Finpartition.equivPartsMinterms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} [BooleanAlgebra α] [DecidableEq α] (φ : ι → α) : { σ : ι → Bool // minterm φ σ ≠ ⊥ } ≃ ↥(minterms φ).parts

The nonzero minterms of a family correspond to the polarity assignments at which its minterm does not vanish.

Equations

• Finpartition.equivPartsMinterms φ = Equiv.ofBijective (fun (σ : { σ : ι → Bool // minterm φ σ ≠ ⊥ }) => ⟨minterm φ ↑σ, ⋯⟩) ⋯

@[simp]

theorem Finpartition.coe_equivPartsMinterms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} [BooleanAlgebra α] [DecidableEq α] {φ : ι → α} (σ : { σ : ι → Bool // minterm φ σ ≠ ⊥ }) : ↑((equivPartsMinterms φ) σ) = minterm φ ↑σ

theorem Finpartition.card_parts_minterms {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} [BooleanAlgebra α] [DecidableEq α] (φ : ι → α) : (minterms φ).parts.card = {σ : ι → Bool | minterm φ σ ≠ ⊥}.card

A family has as many nonzero minterms as polarity assignments at which its minterm does not vanish.

theorem Finpartition.parts_minterms_comp_equiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} {κ : Type u_4} [BooleanAlgebra α] [DecidableEq α] [Fintype κ] [DecidableEq κ] (e : κ ≃ ι) (φ : ι → α) : (minterms (φ ∘ ⇑e)).parts = (minterms φ).parts

Reindexing a family does not change its minterms.

theorem Finpartition.minterms_sumElim {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_3} {κ : Type u_4} [BooleanAlgebra α] [DecidableEq α] [Fintype κ] [DecidableEq κ] (φ : ι → α) (ψ : κ → α) : minterms (Sum.elim φ ψ) = minterms φ ⊓ minterms ψ

The minterms of the union of two families form the meet of their partitions into minterms.