Orbit bijections when inserting a point into a cycle

Adjoin one fixed point to a permutation, then transpose it with an old point. The old cycles survive, with the new point inserted into the cycle of its transposition partner. The resulting orbit bijection sends every old point to its own image, rather than choosing an arbitrary bijection from an equality of orbit counts. This permits transport of data attached to individual cycles, such as the framing coefficients of a braid closure.

The construction uses Mathlib's cycle quotient and Tau Ceti's transposition merge theorem Equiv.Perm.SameCycle.sameCycle_or_of_swap_mul.

theorem Equiv.Perm.sameCycle_mul_swap_iff_of_apply_eq_self {β : Type u_2} [DecidableEq β] {τ : Perm β} {p a x y : β} (hp : τ p = p) (hxp : x ≠ p) (hyp : y ≠ p) : (τ * swap a p).SameCycle x y ↔ τ.SameCycle x y

Splicing a fixed point p into the cycle of a preserves the cycle relation between points other than p. No finiteness or periodicity is required.

theorem Equiv.Perm.sameCycle_mul_swap_iff_of_apply_eq {β : Type u_2} [DecidableEq β] {σ : Perm β} {p m u v : β} (hσp : σ p = m) (hu : u ≠ m) (hv : v ≠ m) : (σ * swap p m).SameCycle u v ↔ σ.SameCycle u v

Removing a point m from its cycle σ p = m by σ * swap p m does not change the cycle relation between points other than m.

theorem Equiv.Perm.apply_eq_self_of_semiconj {α : Type u_1} {β : Type u_2} {σ : Perm α} {τ : Perm β} {f : α → β} {p : β} (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) : τ p = p

A permutation extending another across a single missing point fixes that point.

noncomputable def Equiv.Perm.orbitQuotientEquivSplice {α : Type u_1} {β : Type u_2} [DecidableEq β] (σ : Perm α) (τ : Perm β) (f : α → β) (p : β) (a : α) (hf : Function.Injective f) (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) : Quotient (SameCycle.setoid σ) ≃ Quotient (SameCycle.setoid (τ * swap (f a) p))

Insert a new point into the orbit of a, after extending σ along an injection f whose image misses exactly that point. The orbit bijection follows f on old points.

@[simp]

theorem Equiv.Perm.orbitQuotientEquivSplice_mk {α : Type u_1} {β : Type u_2} [DecidableEq β] (σ : Perm α) (τ : Perm β) (f : α → β) (p : β) (a : α) (hf : Function.Injective f) (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) (x : α) : (σ.orbitQuotientEquivSplice τ f p a hf hfp hsurj hcomm) ⟦x⟧ = ⟦f x⟧

On old points the orbit bijection is the given inclusion.

@[simp]

theorem Equiv.Perm.orbitQuotientEquivSplice_symm_mk {α : Type u_1} {β : Type u_2} [DecidableEq β] (σ : Perm α) (τ : Perm β) (f : α → β) (p : β) (a : α) (hf : Function.Injective f) (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) (x : α) : (σ.orbitQuotientEquivSplice τ f p a hf hfp hsurj hcomm).symm ⟦f x⟧ = ⟦x⟧

The inverse orbit bijection sends an old point back to its original orbit.

@[simp]

theorem Equiv.Perm.orbitQuotientEquivSplice_symm_mk_new {α : Type u_1} {β : Type u_2} [DecidableEq β] (σ : Perm α) (τ : Perm β) (f : α → β) (p : β) (a : α) (hf : Function.Injective f) (hfp : ∀ (x : α), f x ≠ p) (hsurj : ∀ (y : β), y ≠ p → ∃ (x : α), f x = y) (hcomm : Function.Semiconj f ⇑σ ⇑τ) : (σ.orbitQuotientEquivSplice τ f p a hf hfp hsurj hcomm).symm ⟦p⟧ = ⟦a⟧

The inserted point belongs to the orbit of its old transposition partner.