Representatives of the orbits of a permutation

For the periodic gauge (Lemma A.1) the arms of a star are permuted by the twist θ; we solve the gauge equations on one arm of each orbit and transport them. For a permutation θ of a finite linearly ordered type we fix the least element rep i of the orbit of i, an exponent ord i with θ^{ord i} (rep i) = i, and the minimal period per i of rep i; exponents reaching the same point differ by a multiple of the period.

def MultiplicativeBasisDeformations.OrbitReps.rep {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : α

The least element of the orbit.

theorem MultiplicativeBasisDeformations.OrbitReps.sameCycle_rep {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : θ.SameCycle i (rep θ i)

theorem MultiplicativeBasisDeformations.OrbitReps.rep_eq_of_sameCycle {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) {i i' : α} (h : θ.SameCycle i i') : rep θ i = rep θ i'

theorem MultiplicativeBasisDeformations.OrbitReps.rep_apply {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : rep θ (θ i) = rep θ i

theorem MultiplicativeBasisDeformations.OrbitReps.exists_ord {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : ∃ (n : ℕ), (θ ^ n) (rep θ i) = i

noncomputable def MultiplicativeBasisDeformations.OrbitReps.ord {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : ℕ

An exponent reaching i from its representative.

theorem MultiplicativeBasisDeformations.OrbitReps.pow_ord {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : (θ ^ ord θ i) (rep θ i) = i

noncomputable def MultiplicativeBasisDeformations.OrbitReps.per {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : ℕ

The period of the orbit.

theorem MultiplicativeBasisDeformations.OrbitReps.per_pos {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : 0 < per θ i

theorem MultiplicativeBasisDeformations.OrbitReps.pow_per {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : (θ ^ per θ i) (rep θ i) = rep θ i

theorem MultiplicativeBasisDeformations.OrbitReps.per_apply {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : per θ (θ i) = per θ i

theorem MultiplicativeBasisDeformations.OrbitReps.per_dvd_sub {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) {i : α} {a b : ℕ} (h : (θ ^ a) (rep θ i) = (θ ^ b) (rep θ i)) : ↑(per θ i) ∣ ↑a - ↑b

Exponents reaching the same point differ by a multiple of the period.

theorem MultiplicativeBasisDeformations.OrbitReps.ord_apply {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : ↑(per θ i) ∣ ↑(ord θ i) + 1 - ↑(ord θ (θ i))

The exponent of θ i is that of i plus one, up to the period.

theorem MultiplicativeBasisDeformations.OrbitReps.ord_rep {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : ord θ (rep θ i) = 0

theorem MultiplicativeBasisDeformations.OrbitReps.rep_rep {α : Type u_1} [Fintype α] [DecidableEq α] [LinearOrder α] (θ : Equiv.Perm α) (i : α) : rep θ (rep θ i) = rep θ i