Complete permutation orbits on invariant subsets

Equiv.Perm.SelectedOrbits.OrbitOn selects complete orbit classes meeting an invariant subset. Subtype and coordinate equivalences localize the counts, including singleton cycles. Exact splice and incoming-swap counts require no graph or genus assumptions.

@[reducible, inline]

abbrev Equiv.Perm.SelectedOrbits.OrbitOn {α : Type} (f : Perm α) (p : α → Prop) : Type

Actual orbit classes with a representative in the selected invariant dart set.

noncomputable def Equiv.Perm.SelectedOrbits.subtypeOrbitEquiv {α : Type} (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) : Quotient (SameCycle.setoid (f.subtypePerm hp)) ≃ OrbitOn f p

Restriction to invariant darts identifies exactly the selected original orbit classes.

def Equiv.Perm.SelectedOrbits.extendedPredicate {α : Type} (p : α → Prop) (newPoints : Prop) : Option (Option α) → Prop

Include both new indexed ends in a selected component exactly when newPoints holds.

theorem Equiv.Perm.SelectedOrbits.splice_preserves {α : Type} [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (q : Prop) (hh : p h ↔ q) (hk : p k ↔ q) (z : Option (Option α)) : extendedPredicate p q ((CycleSurgery.splice f h k) z) ↔ extendedPredicate p q z

A splice retains an invariant dart selection when its two corners agree on membership.

def Equiv.Perm.SelectedOrbits.selectedPointEquiv {α : Type} (p : α → Prop) : Option (Option { a : α // p a }) ≃ { z : Option (Option α) // extendedPredicate p True z }

When both new points are selected, the selected dart type is literally the old selected set with two indexed ends adjoined.

theorem Equiv.Perm.SelectedOrbits.selected_splice_permCongr {α : Type} [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hh : p h) (hk : p k) : (selectedPointEquiv p).permCongr (CycleSurgery.splice (f.subtypePerm hp) ⟨h, hh⟩ ⟨k, hk⟩) = (CycleSurgery.splice f h k).subtypePerm ⋯

Splice restriction when both corners belong to the selected invariant component.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_splice_selected {α : Type} [Finite α] [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hh : p h) (hk : p k) (hc : f.SameCycle h k) : Nat.card (OrbitOn (CycleSurgery.splice f h k) (extendedPredicate p True)) = Nat.card (OrbitOn f p) + 1

Within the selected component, cofacial insertion adds one actual face class.

def Equiv.Perm.SelectedOrbits.unselectedPointEquiv {α : Type} (p : α → Prop) : { a : α // p a } ≃ { z : Option (Option α) // extendedPredicate p False z }

Excluding both new ends leaves exactly the old selected darts.

theorem Equiv.Perm.SelectedOrbits.unselected_splice_permCongr {α : Type} [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hh : ¬p h) (hk : ¬p k) : (unselectedPointEquiv p).permCongr (f.subtypePerm hp) = (CycleSurgery.splice f h k).subtypePerm ⋯

A component disjoint from the splice corners retains its literal restricted rotation.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_splice_unselected {α : Type} [Finite α] [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hh : ¬p h) (hk : ¬p k) : Nat.card (OrbitOn (CycleSurgery.splice f h k) (extendedPredicate p False)) = Nat.card (OrbitOn f p)

Faces in every component disjoint from the corners are unchanged, including singleton faces and the empty set of dart faces at a declared point component.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_splice {α : Type} [Finite α] [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hm : p h ↔ p k) (hc : f.SameCycle h k) : Nat.card (OrbitOn (CycleSurgery.splice f h k) (extendedPredicate p (p h))) = Nat.card (OrbitOn f p) + if p h then 1 else 0

Exact local face count for a cofacial splice in any invariant selection.

noncomputable def Equiv.Perm.SelectedOrbits.orbitOnEquiv {α β : Type} [Finite α] [Finite β] (e : α ≃ β) (f : Perm α) (g : Perm β) (hm : ∀ (a : α), e (f a) = g (e a)) (p : α → Prop) (q : β → Prop) (hp : ∀ (a : α), p a ↔ q (e a)) : OrbitOn f p ≃ OrbitOn g q

Coordinate transport preserves the selected original orbit classes.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_swap_mul {α : Type} [Finite α] [DecidableEq α] (f : Perm α) (p : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (h k : α) (hne : h ≠ k) (hc : f.SameCycle h k) : Nat.card (OrbitOn (swap h k * f) p) = Nat.card (OrbitOn f p) + if p h then 1 else 0

An incoming swap at distinct same-cycle points adds one selected orbit in their invariant component, and retains every selected orbit outside that component.