# mathlibdocumentation

group_theory.perm.support

# Support of a permutation #

## Main definitions #

In the following, f g : equiv.perm α.

• equiv.perm.disjoint: two permutations f and g are disjoint if every element is fixed either by f, or by g. Equivalently, f and g are disjoint iff their support are disjoint.
• equiv.perm.is_swap: f = swap x y for x ≠ y.
• equiv.perm.support: the elements x : α that are not fixed by f.
def equiv.perm.disjoint {α : Type u_1} (f g : equiv.perm α) :
Prop

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
@[symm]
theorem equiv.perm.disjoint.symm {α : Type u_1} {f g : equiv.perm α} :
f.disjoint gg.disjoint f
theorem equiv.perm.disjoint.symmetric {α : Type u_1} :
theorem equiv.perm.disjoint_comm {α : Type u_1} {f g : equiv.perm α} :
theorem equiv.perm.disjoint.commute {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
g
@[simp]
theorem equiv.perm.disjoint_one_left {α : Type u_1} (f : equiv.perm α) :
@[simp]
theorem equiv.perm.disjoint_one_right {α : Type u_1} (f : equiv.perm α) :
theorem equiv.perm.disjoint_iff_eq_or_eq {α : Type u_1} {f g : equiv.perm α} :
f.disjoint g ∀ (x : α), f x = x g x = x
@[simp]
theorem equiv.perm.disjoint_refl_iff {α : Type u_1} {f : equiv.perm α} :
f.disjoint f f = 1
theorem equiv.perm.disjoint.inv_left {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.disjoint.inv_right {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
@[simp]
theorem equiv.perm.disjoint_inv_left_iff {α : Type u_1} {f g : equiv.perm α} :
@[simp]
theorem equiv.perm.disjoint_inv_right_iff {α : Type u_1} {f g : equiv.perm α} :
theorem equiv.perm.disjoint.mul_left {α : Type u_1} {f g h : equiv.perm α} (H1 : f.disjoint h) (H2 : g.disjoint h) :
(f * g).disjoint h
theorem equiv.perm.disjoint.mul_right {α : Type u_1} {f g h : equiv.perm α} (H1 : f.disjoint g) (H2 : f.disjoint h) :
f.disjoint (g * h)
theorem equiv.perm.disjoint_prod_right {α : Type u_1} {f : equiv.perm α} (l : list (equiv.perm α)) (h : ∀ (g : , g lf.disjoint g) :
theorem equiv.perm.disjoint_prod_perm {α : Type u_1} {l₁ l₂ : list (equiv.perm α)} (hl : l₁) (hp : l₁ ~ l₂) :
l₁.prod = l₂.prod
theorem equiv.perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : list (equiv.perm α)} (h1 : 1 l) (h2 : 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 α} (hστ : σ.disjoint τ) {a : α} :
* τ) a = a σ a = a τ a = a
theorem equiv.perm.disjoint.mul_eq_one_iff {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :
σ * τ = 1 σ = 1 τ = 1
theorem equiv.perm.disjoint.zpow_disjoint_zpow {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ) :
^ m).disjoint ^ n)
theorem equiv.perm.disjoint.pow_disjoint_pow {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ) :
^ m).disjoint ^ n)
def equiv.perm.is_swap {α : Type u_1} [decidable_eq α] (f : equiv.perm α) :
Prop

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

