Mixed fixed-point decomposition

Decomposes the subtype of colourings fixed by a lifted permutation viaEmbeddingHom (castLEEmb h) σ into a product of the fixed colourings on the first m coordinates and free colourings on the tail.

theorem RS.card_tail {m n : ℕ} (h : m ≤ n) : Fintype.card { i : Fin n // m ≤ ↑i } = n - m

The tail has the expected size.

noncomputable def RS.mixedFixedEquiv {m n N : ℕ} (h : m ≤ n) (σ : Equiv.Perm (Fin m)) : { f : Fin n → Fin N // f ∘ ⇑((Equiv.Perm.viaEmbeddingHom (Fin.castLEEmb h)) σ) = f } ≃ { g : Fin m → Fin N // g ∘ ⇑σ = g } × ({ i : Fin n // m ≤ ↑i } → Fin N)

The fixed-point decomposition: a colouring fixed by a lifted permutation is a fixed colouring on the head together with a free one on the tail, which the lift does not move.

Equations

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

theorem RS.mixedFixedEquiv_symm_fibreCard {m n N : ℕ} (h : m ≤ n) (σ : Equiv.Perm (Fin m)) (g : { g : Fin m → Fin N // g ∘ ⇑σ = g }) (t : { i : Fin n // m ≤ ↑i } → Fin N) (c : Fin N) : fibreCard (↑((mixedFixedEquiv h σ).symm (g, t))) c = fibreCard (↑g) c + {i : { i : Fin n // m ≤ ↑i } | t i = c}.card

The colour counts add across the split.