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 α}
(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 : ∀ x ∈ s, f x ∈ s)
{y : α}
(hy : 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 x → p (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 x → p (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 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))
:
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))
:
σ ∈ (Equiv.Perm.sumCongrHom m n).range
theorem
Equiv.Perm.Disjoint.extendDomain
{α : Type u}
{β : Type v}
{p : β → Prop}
[DecidablePred p]
(f : α ≃ Subtype p)
{σ τ : Equiv.Perm α}
(h : σ.Disjoint τ)
:
(σ.extendDomain f).Disjoint (τ.extendDomain f)
theorem
Equiv.Perm.Disjoint.isConj_mul
{α : Type u}
[Finite α]
{σ τ π ρ : Equiv.Perm α}
(hc1 : IsConj σ π)
(hc2 : IsConj τ ρ)
(hd1 : σ.Disjoint τ)
(hd2 : π.Disjoint ρ)
:
theorem
Equiv.Perm.mem_fixedPoints_iff_apply_mem_of_mem_centralizer
{α : Type u}
{g p : Equiv.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 : Equiv.Perm α}
(u : Equiv.Perm ↑(Function.fixedPoints ⇑g))
:
(Equiv.Perm.ofSubtype u).Disjoint g
theorem
Equiv.Perm.support_pow_coprime
{α : Type u}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
{n : ℕ}
(h : n.Coprime (orderOf σ))
: