# Documentation

Mathlib.GroupTheory.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.IsSwap: f = swap x y for x ≠ y≠ y.
• Equiv.Perm.support: the elements x : α that are not fixed by f.
def Equiv.Perm.Disjoint {α : Type u_1} (f : ) (g : ) :

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
• = ∀ (x : α), f x = x g x = x
theorem Equiv.Perm.Disjoint.symm {α : Type u_1} {f : } {g : } :
theorem Equiv.Perm.Disjoint.symmetric {α : Type u_1} :
Symmetric Equiv.Perm.Disjoint
instance Equiv.Perm.instIsSymmPermDisjoint {α : Type u_1} :
IsSymm () Equiv.Perm.Disjoint
Equations
theorem Equiv.Perm.disjoint_comm {α : Type u_1} {f : } {g : } :
theorem Equiv.Perm.Disjoint.commute {α : Type u_1} {f : } {g : } (h : ) :
@[simp]
theorem Equiv.Perm.disjoint_one_left {α : Type u_1} (f : ) :
@[simp]
theorem Equiv.Perm.disjoint_one_right {α : Type u_1} (f : ) :
theorem Equiv.Perm.disjoint_iff_eq_or_eq {α : Type u_1} {f : } {g : } :
∀ (x : α), f x = x g x = x
@[simp]
theorem Equiv.Perm.disjoint_refl_iff {α : Type u_1} {f : } :
f = 1
theorem Equiv.Perm.Disjoint.inv_left {α : Type u_1} {f : } {g : } (h : ) :
theorem Equiv.Perm.Disjoint.inv_right {α : Type u_1} {f : } {g : } (h : ) :
@[simp]
theorem Equiv.Perm.disjoint_inv_left_iff {α : Type u_1} {f : } {g : } :
@[simp]
theorem Equiv.Perm.disjoint_inv_right_iff {α : Type u_1} {f : } {g : } :
theorem Equiv.Perm.Disjoint.mul_left {α : Type u_1} {f : } {g : } {h : } (H1 : ) (H2 : ) :
theorem Equiv.Perm.Disjoint.mul_right {α : Type u_1} {f : } {g : } {h : } (H1 : ) (H2 : ) :
theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : } (l : List ()) (h : ∀ (g : ), g l) :
theorem Equiv.Perm.disjoint_prod_perm {α : Type u_1} {l₁ : List ()} {l₂ : List ()} (hl : List.Pairwise Equiv.Perm.Disjoint l₁) (hp : l₁ ~ l₂) :
=
theorem Equiv.Perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : List ()} (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 : } {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 : } {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 : } {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 : } {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} {σ : } {τ : } (hστ : ) {a : α} :
↑(σ * τ) a = a σ a = a τ a = a
theorem Equiv.Perm.Disjoint.mul_eq_one_iff {α : Type u_1} {σ : } {τ : } (hστ : ) :
σ * τ = 1 σ = 1 τ = 1
theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow {α : Type u_1} {σ : } {τ : } (hστ : ) (m : ) (n : ) :
Equiv.Perm.Disjoint (σ ^ m) (τ ^ n)
theorem Equiv.Perm.Disjoint.pow_disjoint_pow {α : Type u_1} {σ : } {τ : } (hστ : ) (m : ) (n : ) :
Equiv.Perm.Disjoint (σ ^ m) (τ ^ n)
def Equiv.Perm.IsSwap {α : Type u_1} [inst : ] (f : ) :

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 : ] {p : αProp} [inst : ] (x : ) (y : ) :
Equiv.Perm.ofSubtype () = Equiv.swap x y
theorem Equiv.Perm.IsSwap.of_subtype_isSwap {α : Type u_1} [inst : ] {p : αProp} [inst : ] {f : } (h : ) :
Equiv.Perm.IsSwap (Equiv.Perm.ofSubtype f)
theorem Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [inst : ] {f : } {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 : ) :
{ x | p⁻¹ x x } = { x | p x x }
theorem Equiv.Perm.set_support_apply_mem {α : Type u_1} {p : } {a : α} :
p a { x | p x x } a { x | p x x }
theorem Equiv.Perm.set_support_zpow_subset {α : Type u_1} (p : ) (n : ) :
{ x | ↑(p ^ n) x x } { x | p x x }
theorem Equiv.Perm.set_support_mul_subset {α : Type u_1} (p : ) (q : ) :
{ x | ↑(p * q) x x } { x | p x x } { x | q x x }
def Equiv.Perm.support {α : Type u_1} [inst : ] [inst : ] (f : ) :

The Finset of nonfixed points of a permutation.

