# Permutations on Fintypes #

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

theorem Equiv.Perm.isConj_of_support_equiv {α : Type u} [] [] {σ : } {τ : } (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 : } {f : } (h : xs, f x s) {y : α} (hy : y s) :
f⁻¹ y s
theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo {α : Type u} (f : ) {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 : } {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 : } {p : αProp} [Finite { x : α // p x }] (h : ∀ (x : α), p xp (f x)) {x : α} (hx : p x) :
p (f⁻¹ x)
@[reducible, inline]
abbrev Equiv.Perm.subtypePermOfFintype {α : Type u} (f : ) {p : αProp} [Finite { x : α // p x }] (h : ∀ (x : α), p xp (f x)) :
Equiv.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
Instances For
@[simp]
theorem Equiv.Perm.subtypePermOfFintype_apply {α : Type u} (f : ) {p : αProp} [Finite { x : α // p x }] (h : ∀ (x : α), p xp (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 xp (1 x)) :
theorem Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr {m : Type u_1} {n : Type u_2} [] [] (σ : Equiv.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} [] [] {σ : Equiv.Perm (m n)} (h : Set.MapsTo (σ) (Set.range Sum.inl) (Set.range Sum.inl)) :
σ ().range
theorem Equiv.Perm.Disjoint.orderOf {α : Type u} {σ : } {τ : } (hστ : σ.Disjoint τ) :
orderOf (σ * τ) = ().lcm ()
theorem Equiv.Perm.Disjoint.extendDomain {α : Type u} {β : Type v} {p : βProp} [] (f : α ) {σ : } {τ : } (h : σ.Disjoint τ) :
(σ.extendDomain f).Disjoint (τ.extendDomain f)
theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u} [] {σ : } {τ : } {π : } {ρ : } (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : σ.Disjoint τ) (hd2 : π.Disjoint ρ) :
IsConj (σ * τ) (π * ρ)
theorem Equiv.Perm.support_pow_coprime {α : Type u} [] [] {σ : } {n : } (h : n.Coprime ()) :
(σ ^ n).support = σ.support