Cycle data under permutation transport

Transporting a permutation along an equivalence of finite types preserves its cycle type and its fixed-point count: permCongr is extendDomain over the trivial predicate, and extendDomain preserves cycle types.

The consequences for a sum of permutations follow: the two factors sumCongr σ 1 and sumCongr 1 τ are disjoint, so a sumCongr has the sum of the two cycle types and the sum of the two fixed-point counts.

theorem RS.permCongr_eq_extendDomain {α β : Type} (e : α ≃ β) (π : Equiv.Perm α) : e.permCongr π = π.extendDomain (e.trans (Equiv.subtypeUnivEquiv ⋯).symm)

permCongr is extendDomain along the trivial subtype.

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

Transporting a permutation preserves its cycle type.

noncomputable def RS.fixedPointsPermCongrEquiv {α β : Type} (e : α ≃ β) (π : Equiv.Perm α) : ↑(Function.fixedPoints ⇑(e.permCongr π)) ≃ ↑(Function.fixedPoints ⇑π)

Transporting a permutation preserves its fixed points, up to equivalence.

Equations

• RS.fixedPointsPermCongrEquiv e π = (e.subtypeEquiv ⋯).symm

theorem RS.card_fixedPoints_permCongr {α β : Type} (e : α ≃ β) (π : Equiv.Perm α) [Fintype ↑(Function.fixedPoints ⇑π)] [Fintype ↑(Function.fixedPoints ⇑(e.permCongr π))] : Fintype.card ↑(Function.fixedPoints ⇑(e.permCongr π)) = Fintype.card ↑(Function.fixedPoints ⇑π)

Transporting a permutation preserves the fixed-point count.

theorem RS.cycleType_sumCongr_left {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (σ : Equiv.Perm α) : Equiv.Perm.cycleType (Equiv.sumCongr σ 1) = σ.cycleType

Left factor in a sum preserves cycle type.

theorem RS.sumCongr_right_eq_permCongr {α β : Type} (τ : Equiv.Perm β) : Equiv.sumCongr 1 τ = (Equiv.sumComm β α).permCongr (Equiv.sumCongr τ 1)

sumCongr 1 τ equals the permCongr-transport of sumCongr τ 1 by sumComm.

theorem RS.cycleType_sumCongr_right {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (τ : Equiv.Perm β) : Equiv.Perm.cycleType (Equiv.sumCongr 1 τ) = τ.cycleType

Right factor in a sum preserves cycle type.

theorem RS.disjoint_sumCongr {α β : Type} (σ : Equiv.Perm α) (τ : Equiv.Perm β) : Equiv.Perm.Disjoint (Equiv.sumCongr σ 1) (Equiv.sumCongr 1 τ)

The factors sumCongr σ 1 and sumCongr 1 τ are disjoint.

theorem RS.cycleType_sumCongr {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (σ : Equiv.Perm α) (τ : Equiv.Perm β) : Equiv.Perm.cycleType (Equiv.sumCongr σ τ) = σ.cycleType + τ.cycleType

A sum of permutations has the sum of the two cycle types.

noncomputable def RS.fixedPointsSumCongrEquiv {α β : Type} (π₁ : Equiv.Perm α) (π₂ : Equiv.Perm β) : ↑(Function.fixedPoints ⇑(Equiv.sumCongr π₁ π₂)) ≃ ↑(Function.fixedPoints ⇑π₁) ⊕ ↑(Function.fixedPoints ⇑π₂)

The fixed points of a sum of permutations are the sum of the two fixed-point sets.

Equations

• RS.fixedPointsSumCongrEquiv π₁ π₂ = Equiv.subtypeSum.trans ((Equiv.subtypeEquivRight ⋯).sumCongr (Equiv.subtypeEquivRight ⋯))

theorem RS.card_fixedPoints_sumCongr {α β : Type} (π₁ : Equiv.Perm α) (π₂ : Equiv.Perm β) [Fintype ↑(Function.fixedPoints ⇑(Equiv.sumCongr π₁ π₂))] [Fintype ↑(Function.fixedPoints ⇑π₁)] [Fintype ↑(Function.fixedPoints ⇑π₂)] : Fintype.card ↑(Function.fixedPoints ⇑(Equiv.sumCongr π₁ π₂)) = Fintype.card ↑(Function.fixedPoints ⇑π₁) + Fintype.card ↑(Function.fixedPoints ⇑π₂)

A sum of permutations has the sum of the two fixed-point counts.