The number of orbits of a permutation

A permutation σ of a type α partitions α into the classes of Equiv.Perm.SameCycle σ. This file counts them: TauCeti.orbitCount σ is the cardinality of that quotient. Unlike Equiv.Perm.cycleType, which records only the cycles of length at least two, every fixed point of σ contributes an orbit of its own here.

The file then proves how the count responds to three ways of changing a permutation: adjoining a point, splicing a fixed point into another orbit, and merging two orbits. The first two compare a permutation with one of a different type and are stated to allow that; the third compares two permutations of the same type.

• TauCeti.orbitCount_conj: conjugation does not change the number of orbits.
• TauCeti.orbitCount_mul_comm and Equiv.Perm.sameCycle_mul_comm_iff: the two products σ * τ and τ * σ are conjugate, so they have the same number of orbits, and their cycles correspond under σ.
• TauCeti.orbitCount_prodCongrRight_const: permuting the second factor of a product by the same permutation over every point of the first multiplies the number of orbits by the size of the first factor.
• Equiv.Perm.orbitCount_eq_card_parts_partition: on a finite type, the orbit count is the number of parts in Mathlib's full, fixed-point-aware permutation partition, through the decomposition Equiv.Perm.orbitQuotientEquivCycleFactorsSumFixedPoints of TauCeti.GroupTheory.Perm.Partition.
• TauCeti.orbitCount_eq_one_of_forall_sameCycle: a transitive permutation of a nonempty type has orbit count one.
• Equiv.Perm.orbitCount_le_card: on a finite type, a permutation has at most as many orbits as the type has points, the orbits being the classes of a partition of it.
• Equiv.Perm.card_le_orderOf_mul_orbitCount: conversely, the number of points is at most the order of the permutation times its number of orbits, each orbit length dividing the order.
• Equiv.Perm.sign_eq_neg_one_pow_card_sub_orbitCount: the sign is determined by the parity of the number of points minus the number of orbits.
• TauCeti.orbitCount_add_one_eq_of_semiconj: if σ : Equiv.Perm α is carried by an injection f : α → β to τ : Equiv.Perm β, and f misses exactly one point p of β, then τ has one orbit more than σ — the extra orbit is the fixed point p.
• TauCeti.orbitCount_mul_swap_add_one: multiplying a permutation by a transposition that moves one of its fixed points splices that fixed point into another orbit, so the count drops by one.
• List.IsSwapForest.map transports swap forests along embeddings.
• List.IsSwapForest.orbitCount_mul_add_length: a swap forest of n transpositions removes n orbits from a permutation fixing its inserted endpoints; orbitCount_add_length specializes this to the identity.
• TauCeti.orbitCount_add_one_of_merge: if the orbits of τ are the orbits of σ with the orbit of one point and the orbit of another merged, then τ has one orbit fewer.

Composing TauCeti.orbitCount_add_one_eq_of_semiconj with TauCeti.orbitCount_mul_swap_add_one says that adjoining a point to a permutation and immediately splicing it into an existing orbit leaves the number of orbits unchanged. That composite is the reason this file exists: it is the invariance of the number of components of a link under the stabilization move on braids, in TauCeti/KnotTheory/Markov.lean.

Implementation notes

orbitCount is Nat.card of a Quotient, so it is 0 when the permutation has infinitely many orbits or no orbits at all. The three orbit-addition and orbit-removal results assume only that the quotient of the relevant permutation by Equiv.Perm.SameCycle is finite; conjugation preserves the count without any finiteness assumption.

The two cross-type results, TauCeti.orbitCount_add_one_eq_of_semiconj and TauCeti.orbitCount_mul_swap_add_one, are deduced from one private lemma, orbitCount_add_one_eq_aux, whose input is a map F : α → β carrying the orbits of σ bijectively onto the orbits of τ other than a fixed point p of τ. Its SameCycle hypothesis comes from Mathlib's Equiv.Perm.sameCycle_extendDomain for adjoining a point. For splicing a point into an orbit, a one-step statement is propagated over all integer powers by the private lemma sameCycle_zpow_of_forall_sameCycle_apply. TauCeti.orbitCount_add_one_of_merge does not go through that lemma: it exhibits the orbits of τ as the orbits of σ with one class removed and finishes through Equiv.optionSubtypeNe.

noncomputable def TauCeti.orbitCount {α : Type u_1} (σ : Equiv.Perm α) : ℕ

The number of orbits of the cyclic group generated by a permutation σ, that is, the number of classes of Equiv.Perm.SameCycle σ. Every fixed point of σ is an orbit, so on a finite type this counts the cycles of σ together with its fixed points, whereas Equiv.Perm.cycleType records only the former. Being a Nat.card, it is 0 when there are infinitely many orbits.

Equations

• TauCeti.orbitCount σ = Nat.card (Quotient (Equiv.Perm.SameCycle.setoid σ))

theorem TauCeti.orbitCount_def {α : Type u_1} (σ : Equiv.Perm α) : orbitCount σ = Nat.card (Quotient (Equiv.Perm.SameCycle.setoid σ))

The orbit count is the cardinality of the type of orbits.

@[simp]

theorem TauCeti.orbitCount_one {α : Type u_1} : orbitCount 1 = Nat.card α

Each point of α is its own orbit under the identity permutation.

theorem TauCeti.orbitCount_eq_one_of_forall_sameCycle {α : Type u_1} [Nonempty α] {σ : Equiv.Perm α} (h : ∀ (x y : α), σ.SameCycle x y) : orbitCount σ = 1

A permutation with a single orbit on a nonempty type has orbit count one.

theorem Equiv.Perm.orbitCount_le_card {α : Type u_1} [Finite α] (σ : Perm α) : TauCeti.orbitCount σ ≤ Nat.card α

A permutation of a finite type has at most as many orbits as there are points.

theorem Equiv.Perm.orbitCount_pos {α : Type u_1} [Finite α] [Nonempty α] (σ : Perm α) : 0 < TauCeti.orbitCount σ

A permutation of a finite nonempty type has a positive number of orbits.

@[simp]

theorem TauCeti.orbitCount_conj {α : Type u_1} (g σ : Equiv.Perm α) : orbitCount (g * σ * g⁻¹) = orbitCount σ

Conjugate permutations have the same number of orbits: conjugation by g relabels the points by g, hence relabels the orbits.

theorem Equiv.Perm.sameCycle_mul_comm_iff {α : Type u_1} (σ τ : Perm α) {x y : α} : (τ * σ).SameCycle x y ↔ (σ * τ).SameCycle (σ x) (σ y)

The two products of a pair of permutations are conjugate by either factor, so a pair of points lies in one cycle of τ * σ exactly when their images under σ lie in one cycle of σ * τ.

theorem TauCeti.orbitCount_mul_comm {α : Type u_1} (σ τ : Equiv.Perm α) : orbitCount (σ * τ) = orbitCount (τ * σ)

The two products of a pair of permutations have the same number of orbits, being conjugate by either factor.

@[simp]

theorem Equiv.Perm.orbitCount_inv {α : Type u_1} (σ : Perm α) : TauCeti.orbitCount σ⁻¹ = TauCeti.orbitCount σ

Inverting a permutation does not change its number of orbits.

@[simp]

theorem Equiv.orbitCount_permCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) (σ : Perm α) : TauCeti.orbitCount (e.permCongr σ) = TauCeti.orbitCount σ

Transporting a permutation along an equivalence of its underlying type does not change its number of orbits.

theorem TauCeti.orbitCount_prodCongrRight_const {α : Type u_1} {β : Type u_2} (τ : Equiv.Perm β) : orbitCount (Equiv.prodCongrRight fun (x : α) => τ) = Nat.card α * orbitCount τ

Rotating the second coordinate of α × β by the same permutation τ over every point of α has one copy of each orbit of τ over every point of α.

theorem Equiv.Perm.orbitCount_eq_card_parts_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : TauCeti.orbitCount σ = σ.partition.parts.card

The number of permutation orbits is the number of parts in its full cycle partition. This identifies orbitCount, defined from SameCycle, with Mathlib's fixed-point-aware cycle data.

theorem Equiv.Perm.sign_eq_neg_one_pow_card_sub_orbitCount {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) : sign σ = (-1) ^ (Fintype.card α - TauCeti.orbitCount σ)

The sign of a finite permutation is the parity of the number of points minus the number of orbits. Fixed points contribute once to both numbers and hence do not affect the sign.

theorem Equiv.Perm.card_le_orderOf_mul_orbitCount {α : Type u_1} [Finite α] (σ : Perm α) : Nat.card α ≤ orderOf σ * TauCeti.orbitCount σ

A permutation of a finite type has at least Nat.card α / orderOf σ orbits: every orbit has length dividing the order of σ, so at most orderOf σ points.

theorem TauCeti.orbitCount_add_one_eq_of_semiconj {α : Type u_1} {β : Type u_2} {f : α → β} {p : β} {σ : Equiv.Perm α} {τ : Equiv.Perm β} [Finite (Quotient (Equiv.Perm.SameCycle.setoid τ))] (hf : Function.Injective f) (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) : orbitCount σ + 1 = orbitCount τ

Adjoining a fixed point adds one orbit. If an injection f : α → β intertwines σ : Equiv.Perm α with τ : Equiv.Perm β and its image is the complement of a single point p, then p is a fixed point of τ and is the only orbit of τ that is not an orbit of σ.

