Doubling the points of a finite permutation

Equiv.Perm.doubled replaces every point of a cycle by two successive points. Its orbit quotient includes singleton cycles of the original permutation. These finite permutation identities are original and do not assert a geometric realization.

Main definitions

• Equiv.Perm.doubled: replaces each point by two consecutive points.
• Equiv.Perm.doubledOrbitEquiv: complete doubled/original orbit correspondence.
• Equiv.Perm.sumOrbitEquiv: complete disjoint-sum orbit decomposition.

Main results

• Equiv.Perm.SameCycle.map_of_semiconj: maps finite permutation orbits.
• Equiv.Perm.sameCycle_equiv_iff: changes orbit coordinates by an equivalence.
• Equiv.Perm.sameCycle_doubled: doubling preserves the original orbit partition.

theorem Equiv.Perm.SameCycle.map_of_semiconj {α : Type u_1} {β : Type u_2} [Finite α] {f : Perm α} {g : Perm β} {u : α → β} (h : Function.Semiconj u ⇑f ⇑g) {x y : α} (hxy : f.SameCycle x y) : g.SameCycle (u x) (u y)

A semiconjugacy maps an entire finite permutation orbit into one orbit.

theorem Equiv.Perm.sameCycle_equiv_iff {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (e : α ≃ β) (f : Perm α) (g : Perm β) (h : ∀ (x : α), e (f x) = g (e x)) (x y : α) : g.SameCycle (e x) (e y) ↔ f.SameCycle x y

An explicit change of coordinates preserves all permutation orbits.

def Equiv.Perm.doubled {α : Type u_1} (f : Perm α) : Perm (α × Bool)

Replace each point x by the consecutive block (x,false), (x,true).

@[simp]

theorem Equiv.Perm.doubled_squared {α : Type u_1} (f : Perm α) (x : α) : f.doubled (f.doubled (x, false)) = (f x, false)

The square on the first point of each block is the original permutation.

theorem Equiv.Perm.sameCycle_doubled {α : Type u_1} [Finite α] (f : Perm α) (x y : α × Bool) : f.doubled.SameCycle x y ↔ f.SameCycle x.1 y.1

Doubling changes cycle lengths but leaves the full orbit partition unchanged.

def Equiv.Perm.doubledOrbitEquiv {α : Type u_1} [Finite α] (f : Perm α) : Quotient (SameCycle.setoid f.doubled) ≃ Quotient (SameCycle.setoid f)

All doubled orbits, with no omission of fixed points, correspond to original orbits.

def Equiv.Perm.sumOrbitEquiv {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (f : Perm α) (g : Perm β) : Quotient (SameCycle.setoid (Equiv.sumCongr f g)) ≃ Quotient (SameCycle.setoid f) ⊕ Quotient (SameCycle.setoid g)

All orbits of a permutation on a disjoint sum split into the two orbit quotients.