English
The partition associated to a permutation σ is the sum of its cycle type and a multiset of 1's accounting for fixed points.
Русский
Разбиение, соответствующее перестановке σ, есть сумма её типа циклов и мультасета единиц, соответствующих фиксированным точкам.
LaTeX
$$σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1$$
Lean4
/-- The partition corresponding to a permutation -/
def partition (σ : Perm α) : (Fintype.card α).Partition
where
parts := σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
parts_pos
{n hn} := by
rcases mem_add.mp hn with hn | hn
· exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)
· exact lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))
parts_sum := by
rw [sum_add, sum_cycleType, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id, mul_one,
add_tsub_cancel_of_le σ.support.card_le_univ]
