# 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.
• Equiv.Perm.support: the elements x : α that are not fixed by f.

Assume α is a Fintype:

• Equiv.Perm.fixed_point_card_lt_of_ne_one f says that f has strictly less than Fintype.card α - 1 fixed points, unless f = 1. (Equivalently, f.support has at least 2 elements.)
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
• f.Disjoint g = ∀ (x : α), f x = x g x = x
Instances For
theorem Equiv.Perm.Disjoint.symm {α : Type u_1} {f : } {g : } :
f.Disjoint gg.Disjoint f
theorem Equiv.Perm.Disjoint.symmetric {α : Type u_1} :
Symmetric Equiv.Perm.Disjoint
instance Equiv.Perm.instIsSymmDisjoint {α : Type u_1} :
IsSymm (Equiv.Perm α) Equiv.Perm.Disjoint
Equations
• =
theorem Equiv.Perm.disjoint_comm {α : Type u_1} {f : } {g : } :
f.Disjoint g g.Disjoint f
theorem Equiv.Perm.Disjoint.commute {α : Type u_1} {f : } {g : } (h : f.Disjoint g) :
@[simp]
theorem Equiv.Perm.disjoint_one_left {α : Type u_1} (f : ) :
@[simp]
theorem Equiv.Perm.disjoint_one_right {α : Type u_1} (f : ) :
f.Disjoint 1
theorem Equiv.Perm.disjoint_iff_eq_or_eq {α : Type u_1} {f : } {g : } :
f.Disjoint g ∀ (x : α), f x = x g x = x
@[simp]
theorem Equiv.Perm.disjoint_refl_iff {α : Type u_1} {f : } :
f.Disjoint f f = 1
theorem Equiv.Perm.Disjoint.inv_left {α : Type u_1} {f : } {g : } (h : f.Disjoint g) :
f⁻¹.Disjoint g
theorem Equiv.Perm.Disjoint.inv_right {α : Type u_1} {f : } {g : } (h : f.Disjoint g) :
f.Disjoint g⁻¹
@[simp]
theorem Equiv.Perm.disjoint_inv_left_iff {α : Type u_1} {f : } {g : } :
f⁻¹.Disjoint g f.Disjoint g
@[simp]
theorem Equiv.Perm.disjoint_inv_right_iff {α : Type u_1} {f : } {g : } :
f.Disjoint g⁻¹ f.Disjoint g
theorem Equiv.Perm.Disjoint.mul_left {α : Type u_1} {f : } {g : } {h : } (H1 : f.Disjoint h) (H2 : g.Disjoint h) :
(f * g).Disjoint h
theorem Equiv.Perm.Disjoint.mul_right {α : Type u_1} {f : } {g : } {h : } (H1 : f.Disjoint g) (H2 : f.Disjoint h) :
f.Disjoint (g * h)
theorem Equiv.Perm.disjoint_conj {α : Type u_1} {f : } {g : } (h : ) :
(h * f * h⁻¹).Disjoint (h * g * h⁻¹) f.Disjoint g
theorem Equiv.Perm.Disjoint.conj {α : Type u_1} {f : } {g : } (H : f.Disjoint g) (h : ) :
(h * f * h⁻¹).Disjoint (h * g * h⁻¹)
theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : } (l : List (Equiv.Perm α)) (h : gl, f.Disjoint g) :
f.Disjoint l.prod
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₁.Perm l₂) :
l₁.prod = l₂.prod
theorem Equiv.Perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : List (Equiv.Perm α)} (h1 : 1l) (h2 : List.Pairwise Equiv.Perm.Disjoint l) :
l.Nodup
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στ : σ.Disjoint τ) {a : α} :
(σ * τ) a = a σ a = a τ a = a
theorem Equiv.Perm.Disjoint.mul_eq_one_iff {α : Type u_1} {σ : } {τ : } (hστ : σ.Disjoint τ) :
σ * τ = 1 σ = 1 τ = 1
theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow {α : Type u_1} {σ : } {τ : } (hστ : σ.Disjoint τ) (m : ) (n : ) :
(σ ^ m).Disjoint (τ ^ n)
theorem Equiv.Perm.Disjoint.pow_disjoint_pow {α : Type u_1} {σ : } {τ : } (hστ : σ.Disjoint τ) (m : ) (n : ) :
(σ ^ m).Disjoint (τ ^ n)
def Equiv.Perm.IsSwap {α : Type u_1} [] (f : ) :

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

