Permutations on Fintype
s #
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.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
@[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 ⋯
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.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.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 σ))
:
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)
: