Elementary facts about permutations

This file records general-purpose facts about permutations: a map intertwining two permutations intertwines their integer powers (Function.Semiconj.perm_zpow_right), a transposition preserves the complement of a set containing neither of its swapped points, an identity between transpositions, a permutation transporting two points outside a fixed set to another such pair, the values of the three-cycle written as a product of two transpositions sharing a point, a characterization of permutations with a unique fixed point, functions constant on a permutation orbit, the orbit relation of an involution, a positive-power representative of a relation inside a periodic orbit, a function whose difference z ↦ c (σ⁻¹ z) - c z joins points in the same orbit (Equiv.Perm.SameCycle.exists_comp_symm_sub_eq, Equiv.Perm.exists_comp_symm_sub_eq_sum), a transposition forming one cycle on a Fin 2 fibre over Fin 1, a permutation transported along an injection, the combination of two permutations transported along injections with disjoint ranges, the fact that a permutation is a single cycle on each of its own orbits, the transport of its cycles along an equivalence of types, and the factorization of an invariant function through a map on whose fibres the permutation is a single cycle, and a correction by a power of a cycle for a permutation commuting with it. It also identifies functions invariant under a permutation with functions on its cycle quotient (TauCeti.invariantColouringEquiv). Finally, right multiplication by a is a single cycle on the whole group exactly when a generates it (Equiv.isCycleOn_mulRight_univ_iff).

theorem Function.Semiconj.perm_zpow_right {α : Type u_1} {γ : Type u_2} {σ : Equiv.Perm α} {τ : Equiv.Perm γ} {g : α → γ} (hg : Semiconj g ⇑σ ⇑τ) (k : ℤ) : Semiconj g ⇑(σ ^ k) ⇑(τ ^ k)

A map intertwining two permutations also intertwines all of their integer powers. This extends Function.Semiconj.iterate_right to negative exponents.

theorem Equiv.Perm.SameCycle.apply_eq_of_apply_eq {α : Type u_1} {β : Sort u_2} {σ : Perm α} {x y : α} {f : α → β} (hσ : σ.SameCycle x y) (hf : ∀ (z : α), f (σ z) = f z) : f x = f y

A function invariant under one application of a permutation is constant on every orbit of that permutation.

theorem Equiv.Perm.SameCycle.map {α : Type u_1} {σ : Perm α} {x y : α} {γ : Type u_3} {τ : Perm γ} {g : α → γ} (hσ : σ.SameCycle x y) (hg : ∀ (z : α), g (σ z) = τ (g z)) : τ.SameCycle (g x) (g y)

A map intertwining two permutations carries orbits of the first permutation into orbits of the second.

theorem Equiv.Perm.SameCycle.exists_pos_pow_eq_of_mem_periodicPts {α : Type u_1} {σ : Perm α} {x y : α} (h : σ.SameCycle x y) (hx : x ∈ Function.periodicPts ⇑σ) : ∃ (j : ℕ), 0 < j ∧ (σ ^ j) x = y

If a periodic point x of σ shares its orbit with y, some positive natural power of σ carries x to y.

theorem Equiv.Perm.SameCycle.exists_comp_symm_sub_eq {α : Type u_1} {σ : Perm α} {x y : α} [DecidableEq α] {M : Type u_4} [AddCommGroup M] (h : σ.SameCycle x y) (a : M) : ∃ (c : α → M), (fun (z : α) => c ((Equiv.symm σ) z) - c z) = Pi.single y a - Pi.single x a

Two points x, y in the same orbit of σ are joined along the orbit: some c : α → M has difference z ↦ c (σ⁻¹ z) - c z equal to Pi.single y a - Pi.single x a.

theorem TauCeti.isCycleOn_swap_fin_two_fiber (f : Fin 2 → Fin 1) (i : Fin 1) : (Equiv.swap 0 1).IsCycleOn {p : Fin 2 | f p = i}

The transposition of Fin 2 is one cycle on every fibre of a map to Fin 1.

theorem Equiv.Perm.isCycleOn_setOf_sameCycle {α : Type u_1} (σ : Perm α) (x : α) : σ.IsCycleOn {y : α | σ.SameCycle x y}

A permutation is a single cycle on each of its own orbits.

theorem Equiv.Perm.isCycleOn_preimage_quotientMk {α : Type u_1} (σ : Perm α) (b : Quotient (SameCycle.setoid σ)) : σ.IsCycleOn (Quotient.mk (SameCycle.setoid σ) ⁻¹' {b})

A permutation is a single cycle on each fibre of the quotient map onto its orbits. This is the form in which the cyclic order around a vertex of a ribbon graph is read off a permutation.

theorem Equiv.Perm.factorsThrough_of_forall_isCycleOn {α : Type u_1} (σ : Perm α) {ι : Type u_2} {β : Type u_3} {g : α → ι} (hσ : ∀ (i : ι), σ.IsCycleOn {x : α | g x = i}) {f : α → β} (hf : ∀ (x : α), f (σ x) = f x) : Function.FactorsThrough f g

A function invariant under a permutation that is a single cycle on each fibre of g factors through g.

theorem Equiv.Perm.exists_comp_symm_sub_eq_sum {α : Type u_1} [DecidableEq α] {ι : Type u_2} {M : Type u_3} [Fintype ι] [AddCommGroup M] {σ : Perm α} {u v : ι → α} (h : ∀ (i : ι), σ.SameCycle (u i) (v i)) (a : ι → M) : ∃ (c : α → M), (fun (z : α) => c ((Equiv.symm σ) z) - c z) = ∑ i : ι, Pi.single (v i) (a i) - ∑ i : ι, Pi.single (u i) (a i)

Finitely many pairs u i, v i, each in a single orbit of σ, are joined along the orbits with weights a i: some c : α → M has difference z ↦ c (σ⁻¹ z) - c z equal to ∑ i, Pi.single (v i) (a i) - ∑ i, Pi.single (u i) (a i).

theorem Equiv.Perm.IsCycle.exists_mul_zpow_inv_apply_eq_of_commute {α : Type u_1} [Fintype α] [DecidableEq α] {g t : Perm α} (hgc : g.IsCycle) (htg : Commute t g) : ∃ (j : ℤ), (∀ z ∈ g.support, (t * (g ^ j)⁻¹) z = z) ∧ ∀ z ∉ g.support, (t * (g ^ j)⁻¹) z = t z

A permutation commuting with a cycle can be corrected by a power of that cycle to fix its support pointwise, without changing it outside the support.

@[simp]

theorem Equiv.Perm.sameCycle_permCongr {α : Type u_1} (σ : Perm α) {β : Type u_2} (e : α ≃ β) {x y : α} : (e.permCongr σ).SameCycle (e x) (e y) ↔ σ.SameCycle x y

Transporting a permutation along an equivalence transports its cycles.

theorem Equiv.Perm.sameCycle_permCongr_iff {α : Type u_1} (σ : Perm α) {β : Type u_2} (e : α ≃ β) {x y : β} : (e.permCongr σ).SameCycle x y ↔ σ.SameCycle (e.symm x) (e.symm y)

The cycles of a permutation transported along an equivalence are the transported cycles: two points lie in the same cycle of e.permCongr σ exactly when their preimages under e lie in the same cycle of σ.

theorem Equiv.Perm.IsCycleOn.permCongr {α : Type u_1} {σ : Perm α} {β : Type u_2} (e : α ≃ β) {s : Set α} (h : σ.IsCycleOn s) : (e.permCongr σ).IsCycleOn (⇑e '' s)

Transporting a permutation along an equivalence transports its cycles on a set: the analogue of Equiv.Perm.IsCycleOn.conj for an equivalence between two types.

theorem Equiv.isCycleOn_mulRight_univ_iff {G : Type u_1} [Group G] {a : G} : (Equiv.mulRight a).IsCycleOn _root_.Set.univ ↔ Subgroup.zpowers a = ⊤

Right multiplication by a is a single cycle on the whole group exactly when a generates the group.

theorem Equiv.isCycleOn_addRight_univ_iff {G : Type u_1} [AddGroup G] {a : G} : (Equiv.addRight a).IsCycleOn _root_.Set.univ ↔ AddSubgroup.zmultiples a = ⊤

Right addition of a is a single cycle on the whole group exactly when a generates the group.

def TauCeti.invariantColouringEquiv {α : Type u_1} {σ : Type u_2} (π : Equiv.Perm α) : (Quotient (Equiv.Perm.SameCycle.setoid π) → σ) ≃ { f : α → σ // f ∘ ⇑π = f }

Colourings fixed by a permutation are exactly the colourings of its cycles.

Equations

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

@[simp]

theorem TauCeti.invariantColouringEquiv_apply_coe {α : Type u_1} {σ : Type u_2} (π : Equiv.Perm α) (g : Quotient (Equiv.Perm.SameCycle.setoid π) → σ) (a : α) : ↑((invariantColouringEquiv π) g) a = g ⟦a⟧

The colouring corresponding to a map on cycles evaluates at the cycle containing the point.

@[simp]

theorem TauCeti.invariantColouringEquiv_symm_apply {α : Type u_1} {σ : Type u_2} (π : Equiv.Perm α) (f : { f : α → σ // f ∘ ⇑π = f }) (a : α) : (invariantColouringEquiv π).symm f ⟦a⟧ = ↑f a

The map on cycles corresponding to an invariant colouring evaluates at a cycle by evaluating the colouring at any point in that cycle.

theorem TauCeti.card_filter_comp_perm {α : Type u_1} {ι : Type u_3} [Fintype α] [DecidableEq ι] (f : α → ι) (g : Equiv.Perm α) (i : ι) : {a : α | f (g a) = i}.card = {a : α | f a = i}.card

Precomposing a function with a permutation preserves the cardinality of each fiber.

theorem TauCeti.swap_apply_notMem {α : Type u_3} [DecidableEq α] {s : Finset α} {a b z : α} (ha : a ∉ s) (hb : b ∉ s) (hz : z ∉ s) : (Equiv.swap a b) z ∉ s

A transposition of two points outside s maps the complement of s to itself.

theorem TauCeti.exists_pair_perm_fixed {α : Type u_3} {s : Set α} {i j i' j' : α} (hij : i ≠ j) (hi'j' : i' ≠ j') (hi : i ∉ s) (hj : j ∉ s) (hi' : i' ∉ s) (hj' : j' ∉ s) : ∃ (perm : Equiv.Perm α), (∀ a ∈ s, perm a = a) ∧ perm i = i' ∧ perm j = j'

Any ordered pair of distinct points outside s can be carried to another such pair by a permutation fixing s pointwise.

theorem TauCeti.sameCycle_toPerm_iff {α : Type u_3} (f : α → α) (hf : Function.Involutive f) (a b : α) : (Function.Involutive.toPerm f hf).SameCycle a b ↔ a = b ∨ a = f b

Two points lie in the same orbit of an involution exactly when they are equal or one is the image of the other.

theorem TauCeti.card_support_add_one_eq_card_iff_existsUnique_fixedPoint {α : Type u_3} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : σ.support.card + 1 = Fintype.card α ↔ ∃! x : α, σ x = x

A permutation moves all but one point exactly when it has a unique fixed point.

theorem TauCeti.swap_braid {α : Type u_4} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hcb : c ≠ b) : Equiv.swap a b * Equiv.swap b c * Equiv.swap a b = Equiv.swap b c * Equiv.swap a b * Equiv.swap b c

Whenever a and c are both distinct from b, the transpositions (a b) and (b c) satisfy the braid relation. The two points a and c need not be distinct: for a = c both sides are (a b).

@[simp]

theorem TauCeti.swap_mul_swap_apply_left {α : Type u_4} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hca : c ≠ a) : (Equiv.swap a b * Equiv.swap b c) a = b

The product Equiv.swap a b * Equiv.swap b c of two transpositions sharing the point b carries a to b. Together with TauCeti.swap_mul_swap_apply_middle and TauCeti.swap_mul_swap_apply_right this evaluates that product, which for three distinct points is the three-cycle a ↦ b ↦ c ↦ a, at each of the three points it moves.

@[simp]

theorem TauCeti.swap_mul_swap_apply_middle {α : Type u_4} [DecidableEq α] {a b c : α} (hca : c ≠ a) (hcb : c ≠ b) : (Equiv.swap a b * Equiv.swap b c) b = c

The product Equiv.swap a b * Equiv.swap b c of two transpositions sharing the point b carries b to c, the point the second transposition moves it to.

@[simp]

theorem TauCeti.swap_mul_swap_apply_right {α : Type u_4} [DecidableEq α] (a b c : α) : (Equiv.swap a b * Equiv.swap b c) c = a

The product Equiv.swap a b * Equiv.swap b c of two transpositions sharing the point b carries c to a, through the shared point b; no distinctness is needed for this value.

theorem TauCeti.exists_perm_apply_eq {α : Type u_4} {γ : Type u_5} {e : α → γ} (he : Function.Injective e) (σ : Equiv.Perm α) : ∃ (ρ : Equiv.Perm γ), ∀ (a : α), ρ (e a) = e (σ a)

A permutation along an injection extends to a permutation of the ambient type. Given an injection e : α → γ, every permutation σ of α is realized along e by some ρ : Equiv.Perm γ. This is Equiv.Perm.viaEmbedding stated in terms of the underlying function of the injection, which is the form a consumer reindexing along e needs.

theorem TauCeti.exists_perm_apply_eq_of_disjoint_range {α : Type u_4} {β : Type u_5} {γ : Type u_6} {e : α → γ} {f : β → γ} (he : Function.Injective e) (hf : Function.Injective f) (hd : Disjoint (Set.range e) (Set.range f)) (σ : Equiv.Perm α) (τ : Equiv.Perm β) : ∃ (ρ : Equiv.Perm γ), (∀ (a : α), ρ (e a) = e (σ a)) ∧ ∀ (b : β), ρ (f b) = f (τ b)

Two permutations along disjoint injections extend to one permutation of the ambient type. Given injections e : α → γ and f : β → γ with disjoint ranges, every pair of permutations σ of α and τ of β is realized by a single ρ : Equiv.Perm γ which acts as σ along e and as τ along f.