The cycle type of a fibrewise permutation #
The cycle type of Equiv.Perm.sigmaCongrRight is the sum of the
fibres' cycle types: a fibrewise permutation moves each fibre inside
itself, so its orbits are the fibres' orbits.
theorem
RS.cycleType_sigmaCongrRight
{I : Type u_2}
[DecidableEq I]
[Fintype I]
{β : I → Type u_3}
[(i : I) → DecidableEq (β i)]
[(i : I) → Fintype (β i)]
(σ : (i : I) → Equiv.Perm (β i))
:
A fibrewise permutation's cycle type is the sum of the fibres': no cycle crosses between fibres.