Equations
• f.IsSwap = ∃ (x : α) (y : α), x y f =
Instances For
@[simp]
theorem Equiv.Perm.ofSubtype_swap_eq {α : Type u_1} [] {p : αProp} [] (x : ) (y : ) :
Equiv.Perm.ofSubtype (Equiv.swap x y) = Equiv.swap x y
theorem Equiv.Perm.IsSwap.of_subtype_isSwap {α : Type u_1} [] {p : αProp} [] {f : } (h : f.IsSwap) :
(Equiv.Perm.ofSubtype f).IsSwap
theorem Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [] {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}
@[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
@[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
def Equiv.Perm.support {α : Type u_1} [] [] (f : ) :

The Finset of nonfixed points of a permutation.

Equations
Instances For
@[simp]
theorem Equiv.Perm.mem_support {α : Type u_1} [] [] {f : } {x : α} :
x f.support f x x
theorem Equiv.Perm.not_mem_support {α : Type u_1} [] [] {f : } {x : α} :
xf.support f x = x
theorem Equiv.Perm.coe_support_eq_set_support {α : Type u_1} [] [] (f : ) :
f.support = {x : α | f x x}
@[simp]
theorem Equiv.Perm.support_eq_empty_iff {α : Type u_1} [] [] {σ : } :
σ.support = σ = 1
@[simp]
theorem Equiv.Perm.support_one {α : Type u_1} [] [] :
@[simp]
theorem Equiv.Perm.support_refl {α : Type u_1} [] [] :
theorem Equiv.Perm.support_congr {α : Type u_1} [] [] {f : } {g : } (h : f.support g.support) (h' : xg.support, f x = g x) :
f = g
theorem Equiv.Perm.support_mul_le {α : Type u_1} [] [] (f : ) (g : ) :
(f * g).support f.support g.support
theorem Equiv.Perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [] [] {l : List (Equiv.Perm α)} {x : α} (hx : x l.prod.support) :
fl, x f.support
theorem Equiv.Perm.support_pow_le {α : Type u_1} [] [] (σ : ) (n : ) :
(σ ^ n).support σ.support
@[simp]
theorem Equiv.Perm.support_inv {α : Type u_1} [] [] (σ : ) :
σ⁻¹.support = σ.support
theorem Equiv.Perm.apply_mem_support {α : Type u_1} [] [] {f : } {x : α} :
f x f.support x f.support
theorem Equiv.Perm.pow_apply_mem_support {α : Type u_1} [] [] {f : } {n : } {x : α} :
(f ^ n) x f.support x f.support
theorem Equiv.Perm.zpow_apply_mem_support {α : Type u_1} [] [] {f : } {n : } {x : α} :
(f ^ n) x f.support x f.support
theorem Equiv.Perm.pow_eq_on_of_mem_support {α : Type u_1} [] [] {f : } {g : } (h : xf.support g.support, f x = g x) (k : ) (x : α) :
x f.support g.support(f ^ k) x = (g ^ k) x
theorem Equiv.Perm.disjoint_iff_disjoint_support {α : Type u_1} [] [] {f : } {g : } :
f.Disjoint g Disjoint f.support g.support
theorem Equiv.Perm.Disjoint.disjoint_support {α : Type u_1} [] [] {f : } {g : } (h : f.Disjoint g) :
Disjoint f.support g.support
theorem Equiv.Perm.Disjoint.support_mul {α : Type u_1} [] [] {f : } {g : } (h : f.Disjoint g) :
(f * g).support = f.support g.support
theorem Equiv.Perm.support_prod_of_pairwise_disjoint {α : Type u_1} [] [] (l : List (Equiv.Perm α)) (h : List.Pairwise Equiv.Perm.Disjoint l) :
l.prod.support = List.foldr (fun (x1 x2 : ) => x1 x2) (List.map Equiv.Perm.support l)
theorem Equiv.Perm.support_prod_le {α : Type u_1} [] [] (l : List (Equiv.Perm α)) :
l.prod.support List.foldr (fun (x1 x2 : ) => x1 x2) (List.map Equiv.Perm.support l)
theorem Equiv.Perm.support_zpow_le {α : Type u_1} [] [] (σ : ) (n : ) :
(σ ^ n).support σ.support
@[simp]
theorem Equiv.Perm.support_swap {α : Type u_1} [] [] {x : α} {y : α} (h : x y) :
(Equiv.swap x y).support = {x, y}
theorem Equiv.Perm.support_swap_iff {α : Type u_1} [] [] (x : α) (y : α) :
(Equiv.swap x y).support = {x, y} x y
theorem Equiv.Perm.support_swap_mul_swap {α : Type u_1} [] [] {x : α} {y : α} {z : α} (h : [x, y, z].Nodup) :
( * ).support = {x, y, z}
theorem Equiv.Perm.support_swap_mul_ge_support_diff {α : Type u_1} [] [] (f : ) (x : α) (y : α) :
f.support \ {x, y} ( * f).support
theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [] [] (f : ) (x : α) (h : f (f x) x) :
(Equiv.swap x (f x) * f).support = f.support \ {x}
theorem Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [] [] {f : } {x : α} {y : α} (hy : y (Equiv.swap x (f x) * f).support) :
y f.support y x
theorem Equiv.Perm.Disjoint.mem_imp {α : Type u_1} [] [] {f : } {g : } (h : f.Disjoint g) {x : α} (hx : x f.support) :
xg.support
theorem Equiv.Perm.eq_on_support_mem_disjoint {α : Type u_1} [] [] {f : } {l : List (Equiv.Perm α)} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) (x : α) :
x f.supportf x = l.prod x
theorem Equiv.Perm.Disjoint.mono {α : Type u_1} [] [] {f : } {g : } {x : } {y : } (h : f.Disjoint g) (hf : x.support f.support) (hg : y.support g.support) :
x.Disjoint y
theorem Equiv.Perm.support_le_prod_of_mem {α : Type u_1} [] [] {f : } {l : List (Equiv.Perm α)} (h : f l) (hl : List.Pairwise Equiv.Perm.Disjoint l) :
f.support l.prod.support
@[simp]
theorem Equiv.Perm.support_extend_domain {α : Type u_1} [] [] {β : Type u_2} [] [] {p : βProp} [] (f : α ) {g : } :
(g.extendDomain f).support = Finset.map f.asEmbedding g.support
theorem Equiv.Perm.card_support_extend_domain {α : Type u_1} [] [] {β : Type u_2} [] [] {p : βProp} [] (f : α ) {g : } :
(g.extendDomain f).support.card = g.support.card
theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [] [] {f : } :
f.support.card = 0 f = 1
theorem Equiv.Perm.one_lt_card_support_of_ne_one {α : Type u_1} [] [] {f : } (h : f 1) :
1 < f.support.card
theorem Equiv.Perm.card_support_ne_one {α : Type u_1} [] [] (f : ) :
f.support.card 1
@[simp]
theorem Equiv.Perm.card_support_le_one {α : Type u_1} [] [] {f : } :
f.support.card 1 f = 1
theorem Equiv.Perm.two_le_card_support_of_ne_one {α : Type u_1} [] [] {f : } (h : f 1) :
2 f.support.card
theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [] [] {f : } {x : α} (hx : f x x) :
(Equiv.swap x (f x) * f).support.card < f.support.card
theorem Equiv.Perm.card_support_swap {α : Type u_1} [] [] {x : α} {y : α} (hxy : x y) :
(Equiv.swap x y).support.card = 2
@[simp]
theorem Equiv.Perm.card_support_eq_two {α : Type u_1} [] [] {f : } :
f.support.card = 2 f.IsSwap
theorem Equiv.Perm.Disjoint.card_support_mul {α : Type u_1} [] [] {f : } {g : } (h : f.Disjoint g) :
(f * g).support.card = f.support.card + g.support.card
theorem Equiv.Perm.card_support_prod_list_of_pairwise_disjoint {α : Type u_1} [] [] {l : List (Equiv.Perm α)} (h : List.Pairwise Equiv.Perm.Disjoint l) :
l.prod.support.card = (List.map (Finset.card Equiv.Perm.support) l).sum
@[simp]
theorem Equiv.Perm.support_subtype_perm {α : Type u_1} [] {s : } (f : ) (h : ∀ (x : α), x s f x s) :
(f.subtypePerm h).support = Finset.filter (fun (x : { x : α // x s }) => decide (f x x) = true) s.attach

### Fixed points #

theorem Equiv.Perm.fixed_point_card_lt_of_ne_one {α : Type u_1} [] [] {σ : } (h : σ 1) :
(Finset.filter (fun (x : α) => σ x = x) Finset.univ).card <
@[simp]
theorem Equiv.Perm.support_conj {α : Type u_1} [] [] {σ : } {τ : } :
(σ * τ * σ⁻¹).support = Finset.map τ.support
theorem Equiv.Perm.card_support_conj {α : Type u_1} [] [] {σ : } {τ : } :
(σ * τ * σ⁻¹).support.card = τ.support.card