theorem TauCeti.orbitCount_mul_swap_add_one {β : Type u_2} [DecidableEq β] {τ : Equiv.Perm β} [Finite (Quotient (Equiv.Perm.SameCycle.setoid τ))] {p a : β} (hp : τ p = p) (hne : a ≠ p) : orbitCount (τ * Equiv.swap a p) + 1 = orbitCount τ

Splicing a fixed point into another orbit removes one orbit. If τ fixes p and a ≠ p, then in τ * Equiv.swap a p the point p has joined the orbit of a, and no other orbit has changed.

def List.IsSwapForest {β : Type u_2} [DecidableEq β] : List (β × β) → Prop

A list of transpositions [(a₁, p₁), …, (aₙ, pₙ)] is a swap forest if each factor Equiv.swap aᵢ pᵢ moves a point pᵢ ≠ aᵢ that the product of the later factors still fixes. The head of the list is the rightmost factor of the product (factors.reverse.map (Function.uncurry Equiv.swap)).prod, so each factor splices a fixed point into another orbit, as in TauCeti.orbitCount_mul_swap_add_one.

Equations

• [].IsSwapForest = True
• ((a, p) :: factors).IsSwapForest = (factors.IsSwapForest ∧ (List.map (Function.uncurry Equiv.swap) factors.reverse).prod p = p ∧ a ≠ p)

@[simp]

theorem List.isSwapForest_nil {β : Type u_2} [DecidableEq β] : [].IsSwapForest

The empty list of transpositions is a swap forest.

@[simp]

theorem List.isSwapForest_cons {β : Type u_2} [DecidableEq β] (a p : β) (factors : List (β × β)) : ((a, p) :: factors).IsSwapForest ↔ factors.IsSwapForest ∧ (map (Function.uncurry Equiv.swap) factors.reverse).prod p = p ∧ a ≠ p

Unfolding List.IsSwapForest at a cons: the tail is a swap forest and the new factor moves a point p ≠ a fixed by the product of the tail.

theorem List.IsSwapForest.map {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {factors : List (β × β)} (hforest : factors.IsSwapForest) (e : β ↪ γ) : (List.map (fun (factor : β × β) => (e factor.1, e factor.2)) factors).IsSwapForest

Embedding the endpoints of a swap forest preserves the forest property.

theorem List.IsSwapForest.orbitCount_mul_add_length {β : Type u_2} [DecidableEq β] [Finite β] {factors : List (β × β)} (hforest : factors.IsSwapForest) (τ : Equiv.Perm β) (hfix : ∀ factor ∈ factors, τ factor.2 = factor.2) : TauCeti.orbitCount (τ * (List.map (Function.uncurry Equiv.swap) factors.reverse).prod) + factors.length = TauCeti.orbitCount τ

A swap forest splices fixed points into a permutation. If the permutation fixes the second endpoint of every factor, multiplying by the forest removes one orbit per factor.

theorem List.IsSwapForest.orbitCount_add_length {β : Type u_2} [DecidableEq β] [Finite β] {factors : List (β × β)} (hforest : factors.IsSwapForest) : TauCeti.orbitCount (List.map (Function.uncurry Equiv.swap) factors.reverse).prod + factors.length = Nat.card β

A swap forest removes one orbit per factor. The product of a swap forest of n transpositions on a finite type has n orbits fewer than the identity.

theorem List.IsSwapForest.orbitCount_prod_mul_add_length {β : Type u_2} [DecidableEq β] [Finite β] {factors : List (β × β)} (hforest : factors.IsSwapForest) (τ : Equiv.Perm β) (hfix : ∀ factor ∈ factors, τ factor.2 = factor.2) : TauCeti.orbitCount ((List.map (Function.uncurry Equiv.swap) factors).prod * τ) + factors.length = TauCeti.orbitCount τ

A swap forest splices fixed points on the left. If a permutation fixes the second endpoint of every factor, multiplying by the factors in their listed order removes one orbit per factor.

theorem TauCeti.orbitCount_add_one_of_merge {α : Type u_1} {σ τ : Equiv.Perm α} [Finite (Quotient (Equiv.Perm.SameCycle.setoid σ))] {a b : α} (hle : ∀ {u v : α}, σ.SameCycle u v → τ.SameCycle u v) (hmerge : ∀ {u v : α}, τ.SameCycle u v → σ.SameCycle u v ∨ (σ.SameCycle u a ∨ σ.SameCycle u b) ∧ (σ.SameCycle v a ∨ σ.SameCycle v b)) (hab : τ.SameCycle a b) (hnab : ¬σ.SameCycle a b) : orbitCount τ + 1 = orbitCount σ

Merging two orbits removes one orbit. If every orbit of σ is contained in an orbit of τ, if two points a and b lying in different orbits of σ lie in one orbit of τ, and if no orbit of τ merges more than those two, then τ has exactly one orbit fewer than σ. The last hypothesis is the honest content: without it nothing stops τ from gluing the orbits of σ wholesale.