Documentation

Mathlib.GroupTheory.Perm.Finite

Permutations on Fintypes #

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

theorem Equiv.Perm.isConj_of_support_equiv {α : Type u} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {τ : Equiv.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 : Equiv.Perm α} (h : xs, f x s) {y : α} (hy : y s) :
f⁻¹ y s
theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo {α : Type u} (f : Equiv.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 : Equiv.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 : Equiv.Perm α} {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 : Equiv.Perm α) {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 : Equiv.Perm α) {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} [Finite m] [Finite n] (σ : 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} [Finite m] [Finite n] {σ : Equiv.Perm (m n)} (h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)) :
    theorem Equiv.Perm.Disjoint.orderOf {α : Type u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : σ.Disjoint τ) :
    orderOf (σ * τ) = (orderOf σ).lcm (orderOf τ)
    theorem Equiv.Perm.Disjoint.extendDomain {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] (f : α Subtype p) {σ : Equiv.Perm α} {τ : Equiv.Perm α} (h : σ.Disjoint τ) :
    (σ.extendDomain f).Disjoint (τ.extendDomain f)
    theorem Equiv.Perm.Disjoint.isConj_mul {α : Type u} [Finite α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} {π : Equiv.Perm α} {ρ : Equiv.Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : σ.Disjoint τ) (hd2 : π.Disjoint ρ) :
    IsConj (σ * τ) (π * ρ)
    theorem Equiv.Perm.support_pow_coprime {α : Type u} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {n : } (h : n.Coprime (orderOf σ)) :
    (σ ^ n).support = σ.support