Block sizes and pullbacks of set partitions
DefinitionProduct over block sizes#✓fully proved
For a partition \(P\) of a finite set \(s\), a commutative monoid \(R\) and a function \(f : \mathbb{N} \to R\), the block-size product of \(f\) over \(P\) is \(\prod_{B \in P} f(|B|)\), the product over the blocks \(B\) of \(P\) of \(f\) applied to the cardinality of \(B\).
def cardProd {R : Type*} [CommMonoid R] (P : Finpartition s) (f : ℕ → R) : R :=
∏ B ∈ P.parts, f B.cardUsed by 14
TheoremBlocks are no larger than the ground set#✓fully proved
If \(P\) is a partition of a finite set \(s\) and \(B\) is a block of \(P\), then \(|B| \le |s|\).
theorem card_le_of_mem_parts (P : Finpartition s) {B : Finset α} (hB : B ∈ P.parts) :
B.card ≤ s.cardTheoremBlocks are nonempty#✓fully proved
Every block \(B\) of a partition of a finite set \(s\) satisfies \(|B| \ge 1\).
theorem one_le_card_of_mem_parts (P : Finpartition s) {B : Finset α}
(hB : B ∈ P.parts) : 1 ≤ B.cardUsed by 1
TheoremBlocks of a partition other than the coarsest are smaller than the ground set#✓fully proved
Let \(P\) be a partition of a finite set \(s\) that is not the coarsest partition \(\top\) of \(s\) (the one whose only block is \(s\) when \(s\) is nonempty). Then every block \(B\) of \(P\) satisfies \(|B| < |s|\).
theorem card_lt_of_ne_top (P : Finpartition s) (h_ne_top : P ≠ ⊤)
{B : Finset α} (hB : B ∈ P.parts) : B.card < s.cardUsed by 1
TheoremRecognizing the one-block partition#✓fully proved
If \(P\) is a partition of a nonempty finite set \(s\), then \(P\) is the coarsest partition \(\top\) of \(s\), whose only block is \(s\), if and only if \(P\) has exactly one block.
theorem eq_top_iff_card_parts_eq_one (P : Finpartition s) (hs : s.Nonempty) :
P = ⊤ ↔ P.parts.card = 1TheoremA partition has a block exactly when its ground set is nonempty#✓fully proved
A partition \(P\) of a finite set \(s\) has at least one block, that is, its number of blocks is positive, if and only if \(s\) is nonempty.
theorem card_parts_pos_iff (P : Finpartition s) :
0 < P.parts.card ↔ s.NonemptyUsed by 5
TheoremRecognizing the partition into singletons by its number of blocks#✓fully proved
A partition \(P\) of a finite set \(s\) is the finest partition \(\bot\) of \(s\), whose blocks are the singletons \(\{a\}\) for \(a \in s\), if and only if the number of blocks of \(P\) equals \(|s|\).
theorem eq_bot_iff_card_parts_eq_card (P : Finpartition s) :
P = ⊥ ↔ P.parts.card = s.cardTheoremMonoid homomorphisms preserve block-size products#✓fully proved
Let \(P\) be a partition of a finite set \(s\), let \(R\) and \(S\) be commutative monoids, let \(f : \mathbb{N} \to R\), and let \(g : R \to S\) be a monoid homomorphism. Then \(g\bigl(\prod_{B \in P} f(|B|)\bigr) = \prod_{B \in P} g(f(|B|))\), where both products run over the blocks \(B\) of \(P\).
theorem cardProd_mapMonoidHom {R S : Type*} [CommMonoid R] [CommMonoid S]
(P : Finpartition s) (f : ℕ → R) (g : R →* S) :
g (P.cardProd f) = P.cardProd (g ∘ f)Uses 1
DefinitionPull-back of a finite partition along a map#✓fully proved
The pull-back of a partition P of the finite type β along a map f : α → β:
the blocks are the nonempty preimages f ⁻¹' B of the blocks B of P.
def comap (f : α → β) (P : Finpartition (univ : Finset β)) : Finpartition (univ : Finset α) :=
ofExistsUnique ((P.parts.image fun B ↦ univ.filter fun a ↦ f a ∈ B).erase ∅)
(fun _ _ ↦ subset_univ _)
(fun a _ ↦ by
obtain ⟨B, ⟨hB, hfa⟩, hu⟩ := P.existsUnique_mem (mem_univ (f a))
refine ⟨univ.filter fun x ↦ f x ∈ B, ⟨?_, by simp [hfa]⟩, ?_⟩
· exact mem_erase.2 ⟨ne_empty_of_mem (a := a) (by simp [hfa]), mem_image_of_mem _ hB⟩
· rintro C ⟨hC, haC⟩
obtain ⟨B', hB', rfl⟩ := mem_image.1 (mem_erase.1 hC).2
have : B' = B := hu B' ⟨hB', by simpa using haC⟩
rw [this])
(by simp)Used by 25
TheoremBlocks of a pulled-back partition#✓fully proved
The blocks of P.comap f are the nonempty preimages of the blocks of P.
theorem mem_comap_parts {f : α → β} {P : Finpartition (univ : Finset β)} {C : Finset α} :
C ∈ (P.comap f).parts ↔
C.Nonempty ∧ ∃ B ∈ P.parts, (univ.filter fun a ↦ f a ∈ B) = CUses 1 · Used by 8
TheoremPulling back a partition along the identity#✓fully proved
Pulling back along the identity does nothing.
@[simp]
theorem comap_refl (P : Finpartition (univ : Finset α)) :
P.comap id = PUses 2 · Used by 2
TheoremPulling back a partition along a composite#✓fully proved
Pulling back along a composite is pulling back twice.
theorem comap_comap (f : α → β) (g : β → γ) (P : Finpartition (univ : Finset γ)) :
(P.comap g).comap f = P.comap (g ∘ f)Uses 2 · Used by 2
TheoremBlocks of a partition pulled back along an equivalence#✓fully proved
Along an equivalence e, the blocks of P.comap e are the images of the blocks of P
under e.symm.
theorem parts_comap_equiv (e : α ≃ β) (P : Finpartition (univ : Finset β)) :
(P.comap e).parts = P.parts.map (mapEmbedding e.symm.toEmbedding).toEmbeddingUses 2 · Used by 2
TheoremPull-back along an equivalence preserves the number of blocks#✓fully proved
Pulling back along an equivalence preserves the number of blocks.
theorem card_parts_comap_equiv (e : α ≃ β) (P : Finpartition (univ : Finset β)) :
#(P.comap e).parts = #P.partsUses 2 · Used by 4
TheoremPull-back along an equivalence preserves block-size products#✓fully proved
Pulling back along an equivalence preserves every product over the block sizes.
theorem cardProd_comap_equiv {R : Type*} [CommMonoid R] (e : α ≃ β)
(P : Finpartition (univ : Finset β)) (g : ℕ → R) :
(P.comap e).cardProd g = P.cardProd gUses 3 · Used by 2
TheoremPulling back along an equivalence and its inverse#✓fully proved
Pulling back along e and then along e.symm gives back the partition.
@[simp]
theorem comap_symm_comap (e : α ≃ β) (P : Finpartition (univ : Finset β)) :
(P.comap e).comap e.symm = PUses 3 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.