Complete orbit counts for permutation surgery

The orbit quotients count singleton cycles. Removing an isolated permutation point drops one orbit; removing a point from a longer cycle preserves its orbit. The identities retain the directed successor convention and serve face-cycle accounting for rotation surgery.

noncomputable def Equiv.Perm.CycleSurgery.optionOrbitEquiv {α : Type} [Finite α] (f : Perm α) : Quotient (SameCycle.setoid (optionCongr f)) ≃ Option (Quotient (SameCycle.setoid f))

Adding a fixed permutation point adds one actual orbit, including when all old points are absent. The old nontrivial and singleton cycles are both retained.

theorem Equiv.Perm.CycleSurgery.card_orbits_optionCongr {α : Type} [Finite α] (f : Perm α) : Nat.card (Quotient (SameCycle.setoid (optionCongr f))) = Nat.card (Quotient (SameCycle.setoid f)) + 1

The additional singleton orbit is counted exactly once.

theorem Equiv.Perm.CycleSurgery.card_orbits_removeNone_fixed {α : Type} [Finite α] (f : Perm (Option α)) (hn : f none = none) : Nat.card (Quotient (SameCycle.setoid f)) = Nat.card (Quotient (SameCycle.setoid (removeNone f))) + 1

Removing a fixed point removes its one singleton orbit; it does not discard any other fixed points or faces.

theorem Equiv.Perm.CycleSurgery.sameCycle_removeNone {α : Type} [Finite α] (f : Perm (Option α)) (a b : α) : SameCycle (removeNone f) a b ↔ f.SameCycle (some a) (some b)

Deleting a permutation point preserves the orbit relation on every retained pair, whether the deleted point was a singleton or belonged to a longer cycle.

theorem Equiv.Perm.CycleSurgery.removeNone_mul_swap {α : Type} [DecidableEq α] (f : Perm (Option α)) (a b : α) : removeNone (f * swap (some a) (some b)) = removeNone f * swap a b

Deletion commutes with swapping the outgoing successors of two retained points. The removed point is fixed by the swap, but may lie anywhere in the original permutation.

theorem Equiv.Perm.CycleSurgery.removeNone_mul_optionCongr {α : Type} (f : Perm (Option α)) (g : Perm α) : removeNone (f * optionCongr g) = removeNone f * g

Deleting the extra point commutes with postcomposition by a permutation of the retained points. The extra point need not be fixed by the first permutation.

theorem Equiv.Perm.CycleSurgery.card_orbits_permCongr {α : Type} [Finite α] {β : Type} [Finite β] (e : α ≃ β) (f : Perm α) : Nat.card (Quotient (SameCycle.setoid (e.permCongr f))) = Nat.card (Quotient (SameCycle.setoid f))

Transporting a permutation retains its complete orbit count.

theorem Equiv.Perm.CycleSurgery.card_orbits_removeNone_add {α : Type} [Finite α] (f : Perm (Option α)) : Nat.card (Quotient (SameCycle.setoid f)) = Nat.card (Quotient (SameCycle.setoid (removeNone f))) + if f none = none then 1 else 0

Deleting a point drops exactly its singleton orbit when it is fixed.

theorem Equiv.Perm.CycleSurgery.card_orbits_removeNone_balance {α : Type} [Finite α] (f : Perm (Option α)) (g : Perm α) : Nat.card (Quotient (SameCycle.setoid (f * optionCongr g))) + Nat.card (Quotient (SameCycle.setoid (removeNone f))) = Nat.card (Quotient (SameCycle.setoid f)) + Nat.card (Quotient (SameCycle.setoid (removeNone (f * optionCongr g))))

A permutation of retained points does not affect the number of singleton orbits lost by deleting the extra point. All counts use the full orbit quotient.

theorem Equiv.Perm.CycleSurgery.card_orbits_mul_swap {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (a b : α) (hab : a ≠ b) : (f.SameCycle a b → Nat.card (Quotient (SameCycle.setoid (f * swap a b))) = Nat.card (Quotient (SameCycle.setoid f)) + 1) ∧ (¬f.SameCycle a b → Nat.card (Quotient (SameCycle.setoid (f * swap a b))) + 1 = Nat.card (Quotient (SameCycle.setoid f)))

Swapping two distinct outgoing successors splits their common orbit into two, or merges their two different orbits. Singleton cycles are included.

theorem Equiv.Perm.CycleSurgery.card_orbits_inv {α : Type} (f : Perm α) : Nat.card (Quotient (SameCycle.setoid f⁻¹)) = Nat.card (Quotient (SameCycle.setoid f))

Reversing the directed traversal of every orbit retains the full orbit quotient.

theorem Equiv.Perm.CycleSurgery.card_orbits_swap_mul {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (a b : α) (hab : a ≠ b) : (f.SameCycle a b → Nat.card (Quotient (SameCycle.setoid (swap a b * f))) = Nat.card (Quotient (SameCycle.setoid f)) + 1) ∧ (¬f.SameCycle a b → Nat.card (Quotient (SameCycle.setoid (swap a b * f))) + 1 = Nat.card (Quotient (SameCycle.setoid f)))

Swapping incoming successors has the same exact split/merge count as swapping outgoing successors. The orbit condition is evaluated in the original permutation.

def Equiv.Perm.CycleSurgery.splice {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : Perm (Option (Option α))

The literal face successor after inserting the two edge ends. some none is the first new end and none the second; the remaining points are old indexed darts.

theorem Equiv.Perm.CycleSurgery.removeNone_splice {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : removeNone (splice f h k) = swap (some k) none * optionCongr (swap h k * f)

Deleting the second new end leaves the first inserted before k, in the permutation whose incoming successors at h and k have been interchanged. This holds also for h=k.

theorem Equiv.Perm.CycleSurgery.removeNone_splice_none {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : (removeNone (splice f h k)) none = some k

The first inserted end is never a singleton face after deleting the second end.

theorem Equiv.Perm.CycleSurgery.splice_none_fixed_iff {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : (splice f h k) none = none ↔ h = k

The second inserted end is a singleton face exactly for coincident corners.

theorem Equiv.Perm.CycleSurgery.removeNone_removeNone_splice {α : Type} [DecidableEq α] (f : Perm α) (h k : α) : (removeNone (splice f h k)).removeNone = swap h k * f

Removing both inserted ends leaves precisely the incoming-successor swap.

theorem Equiv.Perm.CycleSurgery.card_orbits_splice {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h k : α) : Nat.card (Quotient (SameCycle.setoid (splice f h k))) = Nat.card (Quotient (SameCycle.setoid (swap h k * f))) + if h = k then 1 else 0

Exact face count before distinguishing the equal-corner and two-corner cases.

theorem Equiv.Perm.CycleSurgery.card_orbits_splice_sameCycle {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h k : α) (hc : f.SameCycle h k) : Nat.card (Quotient (SameCycle.setoid (splice f h k))) = Nat.card (Quotient (SameCycle.setoid f)) + 1

Cofacial corners, including coincident corners, gain exactly one face.

theorem Equiv.Perm.CycleSurgery.card_orbits_splice_of_not_sameCycle {α : Type} [DecidableEq α] [Finite α] (f : Perm α) (h k : α) (hc : ¬f.SameCycle h k) : Nat.card (Quotient (SameCycle.setoid (splice f h k))) + 1 = Nat.card (Quotient (SameCycle.setoid f))

Different face cycles merge, so the total face count decreases by one.