Weighted stabilizer factorization

The completed cycle-type weight summed over the stabilizer of a colouring factorizes over the fibres, and the colour-character weighted permutation sum evaluates to n! times the product of the complete homogeneous values of the fibre sizes. The two cycle-type transport facts (invariance under permCongr and additivity over sigmaCongrRight) enter as explicit hypotheses, discharged in ColourCycleSum.lean.

noncomputable def RS.cycleProdOn {γ : Type} [Fintype γ] [DecidableEq γ] (t : ℕ → ℂ) (σ : Equiv.Perm γ) : ℂ

The completed cycle-type product on an arbitrary finite carrier.

Equations

• RS.cycleProdOn t σ = (Multiset.map t σ.cycleType).prod * t 1 ^ (Fintype.card γ - σ.cycleType.sum)

@[reducible, inline]

abbrev RS.PermCongrCT : Prop

The permCongr-invariance hypothesis.

Equations

• RS.PermCongrCT = ∀ (A B : Type) [inst : Fintype A] [inst_1 : DecidableEq A] [inst_2 : Fintype B] [inst_3 : DecidableEq B] (e : A ≃ B) (σ : Equiv.Perm A), (e.permCongr σ).cycleType = σ.cycleType

@[reducible, inline]

abbrev RS.SigmaCT : Prop

The sigma-additivity hypothesis.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.sum_cycleProdOn_eq (H1 : PermCongrCT) {γ : Type} [Fintype γ] [DecidableEq γ] (t : ℕ → ℂ) : ∑ σ : Equiv.Perm γ, cycleProdOn t σ = ↑(Fintype.card γ).factorial * newtonH t (Fintype.card γ)

The general-carrier cycle sum, by transport along an enumeration.

theorem RS.cycleProd_ofFibrePerms {n N : ℕ} (H1 : PermCongrCT) (H2 : SigmaCT) (t : ℕ → ℂ) (f : Fin n → Fin N) (σ : (j : Fin N) → Equiv.Perm { i : Fin n // f i = j }) : cycleProd t (ofFibrePerms f σ) = ∏ j : Fin N, cycleProdOn t (σ j)

The fiberwise cycle weight: the completed cycle weight of an assembled fixing permutation is the product of the fibre weights.

theorem RS.sum_fixing_cycleProd {n N : ℕ} (H1 : PermCongrCT) (H2 : SigmaCT) (t : ℕ → ℂ) (f : Fin n → Fin N) : ∑ π : Equiv.Perm (Fin n) with f ∘ ⇑π = f, cycleProd t π = ∏ j : Fin N, ↑(fibreCard f j).factorial * newtonH t (fibreCard f j)

The weighted stabilizer factorization: the completed cycle weight summed over the stabilizer of a colouring is the product of the fibre factorial-homogeneous values.

theorem RS.colour_cycleSum {n N : ℕ} (H1 : PermCongrCT) (H2 : SigmaCT) (t : ℕ → ℂ) (α : Fin N → ℕ) (hsum : ∑ j : Fin N, α j = n) : ∑ π : Equiv.Perm (Fin n), ↑(colourChar α π) * cycleProd t π = ↑n.factorial * ∏ j : Fin N, newtonH t (α j)

The colour cycle sum: the colourChar-weighted completed cycle sum evaluates to n! times the product of the complete homogeneous values of the composition.