Cycle partitions of permutations on dependent sums #
A permutation acting separately on the fibres of a dependent sum has the cycles of all its fibre permutations, including their fixed points. This gives the cycle partitions and cycle counts used when a finite cover is decomposed into its connected components.
The partition calculation uses Equiv.Perm.fullCycleType_eq_sum_subtypePerm, the
invariant-fibre decomposition theorem, and Equiv.sigmaSubtype to identify each fibre.
@[simp]
theorem
Equiv.Perm.parts_partition_sigmaCongrRight
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[(i : ι) → Fintype (α i)]
[DecidableEq ι]
[(i : ι) → DecidableEq (α i)]
(σ : (i : ι) → Perm (α i))
:
The full cycle partition of a permutation on a dependent sum is the sum of the full cycle partitions on the fibres. Fixed points contribute parts equal to one.
@[simp]
theorem
Equiv.Perm.orbitCount_sigmaCongrRight
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[∀ (i : ι), Finite (α i)]
(σ : (i : ι) → Perm (α i))
:
The number of cycles of a permutation on a dependent sum is the sum of the cycle counts on its fibres. Empty fibres and an empty index type are allowed.