Transpositions and the number of orbits #
Multiplying a permutation σ of a finite type by the transposition Equiv.swap a b of two
distinct points either merges the orbit of a with the orbit of b, or splits the single orbit
carrying both of them in two. The number of orbits therefore changes by exactly one, and which way
is decided by Equiv.Perm.SameCycle σ a b:
TauCeti.orbitCount_swap_mul_add_one_of_not_sameCycle, the merging step; its hypothesis¬ Equiv.Perm.SameCycle σ a balready forcesa ≠ b, since a point shares its own orbit;TauCeti.orbitCount_swap_mul_of_sameCycle, the splitting step, which asks fora ≠ bexplicitly.
The degenerate case a = b falls outside that dichotomy: Equiv.swap a a is the identity, so the
number of orbits is unchanged, and Equiv.Perm.SameCycle σ a b, which then holds, decides nothing.
Iterating the two steps measures how many transpositions it takes to build σ: every
factorization of σ into transpositions has at least Nat.card α - TauCeti.orbitCount σ factors
(TauCeti.card_le_orbitCount_add_length), and one with exactly that many exists
(Equiv.Perm.exists_isSwap_list_prod_eq_and_orbitCount_add_length_eq_card), so that number is
the reflection length of σ (Equiv.Perm.isLeast_card_sub_orbitCount). More generally,
TauCeti.card_add_orbitCount_le_length_add_two_mul_card_orbits sharpens the lower bound by
retaining the orbit count of their product and the number of orbits generated by the factors;
TauCeti.card_add_orbitCount_le_length_add_two is its transitive specialization.
Both steps rest on a description of the orbits of the product:
Equiv.Perm.SameCycle.sameCycle_or_of_swap_mul says that two points sharing an orbit of
Equiv.swap a b * σ either shared an orbit of σ already, or were attached one to a and the
other to b. That containment needs no hypothesis at all; what the two orbit-relation statements
TauCeti.sameCycle_swap_mul_of_mem_periodicPts_of_not_sameCycle and
TauCeti.not_sameCycle_swap_mul_of_mem_periodicPts_of_ne_of_sameCycle do need is that the orbit
being walked round comes back to its starting point, that is, that the relevant point is periodic
for σ. Every point of a finite type is periodic (Function.Injective.mem_periodicPts), which is
how the orbit-count steps below supply that.
⚠ That periodicity is essential rather than a convenience. For the shift on two disjoint copies of
ℤ, with a and b the two origins, the product Equiv.swap a b * σ cuts both lines and
reconnects them into two lines again, so the two orbits do not merge.
TauCeti.orbitCount_mul_swap_add_one in TauCeti/GroupTheory/Perm/OrbitCount/Basic.lean is the
specialized fixed-point formulation of the right-multiplication merging step: the transposition
splices that one-point orbit into another one. The generalized step lemmas below assume only
finiteness of the relevant orbit quotient together with an explicit periodic-point hypothesis;
their @[simp] corollaries assume that the underlying type is finite.
Source #
Equiv.Perm.exists_isSwap_list_prod_eq_and_orbitCount_add_length_eq_card returns the list that
Mathlib's Equiv.Perm.swapFactors builds by the recursion of Equiv.Perm.swapFactorsAux in
Mathlib/GroupTheory/Perm/Sign.lean, and measures it: that list L satisfies
TauCeti.orbitCount σ + L.length = Nat.card α. With the lower bound
TauCeti.card_le_orbitCount_add_length this makes Nat.card α - TauCeti.orbitCount σ the
reflection length of σ, so that an induction along a minimal factorization, as in
Euler-characteristic bounds for products of permutations, changes the number of orbits by exactly
one at each step.
Multiplying by a transposition can only merge the orbits of its two points. Two points in
one orbit of Equiv.swap a b * σ either lie in one orbit of σ already, or one of them is joined
to a and the other to b.
Once a and b share an orbit of Equiv.swap a b * σ — the receiver hab — every orbit of
σ is contained in an orbit of that product.
Multiplying by a transposition merges the orbits of its two points. If a and b lie in
different orbits of σ, and b is a periodic point of σ, they lie in one orbit of
Equiv.swap a b * σ: following the orbit of b right round, the product diverts its closing step
to a.
Multiplying by a transposition splits the orbit of its two points. If a ≠ b lie in one
orbit of σ, and a is a periodic point of σ, they lie in different orbits of
Equiv.swap a b * σ: the product closes the arc from a to b into an orbit of its own, which
b is not on.
The transposition step lemma, merging, for a finite set of orbits. If a and b lie in
different orbits of σ, the orbit set of σ is finite, and b is periodic, then
Equiv.swap a b * σ has one orbit fewer than σ.
The transposition step lemma, merging. If a and b lie in different orbits of σ, then
Equiv.swap a b * σ has one orbit fewer than σ: its orbits are those of σ, with the orbit of
a and the orbit of b merged.
The transposition step lemma, splitting, for a finite set of resulting orbits. If a ≠ b
lie in one orbit of σ, a is periodic for σ, and the orbit set of
Equiv.swap a b * σ is finite, then that product has one orbit more than σ.
The transposition step lemma, splitting. If a ≠ b lie in one orbit of σ, then
Equiv.swap a b * σ has one orbit more than σ: that orbit has been cut in two.
Multiplying on the left by a transposition removes at most one orbit, whichever of the two steps applies.
The transposition step lemma on the other side, merging, for a finite set of orbits. If
a and b lie in different orbits of σ, the orbit set of σ is finite, and b is periodic,
then σ * Equiv.swap a b has one orbit fewer than σ.
The transposition step lemma on the other side, merging. If a and b lie in different
orbits of σ, then multiplying on the right merges those two orbits just as multiplying on the
left does, so σ * Equiv.swap a b has one orbit fewer than σ:
orbitCount (σ * Equiv.swap a b) + 1 = orbitCount σ.
The transposition step lemma on the other side, splitting, for a finite set of resulting
orbits. If a ≠ b lie in one orbit of σ, a is periodic for σ, and the orbit set of
σ * Equiv.swap a b is finite, then that product has one orbit more than σ.
The transposition step lemma on the other side, splitting. If a ≠ b lie in one orbit of
σ, then multiplying on the right cuts that orbit in two just as multiplying on the left does, so
σ * Equiv.swap a b has one orbit more than σ:
orbitCount (σ * Equiv.swap a b) = orbitCount σ + 1.
Multiplying on the right by a transposition removes at most one orbit, the mirror of
Equiv.Perm.orbitCount_le_orbitCount_swap_mul_add_one.
A permutation other than the identity has fewer orbits than there are points: the two ends of one of its nontrivial steps share an orbit.
No factorization into transpositions is shorter than the reflection length. Every
factorization of a permutation into transpositions has at least Nat.card α - orbitCount factors,
because each factor removes at most one orbit from the Nat.card α orbits of the identity.
Hurwitz's transposition bound, componentwise. If L is a list of transpositions,
the number of points plus the number of cycles of its product is at most the length of L
plus twice the number of orbits of the group generated by L.
This is the disconnected form of TauCeti.card_add_orbitCount_le_length_add_two: each orbit
of the generated group is one connected component of the transposition graph.
Hurwitz's transposition bound. If a list of transpositions generates a group acting
transitively on a finite type, its length is at least the number of points plus the number of
cycles of its product, minus two. Equivalently,
Nat.card α + orbitCount L.prod ≤ L.length + 2.
A factorization into transpositions of exactly the reflection length exists. Splitting off
the transposition Equiv.swap x (σ x) adds one orbit, so after Nat.card α - orbitCount σ such
steps the identity is reached.
The reflection length of a permutation of a finite type. The least number of transpositions
whose product is σ is Nat.card α - orbitCount σ.