Equations
@[simp]
theorem Equiv.Perm.mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {x : α} :
f x x
theorem Equiv.Perm.not_mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {x : α} :
¬ f x = x
theorem Equiv.Perm.coe_support_eq_set_support {α : Type u_1} [inst : ] [inst : ] (f : ) :
↑() = { x | f x x }
@[simp]
theorem Equiv.Perm.support_eq_empty_iff {α : Type u_1} [inst : ] [inst : ] {σ : } :
σ = 1
@[simp]
theorem Equiv.Perm.support_one {α : Type u_1} [inst : ] [inst : ] :
@[simp]
theorem Equiv.Perm.support_refl {α : Type u_1} [inst : ] [inst : ] :
theorem Equiv.Perm.support_congr {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ) (h' : ∀ (x : α), f x = g x) :
f = g
theorem Equiv.Perm.support_mul_le {α : Type u_1} [inst : ] [inst : ] (f : ) (g : ) :
theorem Equiv.Perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [inst : ] [inst : ] {l : List ()} {x : α} (hx : ) :
f, f l
theorem Equiv.Perm.support_pow_le {α : Type u_1} [inst : ] [inst : ] (σ : ) (n : ) :
@[simp]
theorem Equiv.Perm.support_inv {α : Type u_1} [inst : ] [inst : ] (σ : ) :
theorem Equiv.Perm.apply_mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {x : α} :
f x
@[simp]
theorem Equiv.Perm.apply_pow_apply_eq_iff {α : Type u_1} (f : ) (n : ) {x : α} :
f (↑(f ^ n) x) = ↑(f ^ n) x f x = x
theorem Equiv.Perm.pow_apply_mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {n : } {x : α} :
↑(f ^ n) x
@[simp]
theorem Equiv.Perm.apply_zpow_apply_eq_iff {α : Type u_1} (f : ) (n : ) {x : α} :
f (↑(f ^ n) x) = ↑(f ^ n) x f x = x
theorem Equiv.Perm.zpow_apply_mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {n : } {x : α} :
↑(f ^ n) x
theorem Equiv.Perm.pow_eq_on_of_mem_support {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ∀ (x : α), f x = g x) (k : ) (x : α) :
↑(f ^ k) x = ↑(g ^ k) x
theorem Equiv.Perm.disjoint_iff_disjoint_support {α : Type u_1} [inst : ] [inst : ] {f : } {g : } :
theorem Equiv.Perm.Disjoint.disjoint_support {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ) :
theorem Equiv.Perm.Disjoint.support_mul {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ) :
theorem Equiv.Perm.support_prod_of_pairwise_disjoint {α : Type u_1} [inst : ] [inst : ] (l : List ()) (h : List.Pairwise Equiv.Perm.Disjoint 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 : ] [inst : ] (l : List ()) :
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 : ] [inst : ] (σ : ) (n : ) :
@[simp]
theorem Equiv.Perm.support_swap {α : Type u_1} [inst : ] [inst : ] {x : α} {y : α} (h : x y) :
= {x, y}
theorem Equiv.Perm.support_swap_iff {α : Type u_1} [inst : ] [inst : ] (x : α) (y : α) :
= {x, y} x y
theorem Equiv.Perm.support_swap_mul_swap {α : Type u_1} [inst : ] [inst : ] {x : α} {y : α} {z : α} (h : List.Nodup [x, y, z]) :
Equiv.Perm.support ( * ) = {x, y, z}
theorem Equiv.Perm.support_swap_mul_ge_support_diff {α : Type u_1} [inst : ] [inst : ] (f : ) (x : α) (y : α) :
\ {x, y} Equiv.Perm.support ( * f)
theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [inst : ] [inst : ] (f : ) (x : α) (h : f (f x) x) :
Equiv.Perm.support (Equiv.swap x (f x) * f) = \ {x}
theorem Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [inst : ] [inst : ] {f : } {x : α} {y : α} (hy : y Equiv.Perm.support (Equiv.swap x (f x) * f)) :
y x
theorem Equiv.Perm.Disjoint.mem_imp {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ) {x : α} (hx : ) :
theorem Equiv.Perm.eq_on_support_mem_disjoint {α : Type u_1} [inst : ] [inst : ] {f : } {l : List ()} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) (x : α) :
f x = ↑() x
theorem Equiv.Perm.Disjoint.mono {α : Type u_1} [inst : ] [inst : ] {f : } {g : } {x : } {y : } (h : ) (hf : ) (hg : ) :
theorem Equiv.Perm.support_le_prod_of_mem {α : Type u_1} [inst : ] [inst : ] {f : } {l : List ()} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) :
@[simp]
theorem Equiv.Perm.support_extend_domain {α : Type u_1} [inst : ] [inst : ] {β : Type u_2} [inst : ] [inst : ] {p : βProp} [inst : ] (f : α ) {g : } :
theorem Equiv.Perm.card_support_extend_domain {α : Type u_1} [inst : ] [inst : ] {β : Type u_2} [inst : ] [inst : ] {p : βProp} [inst : ] (f : α ) {g : } :
theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [inst : ] [inst : ] {f : } :
f = 1
theorem Equiv.Perm.one_lt_card_support_of_ne_one {α : Type u_1} [inst : ] [inst : ] {f : } (h : f 1) :
theorem Equiv.Perm.card_support_ne_one {α : Type u_1} [inst : ] [inst : ] (f : ) :
@[simp]
theorem Equiv.Perm.card_support_le_one {α : Type u_1} [inst : ] [inst : ] {f : } :
f = 1
theorem Equiv.Perm.two_le_card_support_of_ne_one {α : Type u_1} [inst : ] [inst : ] {f : } (h : f 1) :
theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [inst : ] [inst : ] {f : } {x : α} (hx : f x x) :
theorem Equiv.Perm.card_support_swap {α : Type u_1} [inst : ] [inst : ] {x : α} {y : α} (hxy : x y) :
= 2
@[simp]
theorem Equiv.Perm.card_support_eq_two {α : Type u_1} [inst : ] [inst : ] {f : } :
theorem Equiv.Perm.Disjoint.card_support_mul {α : Type u_1} [inst : ] [inst : ] {f : } {g : } (h : ) :
theorem Equiv.Perm.card_support_prod_list_of_pairwise_disjoint {α : Type u_1} [inst : ] [inst : ] {l : List ()} (h : List.Pairwise Equiv.Perm.Disjoint l) :
= List.sum (List.map (Finset.card Equiv.Perm.support) l)
@[simp]
theorem Equiv.Perm.support_subtype_perm {α : Type u_1} [inst : ] {s : } (f : ) (h : ∀ (x : α), x s f x s) :
= Finset.filter (fun x => decide (f x x) = true) ()