Joining selected complete permutation orbits

Disjoint predicates, one invariant, select disjoint sets of complete orbits. Their union has the sum of their cardinalities. A transposition joining two different cycles removes one selected orbit exactly when its corners are selected. Fixed points and empty selections are included. Incoming and outgoing successor conventions are both explicit.

noncomputable def Equiv.Perm.SelectedOrbits.orbitOnUnionEquiv {α : Type} [Finite α] (f : Perm α) (p q : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (hd : _root_.Disjoint p q) : (OrbitOn f fun (a : α) => p a ∨ q a) ≃ OrbitOn f p ⊕ OrbitOn f q

The complete orbits selected by disjoint predicates, the first invariant, are exactly the disjoint sum of the two selected orbit sets, including singleton cycles.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_union {α : Type} [Finite α] (f : Perm α) (p q : α → Prop) (hp : ∀ (a : α), p (f a) ↔ p a) (hd : _root_.Disjoint p q) : Nat.card (OrbitOn f fun (a : α) => p a ∨ q a) = Nat.card (OrbitOn f p) + Nat.card (OrbitOn f q)

The disjoint union of invariant selections adds their complete orbit counts. Only the first predicate needs invariance to exclude a shared orbit. The other may select partial representatives, because OrbitOn itself selects their complete equivalence classes.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_swap_mul_of_not_sameCycle {α : 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 (swap h k * f) p) + if p h then 1 else 0) = Nat.card (OrbitOn f p)

An incoming successor swap joining different cycles removes one selected complete orbit when both corners are selected; an unselected pair changes no selected orbit.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_mul_swap_of_not_sameCycle {α : 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 (f * swap h k) p) + if p h then 1 else 0) = Nat.card (OrbitOn f p)

The corresponding exact count for an outgoing successor swap. The old cycle relation and old corner membership determine the decrease, including singleton and empty cases.

noncomputable def Equiv.Perm.SelectedOrbits.orbitOnSumEquiv {α β : Type} [Finite α] [Finite β] (f : Perm α) (g : Perm β) (p : α → Prop) (q : β → Prop) : OrbitOn (Equiv.sumCongr f g) (Sum.elim p q) ≃ OrbitOn f p ⊕ OrbitOn g q

Disjoint-sum coordinates split all selected complete orbits into their source blocks. No invariance is needed: selections mean the full orbits meeting the given predicates.

theorem Equiv.Perm.SelectedOrbits.card_orbitOn_sum {α β : Type} [Finite α] [Finite β] (f : Perm α) (g : Perm β) (p : α → Prop) (q : β → Prop) : Nat.card (OrbitOn (Equiv.sumCongr f g) (Sum.elim p q)) = Nat.card (OrbitOn f p) + Nat.card (OrbitOn g q)

The selected complete orbit count of a sum is the sum of its selected block counts.