Inserting a point in a permutation cycle

Equiv.Perm.Insertion.insertAfter inserts an optional point immediately after a chosen point. Exact successor equations, complete orbit correspondence and the removeNone inverse include singleton cycles. The results are about arbitrary permutations and have no graph dependency or geometric hypothesis.

def Equiv.Perm.Insertion.insertAfter {α : Type} [DecidableEq α] (f : Perm α) (h : α) : Perm (Option α)

Insert none after h in the cycle of f, preserving every other successor.

@[simp]

theorem Equiv.Perm.Insertion.insertAfter_at {α : Type} [DecidableEq α] (f : Perm α) (h : α) : (insertAfter f h) (some h) = none

The chosen old dart leads to the inserted dart.

@[simp]

theorem Equiv.Perm.Insertion.insertAfter_none {α : Type} [DecidableEq α] (f : Perm α) (h : α) : (insertAfter f h) none = some (f h)

The inserted dart leads to the old successor of its corner.

theorem Equiv.Perm.Insertion.insertAfter_other {α : Type} [DecidableEq α] (f : Perm α) (h a : α) (ha : a ≠ h) : (insertAfter f h) (some a) = some (f a)

All other old successors remain literally unchanged.

def Equiv.Perm.Insertion.collapse {α : Type} (h : α) : Option α → α

Collapse just the inserted dart to its preceding corner.

theorem Equiv.Perm.Insertion.sameCycle_iff {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h : α) (x y : Option α) : (insertAfter f h).SameCycle x y ↔ f.SameCycle (collapse h x) (collapse h y)

Insertion preserves exactly the old cycles, and places the new dart in the corner's cycle. This includes singleton cycles and makes no distinct-vertex assumption.

noncomputable def Equiv.Perm.Insertion.orbitEquiv {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h : α) : Quotient (SameCycle.setoid (insertAfter f h)) ≃ Quotient (SameCycle.setoid f)

Every cycle, including a fixed point, survives insertion exactly once.

theorem Equiv.Perm.Insertion.card_orbits_insertAfter {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h : α) : Nat.card (Quotient (SameCycle.setoid (insertAfter f h))) = Nat.card (Quotient (SameCycle.setoid f))

The number of all cycles is unchanged by inserting a dart in an existing cycle.

theorem Equiv.Perm.Insertion.insertAfter_removeNone {α : Type} [DecidableEq α] (f : Perm (Option α)) (h : α) (hh : f (some h) = none) : insertAfter (removeNone f) h = f

Deleting a non-singleton dart and reinserting it after its predecessor recovers the literal permutation, including its orientation. removeNone is Mathlib's deletion.

theorem Equiv.Perm.Insertion.sameCycle_removeNone_iff {α : Type} [Finite α] (f : Perm (Option α)) (hn : f none ≠ none) (a b : α) : SameCycle (removeNone f) a b ↔ f.SameCycle (some a) (some b)

Removing a dart from a cycle of length at least two preserves all remaining orbit identifications; the two adjacent successors are joined with their original direction.

theorem Equiv.Perm.Insertion.card_orbits_removeNone {α : Type} [Finite α] (f : Perm (Option α)) (hn : f none ≠ none) : Nat.card (Quotient (SameCycle.setoid (removeNone f))) = Nat.card (Quotient (SameCycle.setoid f))

Deleting a non-singleton dart preserves the total number of faces or vertex cycles.

theorem Equiv.Perm.Insertion.insertAfter_twice {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : insertAfter (insertAfter f h) (some k) = (optionCongr f).optionCongr * swap (some (some h)) (some none) * swap (some (some k)) none

Inserting two points gives the two literal outgoing-successor swaps.