Additive splitting of the completed cycle product

The completed cycle product of a permutation, generalised from Fin n to an arbitrary finite carrier, splits additively over the invariant subsets of the carrier: at a pointwise sum of scalar sequences it equals the sum, over all invariant subsets, of the product of the completed cycle products of the two restrictions — to the subset and to its complement. This is the combinatorial heart of the induction-multiplicity identity.

The route is through orbits: the completed cycle product is the product of t (O.card) over the set of all orbits of the permutation, singleton orbits included; the splitting is then the expansion of a product of binomials, with subsets of the orbit set enumerating exactly the invariant subsets of the carrier.

The completed cycle product over an arbitrary carrier

noncomputable def RS.cycleFunG {α : Type u_1} [Fintype α] [DecidableEq α] (t : ℕ → ℂ) (π : Equiv.Perm α) : ℂ

The completed cycle product of a prospective power-sum sequence over an arbitrary finite carrier: the product of t over the cycle type, completed by t 1 over the fixed points.

Equations

• RS.cycleFunG t π = (Multiset.map t π.cycleType).prod * t 1 ^ (Fintype.card α - π.cycleType.sum)

theorem RS.cycleFunG_fin {n : ℕ} (t : ℕ → ℂ) (π : Equiv.Perm (Fin n)) : cycleFunG t π = cycleFun t π

On Fin n the generalised completed cycle product is the completed cycle product.

theorem RS.cycleType_permCongr' {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (e : α ≃ β) (π : Equiv.Perm α) : (e.permCongr π).cycleType = π.cycleType

The cycle type is invariant under conjugation by an equivalence of carriers. Universe-polymorphic form of cycleType_permCongr.

theorem RS.cycleFunG_permCongr {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (e : α ≃ β) (t : ℕ → ℂ) (π : Equiv.Perm α) : cycleFunG t (e.permCongr π) = cycleFunG t π

The completed cycle product is invariant under conjugation by an equivalence of carriers.

Invariant subsets

theorem RS.mem_iff_of_invariant {α : Type u_1} {π : Equiv.Perm α} {s : Finset α} (hs : ∀ x ∈ s, π x ∈ s) (x : α) : π x ∈ s ↔ x ∈ s

A finite set closed under a permutation is closed in both directions: the permutation restricts to an injective self-map of the set, which is onto by finiteness.

theorem RS.invariant_compl {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (hs : ∀ x ∈ s, π x ∈ s) (x : α) : x ∈ sᶜ → π x ∈ sᶜ

The complement of an invariant set is invariant.

theorem RS.zpow_apply_mem_of_invariant {α : Type u_1} {π : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), π x ∈ s ↔ x ∈ s) {x : α} (hx : x ∈ s) (i : ℤ) : (π ^ i) x ∈ s

Integer powers of a permutation preserve a two-sided invariant set.

def RS.permRestrict {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) (s : Finset α) : Equiv.Perm ↥s

The restriction of a permutation to a finite subset, as a permutation of the subtype: the two-sided restriction when the subset is invariant, the identity otherwise.

Equations

• RS.permRestrict π s = if h : ∀ (x : α), π x ∈ s ↔ x ∈ s then π.subtypePerm h else 1

theorem RS.permRestrict_of_invariant {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (h : ∀ (x : α), π x ∈ s ↔ x ∈ s) : permRestrict π s = π.subtypePerm h

On an invariant subset the restriction is subtypePerm.

Orbits as finite sets

def RS.cycleOrbit {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) (x : α) : Finset α

The orbit of a point under a permutation, as a finite set; singleton orbits of fixed points included.

Equations

• RS.cycleOrbit π x = Finset.filter (π.SameCycle x) Finset.univ

theorem RS.mem_cycleOrbit {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {x y : α} : y ∈ cycleOrbit π x ↔ π.SameCycle x y

Membership in an orbit is the same-cycle relation.

theorem RS.self_mem_cycleOrbit {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) (x : α) : x ∈ cycleOrbit π x

A point lies in its own orbit.

theorem RS.apply_mem_cycleOrbit {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) (x : α) : π x ∈ cycleOrbit π x

The image of a point lies in the point's orbit.

theorem RS.cycleOrbit_eq_of_mem {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {x y : α} (h : y ∈ cycleOrbit π x) : cycleOrbit π y = cycleOrbit π x

Orbits through a common point coincide.

theorem RS.cycleOrbit_eq_singleton {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {x : α} (hx : π x = x) : cycleOrbit π x = {x}

The orbit of a fixed point is a singleton.

theorem RS.cycleOrbit_eq_support_cycleOf {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {x : α} (hx : π x ≠ x) : cycleOrbit π x = (π.cycleOf x).support

The orbit of a moved point is the support of its cycle.

def RS.cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) : Finset (Finset α)

The set of orbits of a permutation, singleton orbits included.

Equations

• RS.cycleOrbits π = Finset.image (RS.cycleOrbit π) Finset.univ

theorem RS.cycleOrbit_mem_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) (x : α) : cycleOrbit π x ∈ cycleOrbits π

Every orbit belongs to the set of orbits.

theorem RS.mem_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {O : Finset α} : O ∈ cycleOrbits π ↔ ∃ (x : α), cycleOrbit π x = O

The members of the set of orbits are the orbits.

theorem RS.eq_cycleOrbit_of_mem {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {O : Finset α} (hO : O ∈ cycleOrbits π) {x : α} (hx : x ∈ O) : O = cycleOrbit π x

An orbit is the orbit of each of its points.

theorem RS.nonempty_of_mem_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {O : Finset α} (hO : O ∈ cycleOrbits π) : O.Nonempty

Orbits are nonempty.

The completed cycle product as an orbit product

theorem RS.filter_card_one_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) : {O ∈ cycleOrbits π | O.card = 1} = Finset.image (fun (x : α) => {x}) π.supportᶜ

The singleton orbits are the fixed points.

theorem RS.filter_card_ne_one_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] (π : Equiv.Perm α) : {O ∈ cycleOrbits π | ¬O.card = 1} = Finset.image Equiv.Perm.support π.cycleFactorsFinset

The non-singleton orbits are the supports of the cycle factors.

theorem RS.cycleFunG_eq_prod_cycleOrbits {α : Type u_1} [Fintype α] [DecidableEq α] (t : ℕ → ℂ) (π : Equiv.Perm α) : cycleFunG t π = ∏ O ∈ cycleOrbits π, t O.card

The completed cycle product is the orbit product: the product of t at the orbit sizes, over all orbits, singleton orbits included.

Restriction to an invariant subset

theorem RS.cycleOrbit_subset_of_invariant {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), π x ∈ s ↔ x ∈ s) {x : α} (hx : x ∈ s) : cycleOrbit π x ⊆ s

Orbits of points of a two-sided invariant set stay inside the set.

theorem RS.cycleOrbit_subtypePerm {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (h : ∀ (x : α), π x ∈ s ↔ x ∈ s) (x : ↥s) : Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ s) (cycleOrbit (π.subtypePerm h) x) = cycleOrbit π ↑x

The orbit of the restriction to an invariant set is the orbit of the ambient permutation, transported along the subtype map.

theorem RS.cycleFunG_subtypePerm {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (h : ∀ (x : α), π x ∈ s ↔ x ∈ s) (t : ℕ → ℂ) : cycleFunG t (π.subtypePerm h) = ∏ O ∈ cycleOrbits π with O ⊆ s, t O.card

The completed cycle product of the restriction to an invariant set is the product over the ambient orbits inside the set.

Invariant subsets are unions of orbits

theorem RS.biUnion_invariant {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {S : Finset (Finset α)} (hS : S ⊆ cycleOrbits π) (x : α) : x ∈ S.biUnion id → π x ∈ S.biUnion id

A union of orbits is an invariant set.

theorem RS.biUnion_filter_subset_eq {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), π x ∈ s ↔ x ∈ s) : {O ∈ cycleOrbits π | O ⊆ s}.biUnion id = s

An invariant set is the union of the orbits it contains.

theorem RS.filter_subset_biUnion {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {S : Finset (Finset α)} (hS : S ⊆ cycleOrbits π) : {O ∈ cycleOrbits π | O ⊆ S.biUnion id} = S

The orbits inside a union of orbits are the orbits of the union.

theorem RS.filter_subset_compl_eq_sdiff {α : Type u_1} [Fintype α] [DecidableEq α] {π : Equiv.Perm α} {s : Finset α} (hs : ∀ (x : α), π x ∈ s ↔ x ∈ s) : {O ∈ cycleOrbits π | O ⊆ sᶜ} = cycleOrbits π \ {O ∈ cycleOrbits π | O ⊆ s}

The orbits inside the complement of an invariant set are the orbits not inside the set.

The additive splitting

theorem RS.cycleFunG_add_split {α : Type u_1} [Fintype α] [DecidableEq α] (t t' : ℕ → ℂ) (π : Equiv.Perm α) : cycleFunG (fun (c : ℕ) => t c + t' c) π = ∑ s : Finset α with ∀ x ∈ s, π x ∈ s, cycleFunG t (permRestrict π s) * cycleFunG t' (permRestrict π sᶜ)

Additive splitting of the completed cycle product: at a pointwise sum of scalar sequences the completed cycle product is the sum, over all invariant subsets of the carrier, of the product of the completed cycle products of the restriction to the subset in the first sequence and of the restriction to the complement in the second. Each orbit contributes a binomial factor, and the expansion enumerates the invariant subsets.

theorem RS.cycleFun_add_split {n : ℕ} (t t' : ℕ → ℂ) (π : Equiv.Perm (Fin n)) : cycleFun (fun (c : ℕ) => t c + t' c) π = ∑ s : Finset (Fin n) with ∀ x ∈ s, π x ∈ s, cycleFunG t (permRestrict π s) * cycleFunG t' (permRestrict π sᶜ)

Additive splitting of the completed cycle product on Fin n: the canonical form of the splitting for the shape-level consumers.