The cycles of a permutation acting separately on the two halves of a sum

Equiv.Perm.sumCongr σ τ permutes α ⊕ β by σ on the left summand and by τ on the right one. Every cycle stays inside one of the two halves, so all the cycle data simply concatenates.

Main results

• Equiv.Perm.cycleType_sumCongr, Equiv.Perm.card_support_sumCongr, Equiv.Perm.parts_partition_sumCongr: the cycle type, the number of moved points and the parts of the full, fixed-point-aware partition are additive.
• Equiv.Perm.orbitCount_sumCongr: so is the number of orbits, fixed points included.
• Equiv.Perm.orbitCount_sumCongr_one_mul_swap_mul_swap_mul_swap_mul_swap: splicing four adjoined fixed points into the orbits of a permutation leaves its number of orbits.
• Equiv.Perm.sumCongr_zpow: powers are taken summandwise.
• Equiv.Perm.sameCycle_sumCongr_inl, Equiv.Perm.sameCycle_sumCongr_inr: two points of one summand share a cycle exactly when they share a cycle of the permutation of that summand.
• Equiv.Perm.finSumPerm: the same construction read on Fin (m + n) through finSumFinEquiv, with Equiv.Perm.finSumPermHom packaging it as a monoid homomorphism from Equiv.Perm (Fin m) × Equiv.Perm (Fin n), and with the two cycle-counting results transported.

Splitting a sum permutation into its two halves

theorem Equiv.Perm.sumCongr_one_eq_extendDomain {α : Type u_1} {β : Type u_2} (σ : Perm α) : σ.sumCongr 1 = σ.extendDomain sumIsLeft.symm

A permutation of the left summand, extended by the identity, is the extension of its domain along Equiv.sumIsLeft.

theorem Equiv.Perm.one_sumCongr_eq_extendDomain {α : Type u_1} {β : Type u_2} (τ : Perm β) : sumCongr 1 τ = τ.extendDomain sumIsRight.symm

A permutation of the right summand, extended by the identity, is the extension of its domain along Equiv.sumIsRight.

theorem Equiv.Perm.disjoint_sumCongr_one_one_sumCongr {α : Type u_1} {β : Type u_2} (σ : Perm α) (τ : Perm β) : (σ.sumCongr 1).Disjoint (sumCongr 1 τ)

The two halves of a sum permutation are disjoint: each of them fixes everything the other can move.

@[simp]

theorem Equiv.Perm.sumCongr_zpow {α : Type u_1} {β : Type u_2} (σ : Perm α) (τ : Perm β) (k : ℤ) : σ.sumCongr τ ^ k = (σ ^ k).sumCongr (τ ^ k)

The powers of a sum permutation are taken separately on the two summands.

@[simp]

theorem Equiv.Perm.sameCycle_sumCongr_inl {α : Type u_1} {β : Type u_2} {σ : Perm α} {τ : Perm β} {a b : α} : (σ.sumCongr τ).SameCycle (Sum.inl a) (Sum.inl b) ↔ σ.SameCycle a b

Two points of the left summand lie in one cycle of Equiv.Perm.sumCongr σ τ exactly when they lie in one cycle of σ.

@[simp]

theorem Equiv.Perm.sameCycle_sumCongr_inr {α : Type u_1} {β : Type u_2} {σ : Perm α} {τ : Perm β} {a b : β} : (σ.sumCongr τ).SameCycle (Sum.inr a) (Sum.inr b) ↔ τ.SameCycle a b

Two points of the right summand lie in one cycle of Equiv.Perm.sumCongr σ τ exactly when they lie in one cycle of τ.

@[simp]

theorem Equiv.Perm.not_sameCycle_sumCongr_inl_inr {α : Type u_1} {β : Type u_2} (σ : Perm α) (τ : Perm β) (a : α) (b : β) : ¬(σ.sumCongr τ).SameCycle (Sum.inl a) (Sum.inr b)

Points in different summands cannot lie in the same cycle of a sum permutation.

Additivity of the cycle data

@[simp]

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

The cycles of Equiv.Perm.sumCongr σ τ are those of σ together with those of τ.

@[simp]

theorem Equiv.Perm.card_support_sumCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (σ : Perm α) (τ : Perm β) : (σ.sumCongr τ).support.card = σ.support.card + τ.support.card

The points moved by Equiv.Perm.sumCongr σ τ are those moved by σ together with those moved by τ.

@[simp]

theorem Equiv.Perm.parts_partition_sumCongr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (σ : Perm α) (τ : Perm β) : (σ.sumCongr τ).partition.parts = σ.partition.parts + τ.partition.parts

The full, fixed-point-aware cycle partition of a sum permutation is the concatenation of the two partitions it is assembled from. Unlike Equiv.Perm.cycleType_sumCongr this keeps track of the fixed points, and it is the form the Euler characteristic of a disjoint sum of permutation triples is computed from.

@[simp]

theorem Equiv.Perm.orbitCount_sumCongr {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (σ : Perm α) (τ : Perm β) : TauCeti.orbitCount (σ.sumCongr τ) = TauCeti.orbitCount σ + TauCeti.orbitCount τ

The orbits of Equiv.Perm.sumCongr σ τ, fixed points included, are those of σ together with those of τ.

theorem Equiv.Perm.orbitCount_sumCongr_mul_swap_mul_swap_add_two {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Finite α] [Finite β] (σ : Perm α) (τ : Perm β) (a c : α) {b d : β} (hbd : ¬τ.SameCycle b d) : TauCeti.orbitCount (σ.sumCongr τ * swap (Sum.inl a) (Sum.inr b) * swap (Sum.inl c) (Sum.inr d)) + 2 = TauCeti.orbitCount σ + TauCeti.orbitCount τ

Attach two distinct cycles of the right summand to cycles of the left summand. Each attachment removes one orbit, even if the two left endpoints lie in the same cycle.

theorem Equiv.Perm.orbitCount_sumCongr_one_mul_swap_mul_swap_mul_swap_mul_swap {α : Type u_1} [DecidableEq α] [Finite α] (σ : Perm α) (x₀ x₁ x₂ x₃ : α) {i₀ i₁ i₂ i₃ : Fin 4} (h₀₁ : i₀ ≠ i₁) (h₀₂ : i₀ ≠ i₂) (h₀₃ : i₀ ≠ i₃) (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : TauCeti.orbitCount (σ.sumCongr 1 * swap (Sum.inl x₀) (Sum.inr i₀) * swap (Sum.inl x₁) (Sum.inr i₁) * swap (Sum.inl x₂) (Sum.inr i₂) * swap (Sum.inl x₃) (Sum.inr i₃)) = TauCeti.orbitCount σ

Splicing four adjoined fixed points. Adjoin four fixed points to σ and splice each of them into an orbit, i₀ after x₀, then i₁ after x₁, i₂ after x₂ and i₃ after x₃: each splice removes one orbit, so as many orbits as σ has are left.

The sum of a permutation of Fin m and a permutation of Fin n

def Equiv.Perm.finSumPerm {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) : Perm (Fin (m + n))

The permutation of Fin (m + n) that acts as σ on the first m labels and as τ on the last n, the two blocks being separated by finSumFinEquiv.

Equations

• σ.finSumPerm τ = finSumFinEquiv.permCongr (σ.sumCongr τ)

def Equiv.Perm.finSumPermHom (m n : ℕ) : Perm (Fin m) × Perm (Fin n) →* Perm (Fin (m + n))

Permuting the first m labels and the last n labels separately, as a monoid homomorphism. Its range is the subgroup of Equiv.Perm (Fin (m + n)) preserving the two blocks.

Equations

• Equiv.Perm.finSumPermHom m n = finSumFinEquiv.permCongrHom.toMonoidHom.comp (Equiv.Perm.sumCongrHom (Fin m) (Fin n))

@[simp]

theorem Equiv.Perm.finSumPermHom_apply {m n : ℕ} (p : Perm (Fin m) × Perm (Fin n)) : (finSumPermHom m n) p = p.1.finSumPerm p.2

theorem Equiv.Perm.finSumPerm_apply {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) (x : Fin (m + n)) : (σ.finSumPerm τ) x = finSumFinEquiv (Sum.map (⇑σ) (⇑τ) (finSumFinEquiv.symm x))

@[simp]

theorem Equiv.Perm.finSumPerm_apply_castAdd {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) (i : Fin m) : (σ.finSumPerm τ) (Fin.castAdd n i) = Fin.castAdd n (σ i)

@[simp]

theorem Equiv.Perm.finSumPerm_apply_natAdd {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) (j : Fin n) : (σ.finSumPerm τ) (Fin.natAdd m j) = Fin.natAdd m (τ j)

@[simp]

theorem Equiv.Perm.finSumPerm_one {m n : ℕ} : finSumPerm 1 1 = 1

@[simp]

theorem Equiv.Perm.finSumPerm_inv {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) : (σ.finSumPerm τ)⁻¹ = σ⁻¹.finSumPerm τ⁻¹

@[simp]

theorem Equiv.Perm.finSumPerm_mul {m n : ℕ} (σ σ' : Perm (Fin m)) (τ τ' : Perm (Fin n)) : σ.finSumPerm τ * σ'.finSumPerm τ' = (σ * σ').finSumPerm (τ * τ')

@[simp]

theorem Equiv.Perm.parts_partition_finSumPerm {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) : (σ.finSumPerm τ).partition.parts = σ.partition.parts + τ.partition.parts

The full cycle partition of Equiv.Perm.finSumPerm σ τ is the concatenation of those of σ and of τ.

@[simp]

theorem Equiv.Perm.orbitCount_finSumPerm {m n : ℕ} (σ : Perm (Fin m)) (τ : Perm (Fin n)) : TauCeti.orbitCount (σ.finSumPerm τ) = TauCeti.orbitCount σ + TauCeti.orbitCount τ

The number of orbits of Equiv.Perm.finSumPerm σ τ, fixed points included, is the sum of the numbers of orbits of σ and of τ.