Executable full cycle types

This file gives an executable decomposition of a permutation of a finite linearly ordered type. For a point i, Equiv.Perm.cycleLenOf σ i counts the points in its cycle. A point is the canonical representative of its cycle when it is the least point in that cycle, and Equiv.Perm.computedCycleType σ lists cycleLenOf σ i over those representatives.

The main theorem Equiv.Perm.computedCycleType_eq_fullCycleType identifies this finite search with Equiv.Perm.fullCycleType, the canonical full cycle partition. Thus computations use only decidable finite predicates, while mathematical statements can continue to use the canonical partition API.

Main definitions

• Equiv.Perm.cycleLenOf: the length of the cycle containing a point, computed as the size of its orbit Finset.orbitFinset {σ} i.
• Equiv.Perm.IsCycleMin: the predicate that a point is the least point of its cycle.
• Equiv.Perm.computedCycleType: the multiset of cycle lengths at the cycle minima.

Main result

• Equiv.Perm.computedCycleType_eq_fullCycleType: the computed and canonical full cycle types agree.

References

• S. K. Lando and A. K. Zvonkin, Graphs on Surfaces and Their Applications, §1.5.

theorem Equiv.Perm.mem_orbitFinset_singleton_iff_sameCycle {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {i j : α} : j ∈ {σ}.orbitFinset i ↔ σ.SameCycle i j

A point lies in the computed orbit Finset.orbitFinset {σ} i exactly when it lies in the cycle of σ containing i.

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

The length of the cycle of σ containing i, computed as the size of the orbit of i under σ.

Equations

• σ.cycleLenOf i = ({σ}.orbitFinset i).card

@[simp]

theorem Equiv.Perm.cycleLenOf_pos {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) (i : α) : 0 < σ.cycleLenOf i

The computed cycle length is positive.

theorem Equiv.Perm.cycleLenOf_eq_of_sameCycle {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {i j : α} (hij : σ.SameCycle i j) : σ.cycleLenOf i = σ.cycleLenOf j

Points in the same cycle have the same computed cycle length.

theorem Equiv.Perm.cycleLenOf_eq_minimalPeriod {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Perm α) (i : α) : σ.cycleLenOf i = Function.minimalPeriod (⇑σ) i

The executable cycle length agrees with the abstract minimal period of the point.

@[simp]

theorem Equiv.Perm.cycleLenOf_eq_one_iff {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} {i : α} : σ.cycleLenOf i = 1 ↔ σ i = i

The cycle of a point has length one exactly when the point is fixed.

def Equiv.Perm.cycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) (i : α) : α

The least point in the cycle of i. This is an executable canonical representative.

Equations

• σ.cycleMin i = ({σ}.orbitFinset i).min' ⋯

theorem Equiv.Perm.sameCycle_cycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) (i : α) : σ.SameCycle i (σ.cycleMin i)

The least representative of a cycle belongs to that cycle.

theorem Equiv.Perm.cycleMin_le_of_sameCycle {α : Type u_1} [Fintype α] [LinearOrder α] {σ : Perm α} {i j : α} (hij : σ.SameCycle i j) : σ.cycleMin i ≤ j

The canonical representative is no larger than any point in its cycle.

@[simp]

theorem Equiv.Perm.cycleMin_eq_cycleMin_iff {α : Type u_1} [Fintype α] [LinearOrder α] {σ : Perm α} {i j : α} : σ.cycleMin i = σ.cycleMin j ↔ σ.SameCycle i j

Two points have the same canonical representative exactly when they lie in the same cycle.

def Equiv.Perm.IsCycleMin {α : Type u_1} [LinearOrder α] (σ : Perm α) (i : α) : Prop

A point is a cycle minimum when it is no larger than every point in its cycle.

Equations

• σ.IsCycleMin i = ∀ (j : α), σ.SameCycle i j → i ≤ j

@[instance_reducible]

instance Equiv.Perm.decidableIsCycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) (i : α) : Decidable (σ.IsCycleMin i)

Equations

• σ.decidableIsCycleMin i = decidable_of_iff (∀ (j : α), σ.SameCycle i j → i ≤ j) ⋯

@[simp]

theorem Equiv.Perm.cycleMin_eq_self_iff {α : Type u_1} [Fintype α] [LinearOrder α] {σ : Perm α} {i : α} : σ.cycleMin i = i ↔ σ.IsCycleMin i

A point is the least point of its cycle exactly when it is its canonical representative.

@[simp]

theorem Equiv.Perm.cycleMin_cycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) (i : α) : σ.cycleMin (σ.cycleMin i) = σ.cycleMin i

Taking the cycle minimum is idempotent.

@[simp]

theorem Equiv.Perm.isCycleMin_cycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) (i : α) : σ.IsCycleMin (σ.cycleMin i)

The canonical representative is a cycle minimum.

theorem Equiv.Perm.image_cycleMin {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) : Finset.image σ.cycleMin Finset.univ = Finset.filter σ.IsCycleMin Finset.univ

The image of the cycle-minimum map is exactly the finset of cycle minima.

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

The full cycle type computed by listing the length at the least point of every cycle.

Equations

• σ.computedCycleType = Multiset.map σ.cycleLenOf (Finset.filter σ.IsCycleMin Finset.univ).val

@[simp]

theorem Equiv.Perm.computedCycleType_eq_fullCycleType {α : Type u_1} [Fintype α] [LinearOrder α] (σ : Perm α) : σ.computedCycleType = σ.fullCycleType

The executable cycle decomposition agrees with the canonical full cycle type.