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_symm_on_of_perm_on_finset {α : Type u} {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α} (hy : y ∈ s) : (Equiv.symm f) y ∈ s

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

@[simp]

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

theorem Equiv.Perm.perm_symm_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 ((Equiv.symm 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.apply_mem_fixedPoints_iff_mem_of_mem_centralizer {α : Type u} {g p : Perm α} (hp : p ∈ Subgroup.centralizer {g}) {x : α} : p x ∈ Function.fixedPoints ⇑g ↔ 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

theorem Equiv.Perm.ofSubtype_support_disjoint {α : Type u} [DecidableEq α] [Fintype α] {σ : Perm α} (x : Perm ↑(Function.fixedPoints ⇑σ)) : _root_.Disjoint (ofSubtype x).support σ.support

theorem Equiv.Perm.disjoint_of_disjoint_support {α : Type u} [DecidableEq α] [Fintype α] {H K : Subgroup (Perm α)} (h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support) : _root_.Disjoint H K

theorem Equiv.Perm.support_closure_subset_union {α : Type u} [DecidableEq α] [Fintype α] (S : Set (Perm α)) (a : Perm α) : a ∈ Subgroup.closure S → ↑a.support ⊆ ⋃ b ∈ S, ↑b.support

theorem Equiv.Perm.disjoint_support_closure_of_disjoint_support {α : Type u} [DecidableEq α] [Fintype α] {S T : Set (Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) (a : Perm α) : a ∈ Subgroup.closure S → ∀ b ∈ Subgroup.closure T, _root_.Disjoint a.support b.support

theorem Equiv.Perm.disjoint_closure_of_disjoint_support {α : Type u} [DecidableEq α] [Fintype α] {S T : Set (Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) : _root_.Disjoint (Subgroup.closure S) (Subgroup.closure T)

theorem Equiv.Perm.mem_range_ofSubtype_iff {α : Type u} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] {g : Perm α} : g ∈ ofSubtype.range ↔ ↑g.support ⊆ Set.ofPred p