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}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
{τ : Equiv.Perm α}
(f : { x : α // x ∈ ↑(Equiv.Perm.support σ) } ≃ { x : α // x ∈ ↑(Equiv.Perm.support τ) })
(hf : ∀ (x : α) (hx : x ∈ ↑(Equiv.Perm.support σ)), ↑(f { val := σ x, property := ⋯ }) = τ ↑(f { val := x, property := 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)
@[inline, reducible]
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
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 })
:
(Equiv.Perm.subtypePermOfFintype f h) x = { val := f ↑x, property := ⋯ }
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))
:
σ ∈ MonoidHom.range (Equiv.Perm.sumCongrHom m n)
theorem
Equiv.Perm.Disjoint.orderOf
{α : Type u}
{σ : Equiv.Perm α}
{τ : Equiv.Perm α}
(hστ : Equiv.Perm.Disjoint σ τ)
:
theorem
Equiv.Perm.Disjoint.extendDomain
{α : Type u}
{β : Type v}
{p : β → Prop}
[DecidablePred p]
(f : α ≃ Subtype p)
{σ : Equiv.Perm α}
{τ : Equiv.Perm α}
(h : Equiv.Perm.Disjoint σ τ)
:
theorem
Equiv.Perm.Disjoint.isConj_mul
{α : Type u}
[Finite α]
{σ : Equiv.Perm α}
{τ : Equiv.Perm α}
{π : Equiv.Perm α}
{ρ : Equiv.Perm α}
(hc1 : IsConj σ π)
(hc2 : IsConj τ ρ)
(hd1 : Equiv.Perm.Disjoint σ τ)
(hd2 : Equiv.Perm.Disjoint π ρ)
:
theorem
Equiv.Perm.support_pow_coprime
{α : Type u}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
{n : ℕ}
(h : Nat.Coprime n (orderOf σ))
:
Equiv.Perm.support (σ ^ n) = Equiv.Perm.support σ