Cycle types that count fixed points

Equiv.Perm.cycleType σ lists the lengths of the cycles of σ that are at least two, so it forgets the fixed points and is a partition of σ.support.card rather than of the ambient cardinality. The factorization type of a polynomial modulo a prime is, by contrast, a partition of the degree that keeps its parts equal to one. The corrected invariant

σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1

is already in Mathlib: it is (Equiv.Perm.partition σ).parts, the multiset of parts of Equiv.Perm.partition, and Equiv.Perm.parts_partition is its defining equation. This file adds the API that a comparison with a multiset of factor degrees needs, on that multiset.

Main results

• fullCycleType is the canonical name for the complete cycle-length multiset; its bridge to Mathlib's partition API and its sum, identity, conjugacy, and transport lemmas are included.
• Equiv.Perm.count_one_parts_partition, Equiv.Perm.count_parts_partition_of_ne_one: the parts equal to one are the fixed points of σ, and at every value other than one the multiset counts a part as often as Equiv.Perm.cycleType does. Together with Mathlib's Equiv.Perm.filter_parts_partition_eq_cycleType these say that no information is gained or lost.
• Equiv.Perm.parts_partition_eq_cycleType_iff: the correction is trivial exactly for a permutation with no fixed point.
• Equiv.Perm.parts_partition_conj: the multiset is constant on conjugacy classes.
• Equiv.Perm.lcm_parts_partition, Equiv.Perm.sign_of_parts_partition: the order and the sign of a permutation, read off the corrected multiset. These are the two invariants that a single exhibited factorization type contributes to the group that exhibits it.
• Equiv.Perm.exists_orderOf_eq_iff: the orders of the permutations of a finite type are exactly the least common multiples of the partitions of its cardinality.
• Equiv.Perm.parts_partition_permCongr: transport along an equivalence α ≃ β of the underlying types leaves it unchanged. Its ingredient Equiv.Perm.cycleType_permCongr is proved here too, since Mathlib records only Equiv.Perm.sign_permCongr. The form for Equiv.permCongrHom, the group isomorphism a relabelling induces, needs no separate lemma: Mathlib's simp lemma Equiv.permCongrHom_coe rewrites it to Equiv.permCongr.
• Equiv.Perm.parts_partition_of_isCycle, Equiv.Perm.parts_partition_swap: the values on a cycle and on a transposition, which are the two shapes the low-degree recognition theorems read.
• Equiv.Perm.cycleType_eq_singleton_iff: a single cycle length n characterizes a cycle moving n points; through Equiv.Perm.filter_fullCycleType_eq_cycleType this reads a cycle off a full cycle type.
• Equiv.Perm.fullCycleType_eq_map_card_filter: the full cycle type is the multiset of orbit sizes, read through any function whose fibres are the orbits.
• Equiv.Perm.orbitQuotientEquivCycleFactorsSumFixedPoints: the classes of Equiv.Perm.SameCycle are the nontrivial cycle factors together with the fixed points, via the point-level map Equiv.Perm.cycleFactorOrFixedPoint.
• Equiv.Perm.fullCycleType_eq_map_card_orbit: the full cycle type is the multiset of the sizes of the orbits of ⟨σ⟩ on the carrier, with Equiv.Perm.sameCycle_iff_mem_orbit_zpowers, Equiv.Perm.coe_support_cycleOf_eq_orbit_zpowers and Equiv.Perm.orbit_zpowers_eq_singleton identifying those orbits with the cycle supports and the fixed points.

Implementation notes

The definition fullCycleType σ below uses the same [Fintype α] [DecidableEq α] arguments as Equiv.Perm.partition, so the invariant is a wrapper around its defining expression. The public pos_of_mem_fullCycleType lemma exposes the positivity of its parts (Nat.Partition.parts_pos), and count_fullCycleType_of_ne_one exposes the non-one count comparison. The filter lemma (Equiv.Perm.filter_parts_partition_eq_cycleType) and the completeness of the conjugacy invariant (Equiv.Perm.partition_eq_of_isConj) remain stated for partition.parts and are available through the defining bridge. Downstream statements use (Equiv.Perm.partition σ).parts, which is a bare Multiset ℕ and so can be compared with a multiset of factor degrees directly; it is the bundled σ.partition, whose type Nat.Partition n is indexed by the ambient cardinality, that cannot.

Since Equiv.Perm.partition takes the DecidableEq α of its carrier as an instance argument and is not noncomputable, the multiset below is written at the carrier's own instance rather than at Classical.propDecidable, which is what the downstream comparison with a factorization type is stated with. The invariant and its API are in the Equiv.Perm namespace, so permutation expressions can use dot notation and the statements sit alongside the partition lemmas they refine.

def Equiv.Perm.fullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : Multiset ℕ

The cycle lengths of σ, including one part for each fixed point.

Unlike Equiv.Perm.cycleType, this is a partition of the cardinality of the whole carrier. It is the permutation-side cycle invariant used to compare a Galois action with factor degrees.

Equations

• σ.fullCycleType = σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1

The two halves of the multiset

@[simp]

theorem Equiv.Perm.count_one_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : Multiset.count 1 σ.partition.parts = Fintype.card α - σ.support.card

The parts of Equiv.Perm.partition equal to one are the fixed points of σ. Together with Equiv.Perm.filter_parts_partition_eq_cycleType, which recovers the cycle lengths, this says that the correction neither gains nor loses information.

@[simp]

theorem Equiv.Perm.count_parts_partition_of_ne_one {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) {n : ℕ} (hn : n ≠ 1) : Multiset.count n σ.partition.parts = Multiset.count n σ.cycleType

At every value other than one, Equiv.Perm.partition counts a part as often as Equiv.Perm.cycleType does.

@[simp]

theorem Equiv.Perm.card_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ.partition.parts.card = σ.cycleType.card + (Fintype.card α - σ.support.card)

The number of parts of Equiv.Perm.partition is the number of cycles of σ of length at least two together with its fixed points.

The correction term

theorem Equiv.Perm.parts_partition_eq_cycleType_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : σ.partition.parts = σ.cycleType ↔ σ.support = Finset.univ

The correction is trivial exactly when the permutation has no fixed point. This is the one place where the parts of Equiv.Perm.partition and Equiv.Perm.cycleType may be exchanged, and the hypothesis is about σ, not about the ambient type.

theorem Equiv.Perm.parts_partition_eq_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (hσ : σ.support = Finset.univ) : σ.partition.parts = σ.cycleType

For a permutation with no fixed point, the parts of Equiv.Perm.partition are Equiv.Perm.cycleType.

Special values

@[simp]

theorem Equiv.Perm.parts_partition_one {α : Type u_1} [Fintype α] [DecidableEq α] : (partition 1).parts = Multiset.replicate (Fintype.card α) 1

The parts of the identity permutation are all one, with one part for each element of the underlying finite type.

@[simp]

theorem Equiv.Perm.parts_partition_eq_replicate_one_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : σ.partition.parts = Multiset.replicate (Fintype.card α) 1 ↔ σ = 1

The identity is the only permutation all of whose parts are one.

theorem Equiv.Perm.parts_partition_of_isCycle {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (hσ : σ.IsCycle) : σ.partition.parts = σ.support.card ::ₘ Multiset.replicate (Fintype.card α - σ.support.card) 1

The cycle type of a cycle, with its fixed points restored.

theorem Equiv.Perm.parts_partition_swap {α : Type u_1} [Fintype α] [DecidableEq α] {x y : α} (hxy : x ≠ y) : (swap x y).partition.parts = 2 ::ₘ Multiset.replicate (Fintype.card α - 2) 1

The cycle type of a transposition, with its fixed points restored: on a type with n points a transposition has parts {2, 1, …, 1} with n - 2 parts equal to one.

@[simp]

theorem Equiv.Perm.parts_partition_of_isEmpty {α : Type u_1} [Fintype α] [DecidableEq α] [IsEmpty α] (σ : Perm α) : σ.partition.parts = 0

On an empty type there is nothing to partition.

@[simp]

theorem Equiv.Perm.parts_partition_eq_zero_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : σ.partition.parts = 0 ↔ Fintype.card α = 0

The parts of Equiv.Perm.partition are empty exactly on an empty type; in particular they do not vanish on the identity of a nonempty type, unlike Equiv.Perm.cycleType.

Conjugacy

@[simp]

theorem Equiv.Perm.parts_partition_conj {α : Type u_1} [Fintype α] [DecidableEq α] (g σ : Perm α) : (g * σ * g⁻¹).partition.parts = σ.partition.parts

The parts of Equiv.Perm.partition are constant on conjugacy classes. This is the unbundled form of Mathlib's Equiv.Perm.partition_eq_of_isConj, which also gives the converse.

@[simp]

theorem Equiv.Perm.parts_partition_inv {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ⁻¹.partition.parts = σ.partition.parts

Inverting a permutation does not change the parts of its partition.

Order and parity

The two invariants that a single exhibited factorization type contributes: the order of the permutation it exhibits, which divides the order of any group containing it, and its sign.

@[simp]

theorem Equiv.Perm.lcm_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ.partition.parts.lcm = orderOf σ

The order of a permutation is the least common multiple of the parts of Equiv.Perm.partition. The parts equal to one contribute nothing, so this agrees with Equiv.Perm.lcm_cycleType; stating it here means that a factorization type can be read as a lower bound on the order of a group directly, without first discarding its fixed points.

theorem Equiv.Perm.dvd_of_mem_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {n : ℕ} (hn : n ∈ σ.partition.parts) : n ∣ orderOf σ

Every part of a permutation's partition divides the order of the permutation.

theorem Equiv.Perm.exists_orderOf_eq_iff {α : Type u_1} [Finite α] {k : ℕ} : (∃ (σ : Perm α), orderOf σ = k) ↔ ∃ (p : (Nat.card α).Partition), p.parts.lcm = k

A finite type carries a permutation of order k exactly when k is the least common multiple of the parts of some partition of its cardinality. A partition is realized by a permutation whose cycles have its parts of size at least two as lengths, by Equiv.Perm.exists_with_cycleType_iff; the parts equal to one do not change the least common multiple.

theorem Equiv.Perm.sign_of_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : sign σ = (-1) ^ (Fintype.card α + σ.partition.parts.card)

The sign of a permutation, read off the parts of Equiv.Perm.partition: it is the parity of the number of parts, corrected by the ambient cardinality. This is Equiv.Perm.sign_of_cycleType in the convention that keeps the fixed points, and the parity invariant of a Galois image is computed from it.

Transport along an equivalence of the underlying types

@[simp]

theorem Equiv.Perm.cycleType_permCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (σ : Perm α) : (e.permCongr σ).cycleType = σ.cycleType

The cycle type of a permutation does not change when the underlying type is relabelled. Mathlib has this for Equiv.Perm.sign as Equiv.Perm.sign_permCongr, and for the extension of a permutation to a larger type as Equiv.Perm.cycleType_extendDomain; relabelling is the case of the latter in which the predicate cut out is True.

@[simp]

theorem Equiv.Perm.card_support_permCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (σ : Perm α) : (e.permCongr σ).support.card = σ.support.card

Relabelling the underlying type does not change the number of points that a permutation moves.

@[simp]

theorem Equiv.Perm.parts_partition_permCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (σ : Perm α) : (e.permCongr σ).partition.parts = σ.partition.parts

The parts of Equiv.Perm.partition are natural in the underlying type: a relabelling e : α ≃ β leaves them unchanged. This is what lets a statement about the roots of a polynomial, which form a type with no chosen numbering, be compared with a statement about Fin n.

The canonical full cycle type API

theorem Equiv.Perm.fullCycleType_def {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ.fullCycleType = σ.partition.parts

fullCycleType is the unbundled parts of Mathlib's permutation partition.

The filter and conjugacy forms of the partition API.

@[simp]

theorem Equiv.Perm.filter_fullCycleType_eq_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : Multiset.filter (fun (n : ℕ) => 2 ≤ n) σ.fullCycleType = σ.cycleType

Filtering the full cycle type to parts of length at least two recovers the cycle type.

@[simp]

theorem Equiv.Perm.cycleType_eq_singleton_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {n : ℕ} : σ.cycleType = {n} ↔ σ.IsCycle ∧ σ.support.card = n

A permutation has a single cycle length n, and no other, exactly when it is a cycle moving n points.

theorem Equiv.Perm.fullCycleType_eq_of_isConj {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : Perm α} (hστ : IsConj σ τ) : σ.fullCycleType = τ.fullCycleType

Conjugate permutations have equal full cycle types.

@[simp]

theorem Equiv.Perm.sum_fullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ.fullCycleType.sum = Fintype.card α

The full cycle lengths of a permutation sum to the cardinality of its carrier.

theorem Equiv.Perm.pos_of_mem_fullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {n : ℕ} (hn : n ∈ σ.fullCycleType) : 0 < n

Every part of a permutation's full cycle type is positive.

@[simp]

theorem Equiv.Perm.count_fullCycleType_of_ne_one {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) {n : ℕ} (hn : n ≠ 1) : Multiset.count n σ.fullCycleType = Multiset.count n σ.cycleType

At every value other than one, fullCycleType counts a part as often as Equiv.Perm.cycleType does.

@[simp]

theorem Equiv.Perm.fullCycleType_one {α : Type u_1} [Fintype α] [DecidableEq α] : fullCycleType 1 = Multiset.replicate (Fintype.card α) 1

The identity has one full cycle-type part for every point of the carrier.

@[simp]

theorem Equiv.Perm.fullCycleType_of_isEmpty {α : Type u_1} [Fintype α] [DecidableEq α] [IsEmpty α] (σ : Perm α) : σ.fullCycleType = 0

On an empty finite carrier, the full cycle type is empty.

@[simp]

theorem Equiv.Perm.fullCycleType_eq_zero_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : σ.fullCycleType = 0 ↔ Fintype.card α = 0

The full cycle type is empty exactly when the carrier is empty.

theorem Equiv.Perm.fullCycleType_eq_cycleType_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} : σ.fullCycleType = σ.cycleType ↔ σ.support = Finset.univ

The full cycle type agrees with the cycle type exactly when there are no fixed points.

theorem Equiv.Perm.fullCycleType_eq_cycleType {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (hσ : σ.support = Finset.univ) : σ.fullCycleType = σ.cycleType

A fixed-point-free permutation has no one-parts in its full cycle type.

@[simp]

theorem Equiv.Perm.fullCycleType_conj {α : Type u_1} [Fintype α] [DecidableEq α] (g σ : Perm α) : (g * σ * g⁻¹).fullCycleType = σ.fullCycleType

Conjugating a permutation does not change its full cycle type.

@[simp]

theorem Equiv.Perm.fullCycleType_inv {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ⁻¹.fullCycleType = σ.fullCycleType

Inverting a permutation does not change its full cycle type.

@[simp]

theorem Equiv.Perm.fullCycleType_permCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (σ : Perm α) : (e.permCongr σ).fullCycleType = σ.fullCycleType

Relabelling the carrier does not change a permutation's full cycle type.

@[simp]

theorem Equiv.Perm.count_one_fullCycleType {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : Multiset.count 1 σ.fullCycleType = Fintype.card α - σ.support.card

The parts equal to one in the full cycle type are precisely the fixed points.

theorem Equiv.Perm.fullCycleType_eq_map_card_filter {α : Type u_1} [Fintype α] [DecidableEq α] {γ : Type u_3} (σ : Perm α) (m : α → γ) (hm : ∀ (x y : α), σ.SameCycle x y ↔ m x = m y) : σ.fullCycleType = Multiset.map (fun (c : γ) => {x : α | m x = c}.card) (Finset.image m Finset.univ).val

The full cycle type lists the sizes of the orbits. If the fibres of m : α → γ are exactly the orbits of σ, then the full cycle type of σ is the multiset of the sizes of those fibres, one for each value of m.

Orbit sizes

theorem Equiv.Perm.sameCycle_iff_mem_orbit_zpowers {α : Type u_1} (σ : Perm α) {x y : α} : σ.SameCycle x y ↔ y ∈ MulAction.orbit (↥(Subgroup.zpowers σ)) x

Two points lie on the same cycle of σ exactly when one is a ⟨σ⟩-translate of the other.

theorem Equiv.Perm.orbitRel_zpowers_apply {α : Type u_1} (σ : Perm α) {x y : α} : (MulAction.orbitRel (↥(Subgroup.zpowers σ)) α) x y ↔ σ.SameCycle x y

The orbit relation of ⟨σ⟩ is the same-cycle relation of σ.

theorem Equiv.Perm.coe_support_cycleOf_eq_orbit_zpowers {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) {x : α} (hx : x ∈ σ.support) : ↑(σ.cycleOf x).support = MulAction.orbit (↥(Subgroup.zpowers σ)) x

The ⟨σ⟩-orbit of a moved point is the support of its cycle.

theorem Equiv.Perm.orbit_zpowers_eq_singleton {α : Type u_1} (σ : Perm α) {x : α} (hx : σ x = x) : MulAction.orbit (↥(Subgroup.zpowers σ)) x = {x}

The ⟨σ⟩-orbit of a fixed point is a singleton.

theorem Equiv.Perm.card_subtype_apply_eq {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : Fintype.card { x : α // σ x = x } = Fintype.card α - σ.support.card

The fixed points of a permutation are the complement of its support.

def Equiv.Perm.cycleFactorOrFixedPoint {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) (x : α) : ↥σ.cycleFactorsFinset ⊕ { x : α // σ x = x }

The cycle factor of a moved point, or the point itself when it is fixed: the point-level map underlying Equiv.Perm.orbitQuotientEquivCycleFactorsSumFixedPoints.

Equations

• σ.cycleFactorOrFixedPoint x = if hx : σ x = x then Sum.inr ⟨x, hx⟩ else Sum.inl ⟨σ.cycleOf x, ⋯⟩

@[simp]

theorem Equiv.Perm.cycleFactorOrFixedPoint_of_apply_eq {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) {x : α} (hx : σ x = x) : σ.cycleFactorOrFixedPoint x = Sum.inr ⟨x, hx⟩

@[simp]

theorem Equiv.Perm.cycleFactorOrFixedPoint_of_apply_ne {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) {x : α} (hx : σ x ≠ x) : σ.cycleFactorOrFixedPoint x = Sum.inl ⟨σ.cycleOf x, ⋯⟩

noncomputable def Equiv.Perm.orbitQuotientEquivCycleFactorsSumFixedPoints {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : Quotient (SameCycle.setoid σ) ≃ ↥σ.cycleFactorsFinset ⊕ { x : α // σ x = x }

The orbits of a permutation are its nontrivial cycle factors together with its fixed points. This is the set-level decomposition underlying the full cycle partition: a nontrivial orbit is sent to the unique member of cycleFactorsFinset, while a singleton orbit is sent to its fixed point.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Equiv.Perm.orbitQuotientEquivCycleFactorsSumFixedPoints_mk {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) (x : α) : σ.orbitQuotientEquivCycleFactorsSumFixedPoints ⟦x⟧ = σ.cycleFactorOrFixedPoint x

theorem Equiv.Perm.fullCycleType_eq_map_card_orbit {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : σ.fullCycleType = Multiset.map (fun (ω : MulAction.orbitRel.Quotient (↥(Subgroup.zpowers σ)) α) => Nat.card ↑ω.orbit) Finset.univ.val

The full cycle type lists the orbit sizes. The full cycle type of σ is the multiset of the sizes of the orbits of ⟨σ⟩ on the carrier: the cycles of length at least two are the orbits of the moved points, and each fixed point is an orbit of size one.

Worked examples

The three shapes that the degree-four recognition theorems read off a factorization type.