Equations
theorem equiv.perm.is_swap.of_subtype_is_swap {α : Type u_1} [decidable_eq α] {p : α → Prop} {f : equiv.perm (subtype p)} (h : f.is_swap) :
theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [decidable_eq α] {f : equiv.perm α} {x y : α} (hy : (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 q : equiv.perm α) :
{x : α | (p * q) x x} {x : α | p x x} {x : α | q x x}
def equiv.perm.support {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :

The finset of nonfixed points of a permutation.

Equations
@[simp]
theorem equiv.perm.mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
x f.support f x x
theorem equiv.perm.not_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
x f.support f x = x
theorem equiv.perm.coe_support_eq_set_support {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
(f.support) = {x : α | f x x}
@[simp]
theorem equiv.perm.support_eq_empty_iff {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} :
σ = 1
@[simp]
theorem equiv.perm.support_one {α : Type u_1} [decidable_eq α] [fintype α] :
@[simp]
theorem equiv.perm.support_refl {α : Type u_1} [decidable_eq α] [fintype α] :
theorem equiv.perm.support_congr {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.support g.support) (h' : ∀ (x : α), x g.supportf x = g x) :
f = g
theorem equiv.perm.support_mul_le {α : Type u_1} [decidable_eq α] [fintype α] (f g : equiv.perm α) :
theorem equiv.perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [decidable_eq α] [fintype α] {l : list (equiv.perm α)} {x : α} (hx : x l.prod.support) :
∃ (f : , f l x f.support
theorem equiv.perm.support_pow_le {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) (n : ) :
^ n).support σ.support
@[simp]
theorem equiv.perm.support_inv {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) :
@[simp]
theorem equiv.perm.apply_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
@[simp]
theorem equiv.perm.pow_apply_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {n : } {x : α} :
(f ^ n) x f.support x f.support
@[simp]
theorem equiv.perm.zpow_apply_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {n : } {x : α} :
(f ^ n) x f.support x f.support
theorem equiv.perm.pow_eq_on_of_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : ∀ (x : α), x f.support g.supportf x = g x) (k : ) (x : α) (H : x f.support g.support) :
(f ^ k) x = (g ^ k) x
theorem equiv.perm.disjoint_iff_disjoint_support {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} :
theorem equiv.perm.disjoint.disjoint_support {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.disjoint.support_mul {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.support_prod_of_pairwise_disjoint {α : Type u_1} [decidable_eq α] [fintype α] (l : list (equiv.perm α))  :
theorem equiv.perm.support_prod_le {α : Type u_1} [decidable_eq α] [fintype α] (l : list (equiv.perm α)) :
theorem equiv.perm.support_zpow_le {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) (n : ) :
^ n).support σ.support
@[simp]
theorem equiv.perm.support_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y : α} (h : x y) :
y).support = {x, y}
theorem equiv.perm.support_swap_iff {α : Type u_1} [decidable_eq α] [fintype α] (x y : α) :
y).support = {x, y} x y
theorem equiv.perm.support_swap_mul_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y z : α} (h : [x, y, z].nodup) :
y * z).support = {x, y, z}
theorem equiv.perm.support_swap_mul_ge_support_diff {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x y : α) :
f.support \ {x, y} y * f).support
theorem equiv.perm.support_swap_mul_eq {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (h : f (f x) x) :
(f x) * f).support = f.support \ {x}
theorem equiv.perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (hy : y (f x) * f).support) :
y f.support y x
theorem equiv.perm.disjoint.mem_imp {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) {x : α} (hx : x f.support) :
theorem equiv.perm.eq_on_support_mem_disjoint {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {l : list (equiv.perm α)} (h : f l) (hl : l) (x : α) (H : x f.support) :
f x = (l.prod) x
theorem equiv.perm.disjoint.mono {α : Type u_1} [decidable_eq α] [fintype α] {f g x y : equiv.perm α} (h : f.disjoint g) (hf : x.support f.support) (hg : y.support g.support) :
theorem equiv.perm.support_le_prod_of_mem {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {l : list (equiv.perm α)} (h : f l) (hl : l) :
@[simp]
theorem equiv.perm.support_extend_domain {α : Type u_1} [decidable_eq α] [fintype α] {β : Type u_2} [decidable_eq β] [fintype β] {p : β → Prop} (f : α ) {g : equiv.perm α} :
theorem equiv.perm.card_support_extend_domain {α : Type u_1} [decidable_eq α] [fintype α] {β : Type u_2} [decidable_eq β] [fintype β] {p : β → Prop} (f : α ) {g : equiv.perm α} :
@[simp]
theorem equiv.perm.card_support_eq_zero {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card = 0 f = 1
theorem equiv.perm.one_lt_card_support_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f 1) :
theorem equiv.perm.card_support_ne_one {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
@[simp]
theorem equiv.perm.card_support_le_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card 1 f = 1
theorem equiv.perm.two_le_card_support_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f 1) :
theorem equiv.perm.card_support_swap_mul {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hx : f x x) :
theorem equiv.perm.card_support_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y : α} (hxy : x y) :
y).support.card = 2
@[simp]
theorem equiv.perm.card_support_eq_two {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
theorem equiv.perm.disjoint.card_support_mul {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :