Documentation

Mathlib.GroupTheory.Perm.Support

support of a permutation #

Main definitions #

In the following, f g : Equiv.Perm α.

def Equiv.Perm.Disjoint {α : Type u_1} (f : Equiv.Perm α) (g : Equiv.Perm α) :

Two permutations f and g are Disjoint if their supports are disjoint, i.e., every element is fixed either by f, or by g.

Equations
theorem Equiv.Perm.Disjoint.symmetric {α : Type u_1} :
Symmetric Equiv.Perm.Disjoint
theorem Equiv.Perm.disjoint_iff_eq_or_eq {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} :
Equiv.Perm.Disjoint f g ∀ (x : α), f x = x g x = x
@[simp]
theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : Equiv.Perm α} (l : List (Equiv.Perm α)) (h : ∀ (g : Equiv.Perm α), g lEquiv.Perm.Disjoint f g) :
theorem Equiv.Perm.disjoint_prod_perm {α : Type u_1} {l₁ : List (Equiv.Perm α)} {l₂ : List (Equiv.Perm α)} (hl : List.Pairwise Equiv.Perm.Disjoint l₁) (hp : l₁ ~ l₂) :
theorem Equiv.Perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : List (Equiv.Perm α)} (h1 : ¬1 l) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
theorem Equiv.Perm.pow_apply_eq_self_of_apply_eq_self {α : Type u_1} {f : Equiv.Perm α} {x : α} (hfx : f x = x) (n : ) :
↑(f ^ n) x = x
theorem Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self {α : Type u_1} {f : Equiv.Perm α} {x : α} (hfx : f x = x) (n : ) :
↑(f ^ n) x = x
theorem Equiv.Perm.pow_apply_eq_of_apply_apply_eq_self {α : Type u_1} {f : Equiv.Perm α} {x : α} (hffx : f (f x) = x) (n : ) :
↑(f ^ n) x = x ↑(f ^ n) x = f x
theorem Equiv.Perm.zpow_apply_eq_of_apply_apply_eq_self {α : Type u_1} {f : Equiv.Perm α} {x : α} (hffx : f (f x) = x) (i : ) :
↑(f ^ i) x = x ↑(f ^ i) x = f x
theorem Equiv.Perm.Disjoint.mul_apply_eq_iff {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) {a : α} :
↑(σ * τ) a = a σ a = a τ a = a
theorem Equiv.Perm.Disjoint.mul_eq_one_iff {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) :
σ * τ = 1 σ = 1 τ = 1
theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) (m : ) (n : ) :
Equiv.Perm.Disjoint (σ ^ m) (τ ^ n)
theorem Equiv.Perm.Disjoint.pow_disjoint_pow {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) (m : ) (n : ) :
Equiv.Perm.Disjoint (σ ^ m) (τ ^ n)
def Equiv.Perm.IsSwap {α : Type u_1} [inst : DecidableEq α] (f : Equiv.Perm α) :

f.IsSwap indicates that the permutation f is a transposition of two elements.

Equations
@[simp]
theorem Equiv.Perm.ofSubtype_swap_eq {α : Type u_1} [inst : DecidableEq α] {p : αProp} [inst : DecidablePred p] (x : Subtype p) (y : Subtype p) :
Equiv.Perm.ofSubtype (Equiv.swap x y) = Equiv.swap x y
theorem Equiv.Perm.IsSwap.of_subtype_isSwap {α : Type u_1} [inst : DecidableEq α] {p : αProp} [inst : DecidablePred p] {f : Equiv.Perm (Subtype p)} (h : Equiv.Perm.IsSwap f) :
Equiv.Perm.IsSwap (Equiv.Perm.ofSubtype f)
theorem Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [inst : DecidableEq α] {f : Equiv.Perm α} {x : α} {y : α} (hy : ↑(Equiv.swap x (f x) * f) y y) :
f y y y x
theorem Equiv.Perm.set_support_inv_eq {α : Type u_1} (p : Equiv.Perm α) :
{ x | p⁻¹ x x } = { x | p x x }
theorem Equiv.Perm.set_support_apply_mem {α : Type u_1} {p : Equiv.Perm α} {a : α} :
p a { x | p x x } a { x | p x x }
theorem Equiv.Perm.set_support_zpow_subset {α : Type u_1} (p : Equiv.Perm α) (n : ) :
{ x | ↑(p ^ n) x x } { x | p x x }
theorem Equiv.Perm.set_support_mul_subset {α : Type u_1} (p : Equiv.Perm α) (q : Equiv.Perm α) :
{ x | ↑(p * q) x x } { x | p x x } { x | q x x }
def Equiv.Perm.support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (f : Equiv.Perm α) :

The Finset of nonfixed points of a permutation.

Equations
@[simp]
theorem Equiv.Perm.mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {x : α} :
theorem Equiv.Perm.not_mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {x : α} :
theorem Equiv.Perm.coe_support_eq_set_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (f : Equiv.Perm α) :
↑(Equiv.Perm.support f) = { x | f x x }
@[simp]
theorem Equiv.Perm.support_eq_empty_iff {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {σ : Equiv.Perm α} :
@[simp]
theorem Equiv.Perm.support_one {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] :
@[simp]
theorem Equiv.Perm.support_refl {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] :
theorem Equiv.Perm.support_congr {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.support f Equiv.Perm.support g) (h' : ∀ (x : α), x Equiv.Perm.support gf x = g x) :
f = g
theorem Equiv.Perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {l : List (Equiv.Perm α)} {x : α} (hx : x Equiv.Perm.support (List.prod l)) :
f, f l x Equiv.Perm.support f
theorem Equiv.Perm.support_pow_le {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (σ : Equiv.Perm α) (n : ) :
@[simp]
theorem Equiv.Perm.support_inv {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (σ : Equiv.Perm α) :
theorem Equiv.Perm.apply_mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {x : α} :
@[simp]
theorem Equiv.Perm.apply_pow_apply_eq_iff {α : Type u_1} (f : Equiv.Perm α) (n : ) {x : α} :
f (↑(f ^ n) x) = ↑(f ^ n) x f x = x
theorem Equiv.Perm.pow_apply_mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {n : } {x : α} :
@[simp]
theorem Equiv.Perm.apply_zpow_apply_eq_iff {α : Type u_1} (f : Equiv.Perm α) (n : ) {x : α} :
f (↑(f ^ n) x) = ↑(f ^ n) x f x = x
theorem Equiv.Perm.zpow_apply_mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {n : } {x : α} :
theorem Equiv.Perm.pow_eq_on_of_mem_support {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : ∀ (x : α), x Equiv.Perm.support f Equiv.Perm.support gf x = g x) (k : ) (x : α) :
x Equiv.Perm.support f Equiv.Perm.support g↑(f ^ k) x = ↑(g ^ k) x
theorem Equiv.Perm.support_prod_of_pairwise_disjoint {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (l : List (Equiv.Perm α)) (h : List.Pairwise Equiv.Perm.Disjoint l) :
Equiv.Perm.support (List.prod l) = List.foldr (fun x x_1 => x x_1) (List.map Equiv.Perm.support l)
theorem Equiv.Perm.support_prod_le {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (l : List (Equiv.Perm α)) :
Equiv.Perm.support (List.prod l) List.foldr (fun x x_1 => x x_1) (List.map Equiv.Perm.support l)
theorem Equiv.Perm.support_zpow_le {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (σ : Equiv.Perm α) (n : ) :
@[simp]
theorem Equiv.Perm.support_swap {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {x : α} {y : α} (h : x y) :
theorem Equiv.Perm.support_swap_iff {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (x : α) (y : α) :
theorem Equiv.Perm.support_swap_mul_swap {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {x : α} {y : α} {z : α} (h : List.Nodup [x, y, z]) :
theorem Equiv.Perm.support_swap_mul_ge_support_diff {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (f : Equiv.Perm α) (x : α) (y : α) :
theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] (f : Equiv.Perm α) (x : α) (h : f (f x) x) :
theorem Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {x : α} {y : α} (hy : y Equiv.Perm.support (Equiv.swap x (f x) * f)) :
theorem Equiv.Perm.Disjoint.mem_imp {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) {x : α} (hx : x Equiv.Perm.support f) :
theorem Equiv.Perm.eq_on_support_mem_disjoint {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {l : List (Equiv.Perm α)} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) (x : α) :
x Equiv.Perm.support ff x = ↑(List.prod l) x
theorem Equiv.Perm.support_le_prod_of_mem {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {l : List (Equiv.Perm α)} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) :
@[simp]
theorem Equiv.Perm.support_extend_domain {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {β : Type u_2} [inst : DecidableEq β] [inst : Fintype β] {p : βProp} [inst : DecidablePred p] (f : α Subtype p) {g : Equiv.Perm α} :
theorem Equiv.Perm.card_support_extend_domain {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {β : Type u_2} [inst : DecidableEq β] [inst : Fintype β] {p : βProp} [inst : DecidablePred p] (f : α Subtype p) {g : Equiv.Perm α} :
theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} :
theorem Equiv.Perm.one_lt_card_support_of_ne_one {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} (h : f 1) :
@[simp]
theorem Equiv.Perm.card_support_le_one {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} :
theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {f : Equiv.Perm α} {x : α} (hx : f x x) :
theorem Equiv.Perm.card_support_swap {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {x : α} {y : α} (hxy : x y) :
theorem Equiv.Perm.card_support_prod_list_of_pairwise_disjoint {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {l : List (Equiv.Perm α)} (h : List.Pairwise Equiv.Perm.Disjoint l) :
Finset.card (Equiv.Perm.support (List.prod l)) = List.sum (List.map (Finset.card Equiv.Perm.support) l)
@[simp]
theorem Equiv.Perm.support_subtype_perm {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (f : Equiv.Perm α) (h : ∀ (x : α), x s f x s) :