Permutations on Fintypes

This file contains miscellaneous lemmas about Equiv.Perm and Equiv.swap, building on top of those in Mathlib/Logic/Equiv/Basic.lean and other files in Mathlib/GroupTheory/Perm/*.

theorem Equiv.Perm.isConj_of_support_equiv {α : Type u} [DecidableEq α] [Fintype α] {σ τ : Perm α} (f : { x : α // x ∈ ↑σ.support } ≃ { x : α // x ∈ ↑τ.support }) (hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)) : IsConj σ τ

theorem Equiv.Perm.perm_inv_on_of_perm_on_finset {α : Type u} {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α} (hy : y ∈ s) : f⁻¹ y ∈ s

theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo {α : Type u} (f : Perm α) {s : Set α} [Finite ↑s] (h : Set.MapsTo (⇑f) s s) : Set.MapsTo (⇑f⁻¹) s s

@[simp]

theorem Equiv.Perm.perm_inv_mapsTo_iff_mapsTo {α : Type u} {f : Perm α} {s : Set α} [Finite ↑s] : Set.MapsTo (⇑f⁻¹) s s ↔ Set.MapsTo (⇑f) s s

theorem Equiv.Perm.perm_inv_on_of_perm_on_finite {α : Type u} {f : Perm α} {p : α → Prop} [Finite { x : α // p x }] (h : ∀ (x : α), p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x)

@[reducible, inline]

abbrev Equiv.Perm.subtypePermOfFintype {α : Type u} (f : Perm α) {p : α → Prop} [Finite { x : α // p x }] (h : ∀ (x : α), p x → p (f x)) : Perm { x : α // p x }

If the permutation f maps {x // p x} into itself, then this returns the permutation on {x // p x} induced by f. Note that the h hypothesis is weaker than for Equiv.Perm.subtypePerm.

Equations

• f.subtypePermOfFintype h = f.subtypePerm ⋯

@[simp]

theorem Equiv.Perm.subtypePermOfFintype_apply {α : Type u} (f : Perm α) {p : α → Prop} [Finite { x : α // p x }] (h : ∀ (x : α), p x → p (f x)) (x : { x : α // p x }) : (f.subtypePermOfFintype h) x = ⟨f ↑x, ⋯⟩

theorem Equiv.Perm.subtypePermOfFintype_one {α : Type u} (p : α → Prop) [Finite { x : α // p x }] (h : ∀ (x : α), p x → p (1 x)) : subtypePermOfFintype 1 h = 1

theorem Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] (σ : Perm (m ⊕ n)) : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

theorem Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] {σ : Perm (m ⊕ n)} (h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)) : σ ∈ (sumCongrHom m n).range

theorem Equiv.Perm.Disjoint.orderOf {α : Type u} {σ τ : Perm α} (hστ : σ.Disjoint τ) : _root_.orderOf (σ * τ) = (_root_.orderOf σ).lcm (_root_.orderOf τ)

theorem Equiv.Perm.Disjoint.extendDomain {α : Type u} {β : Type v} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {σ τ : Perm α} (h : σ.Disjoint τ) : (σ.extendDomain f).Disjoint (τ.extendDomain f)

theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u} [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : σ.Disjoint τ) (hd2 : π.Disjoint ρ) : IsConj (σ * τ) (π * ρ)

theorem Equiv.Perm.mem_fixedPoints_iff_apply_mem_of_mem_centralizer {α : Type u} {g p : Perm α} (hp : p ∈ Subgroup.centralizer {g}) {x : α} : x ∈ Function.fixedPoints ⇑g ↔ p x ∈ Function.fixedPoints ⇑g

theorem Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self {α : Type u} [DecidableEq α] {g : Perm α} (u : Perm ↑(Function.fixedPoints ⇑g)) : (ofSubtype u).Disjoint g

theorem Equiv.Perm.support_pow_coprime {α : Type u} [DecidableEq α] [Fintype α] {σ : Perm α} {n : ℕ} (h : n.Coprime (orderOf σ)) : (σ ^ n).support = σ.support