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 : 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

• f.Disjoint g = ∀ (x : α), f x = x ∨ g x = x

theorem Equiv.Perm.Disjoint.symm {α : Type u_1} {f g : Perm α} : f.Disjoint g → g.Disjoint f

theorem Equiv.Perm.Disjoint.symmetric {α : Type u_1} : Symmetric Disjoint

instance Equiv.Perm.instIsSymmDisjoint {α : Type u_1} : IsSymm (Perm α) Disjoint

theorem Equiv.Perm.disjoint_comm {α : Type u_1} {f g : Perm α} : f.Disjoint g ↔ g.Disjoint f

theorem Equiv.Perm.Disjoint.commute {α : Type u_1} {f g : Perm α} (h : f.Disjoint g) : Commute f g

@[simp]

theorem Equiv.Perm.disjoint_one_left {α : Type u_1} (f : Perm α) : Disjoint 1 f

@[simp]

theorem Equiv.Perm.disjoint_one_right {α : Type u_1} (f : Perm α) : f.Disjoint 1

theorem Equiv.Perm.disjoint_iff_eq_or_eq {α : Type u_1} {f g : Perm α} : f.Disjoint g ↔ ∀ (x : α), f x = x ∨ g x = x

@[simp]

theorem Equiv.Perm.disjoint_refl_iff {α : Type u_1} {f : Perm α} : f.Disjoint f ↔ f = 1

theorem Equiv.Perm.Disjoint.inv_left {α : Type u_1} {f g : Perm α} (h : f.Disjoint g) : f⁻¹.Disjoint g

theorem Equiv.Perm.Disjoint.inv_right {α : Type u_1} {f g : Perm α} (h : f.Disjoint g) : f.Disjoint g⁻¹

@[simp]

theorem Equiv.Perm.disjoint_inv_left_iff {α : Type u_1} {f g : Perm α} : f⁻¹.Disjoint g ↔ f.Disjoint g

@[simp]

theorem Equiv.Perm.disjoint_inv_right_iff {α : Type u_1} {f g : Perm α} : f.Disjoint g⁻¹ ↔ f.Disjoint g

theorem Equiv.Perm.Disjoint.mul_left {α : Type u_1} {f g h : 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 : Perm α} (H1 : f.Disjoint g) (H2 : f.Disjoint h) : f.Disjoint (g * h)

theorem Equiv.Perm.disjoint_conj {α : Type u_1} {f g : Perm α} (h : Perm α) : (h * f * h⁻¹).Disjoint (h * g * h⁻¹) ↔ f.Disjoint g

theorem Equiv.Perm.Disjoint.conj {α : Type u_1} {f g : Perm α} (H : f.Disjoint g) (h : Perm α) : (h * f * h⁻¹).Disjoint (h * g * h⁻¹)

theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : Perm α} (l : List (Perm α)) (h : ∀ g ∈ l, f.Disjoint g) : f.Disjoint l.prod

theorem Equiv.Perm.disjoint_noncommProd_right {α : Type u_1} {g : Perm α} {ι : Type u_2} {k : ι → Perm α} {s : Finset ι} (hs : (↑s).Pairwise fun (i j : ι) => Commute (k i) (k j)) (hg : ∀ i ∈ s, g.Disjoint (k i)) : g.Disjoint (s.noncommProd k hs)

theorem Equiv.Perm.disjoint_prod_perm {α : Type u_1} {l₁ l₂ : List (Perm α)} (hl : List.Pairwise Disjoint l₁) (hp : l₁.Perm l₂) : l₁.prod = l₂.prod

theorem Equiv.Perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : List (Perm α)} (h1 : 1 ∉ l) (h2 : List.Pairwise Disjoint l) : l.Nodup

theorem Equiv.Perm.pow_apply_eq_self_of_apply_eq_self {α : Type u_1} {f : 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 : 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 : 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 : 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} {σ τ : Perm α} (hστ : σ.Disjoint τ) {a : α} : (σ * τ) a = a ↔ σ a = a ∧ τ a = a

theorem Equiv.Perm.Disjoint.mul_eq_one_iff {α : Type u_1} {σ τ : Perm α} (hστ : σ.Disjoint τ) : σ * τ = 1 ↔ σ = 1 ∧ τ = 1

theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow {α : Type u_1} {σ τ : Perm α} (hστ : σ.Disjoint τ) (m n : ℤ) : (σ ^ m).Disjoint (τ ^ n)

theorem Equiv.Perm.Disjoint.pow_disjoint_pow {α : Type u_1} {σ τ : Perm α} (hστ : σ.Disjoint τ) (m n : ℕ) : (σ ^ m).Disjoint (τ ^ n)

def Equiv.Perm.IsSwap {α : Type u_1} [DecidableEq α] (f : Perm α) : Prop

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

Equations

• f.IsSwap = ∃ (x : α) (y : α), x ≠ y ∧ f = Equiv.swap x y

@[simp]

theorem Equiv.Perm.ofSubtype_swap_eq {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] (x y : Subtype p) : ofSubtype (swap x y) = swap ↑x ↑y

theorem Equiv.Perm.IsSwap.of_subtype_isSwap {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {f : Perm (Subtype p)} (h : f.IsSwap) : (ofSubtype f).IsSwap

theorem Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [DecidableEq α] {f : Perm α} {x y : α} (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x

theorem Equiv.Perm.set_support_inv_eq {α : Type u_1} (p : Perm α) : {x : α | p⁻¹ x ≠ x} = {x : α | p x ≠ x}

theorem Equiv.Perm.set_support_apply_mem {α : Type u_1} {p : Perm α} {a : α} : p a ∈ {x : α | p x ≠ x} ↔ a ∈ {x : α | p x ≠ x}

theorem Equiv.Perm.set_support_zpow_subset {α : Type u_1} (p : Perm α) (n : ℤ) : {x : α | (p ^ n) x ≠ x} ⊆ {x : α | p x ≠ x}

theorem Equiv.Perm.set_support_mul_subset {α : Type u_1} (p q : Perm α) : {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 : Perm α) (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 : Perm α) (n : ℤ) {x : α} : f ((f ^ n) x) = (f ^ n) x ↔ f x = x

def Equiv.Perm.support {α : Type u_1} [DecidableEq α] [Fintype α] (f : Perm α) : Finset α

The Finset of nonfixed points of a permutation.

Equations

• f.support = Finset.filter (fun (x : α) => f x ≠ x) Finset.univ

@[simp]

theorem Equiv.Perm.mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {x : α} : x ∈ f.support ↔ f x ≠ x

theorem Equiv.Perm.not_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {x : α} : x ∉ f.support ↔ f x = x

theorem Equiv.Perm.coe_support_eq_set_support {α : Type u_1} [DecidableEq α] [Fintype α] (f : Perm α) : ↑f.support = {x : α | f x ≠ x}

@[simp]

theorem Equiv.Perm.support_eq_empty_iff {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} : σ.support = ∅ ↔ σ = 1

@[simp]

theorem Equiv.Perm.support_one {α : Type u_1} [DecidableEq α] [Fintype α] : support 1 = ∅

@[simp]

theorem Equiv.Perm.support_refl {α : Type u_1} [DecidableEq α] [Fintype α] : support (Equiv.refl α) = ∅

theorem Equiv.Perm.support_congr {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g

theorem Equiv.Perm.mem_support_iff_of_commute {α : Type u_1} [DecidableEq α] [Fintype α] {g c : Perm α} (hgc : Commute g c) (x : α) : x ∈ c.support ↔ g x ∈ c.support

If g and c commute, then g stabilizes the support of c

theorem Equiv.Perm.support_mul_le {α : Type u_1} [DecidableEq α] [Fintype α] (f g : Perm α) : (f * g).support ≤ f.support ⊔ g.support

theorem Equiv.Perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [DecidableEq α] [Fintype α] {l : List (Perm α)} {x : α} (hx : x ∈ l.prod.support) : ∃ f ∈ l, x ∈ f.support

theorem Equiv.Perm.support_pow_le {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Perm α) (n : ℕ) : (σ ^ n).support ≤ σ.support

@[simp]

theorem Equiv.Perm.support_inv {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Perm α) : σ⁻¹.support = σ.support

theorem Equiv.Perm.apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {x : α} : f x ∈ f.support ↔ x ∈ f.support

theorem Equiv.Perm.isInvariant_of_support_le {α : Type u_1} [DecidableEq α] [Fintype α] {c : Perm α} {s : Finset α} (hcs : c.support ≤ s) (x : α) : x ∈ s ↔ c x ∈ s

The support of a permutation is invariant

theorem Equiv.Perm.ofSubtype_eq_iff {α : Type u_1} [DecidableEq α] [Fintype α] {g c : Perm α} {s : Finset α} (hg : ∀ (x : α), x ∈ s ↔ g x ∈ s) : ofSubtype (g.subtypePerm hg) = c ↔ c.support ≤ s ∧ ∀ (hc' : ∀ (x : α), x ∈ s ↔ c x ∈ s), c.subtypePerm hc' = g.subtypePerm hg

A permutation c is the extension of a restriction of g to s iff its support is contained in s and its restriction is that of g

theorem Equiv.Perm.support_ofSubtype {α : Type u_1} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] (u : Perm (Subtype p)) : (ofSubtype u).support = Finset.map (Function.Embedding.subtype p) u.support

theorem Equiv.Perm.mem_support_of_mem_noncommProd_support {α : Type u_2} {β : Type u_3} [DecidableEq β] [Fintype β] {s : Finset α} {f : α → Perm β} {comm : (↑s).Pairwise (Function.onFun Commute f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) : ∃ a ∈ s, x ∈ (f a).support

theorem Equiv.Perm.pow_apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {n : ℕ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

theorem Equiv.Perm.zpow_apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {n : ℤ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

theorem Equiv.Perm.pow_eq_on_of_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (h : ∀ x ∈ f.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} [DecidableEq α] [Fintype α] {f g : Perm α} : f.Disjoint g ↔ _root_.Disjoint f.support g.support

theorem Equiv.Perm.Disjoint.disjoint_support {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.Disjoint g) : _root_.Disjoint f.support g.support

theorem Equiv.Perm.Disjoint.support_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.Disjoint g) : (f * g).support = f.support ∪ g.support

theorem Equiv.Perm.support_prod_of_pairwise_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] (l : List (Perm α)) (h : List.Pairwise Disjoint l) : l.prod.support = List.foldr (fun (x1 x2 : Finset α) => x1 ⊔ x2) ⊥ (List.map support l)

theorem Equiv.Perm.support_noncommProd {α : Type u_1} [DecidableEq α] [Fintype α] {ι : Type u_2} {k : ι → Perm α} {s : Finset ι} (hs : (↑s).Pairwise fun (i j : ι) => (k i).Disjoint (k j)) : (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) => (k i).support

theorem Equiv.Perm.support_prod_le {α : Type u_1} [DecidableEq α] [Fintype α] (l : List (Perm α)) : l.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) => x1 ⊔ x2) ⊥ (List.map support l)

theorem Equiv.Perm.support_zpow_le {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Perm α) (n : ℤ) : (σ ^ n).support ≤ σ.support

@[simp]

theorem Equiv.Perm.support_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x y : α} (h : x ≠ y) : (swap x y).support = {x, y}

theorem Equiv.Perm.support_swap_iff {α : Type u_1} [DecidableEq α] [Fintype α] (x y : α) : (swap x y).support = {x, y} ↔ x ≠ y

theorem Equiv.Perm.support_swap_mul_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x y z : α} (h : [x, y, z].Nodup) : (swap x y * swap y z).support = {x, y, z}

theorem Equiv.Perm.support_swap_mul_ge_support_diff {α : Type u_1} [DecidableEq α] [Fintype α] (f : Perm α) (x y : α) : f.support \ {x, y} ≤ (swap x y * f).support

theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [DecidableEq α] [Fintype α] (f : Perm α) (x : α) (h : f (f x) ≠ x) : (swap x (f x) * f).support = f.support \ {x}

theorem Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {x y : α} (hy : y ∈ (swap x (f x) * f).support) : y ∈ f.support ∧ y ≠ x

theorem Equiv.Perm.Disjoint.mem_imp {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (h : f.Disjoint g) {x : α} (hx : x ∈ f.support) : x ∉ g.support

theorem Equiv.Perm.eq_on_support_mem_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {l : List (Perm α)} (h : f ∈ l) (hl : List.Pairwise Disjoint l) (x : α) : x ∈ f.support → f x = l.prod x

theorem Equiv.Perm.Disjoint.mono {α : Type u_1} [DecidableEq α] [Fintype α] {f g x y : Perm α} (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} [DecidableEq α] [Fintype α] {f : Perm α} {l : List (Perm α)} (h : f ∈ l) (hl : List.Pairwise Disjoint l) : f.support ≤ l.prod.support

@[simp]

theorem Equiv.Perm.support_extend_domain {α : Type u_1} [DecidableEq α] [Fintype α] {β : Type u_2} [DecidableEq β] [Fintype β] {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {g : Perm α} : (g.extendDomain f).support = Finset.map f.asEmbedding g.support

theorem Equiv.Perm.card_support_extend_domain {α : Type u_1} [DecidableEq α] [Fintype α] {β : Type u_2} [DecidableEq β] [Fintype β] {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {g : Perm α} : (g.extendDomain f).support.card = g.support.card

theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} : f.support.card = 0 ↔ f = 1

theorem Equiv.Perm.one_lt_card_support_of_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} (h : f ≠ 1) : 1 < f.support.card

theorem Equiv.Perm.card_support_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] (f : Perm α) : f.support.card ≠ 1

@[simp]

theorem Equiv.Perm.card_support_le_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} : f.support.card ≤ 1 ↔ f = 1

theorem Equiv.Perm.two_le_card_support_of_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} (h : f ≠ 1) : 2 ≤ f.support.card

theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} {x : α} (hx : f x ≠ x) : (swap x (f x) * f).support.card < f.support.card

theorem Equiv.Perm.card_support_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2

@[simp]

theorem Equiv.Perm.card_support_eq_two {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} : f.support.card = 2 ↔ f.IsSwap

theorem Equiv.Perm.Disjoint.card_support_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f g : Perm α} (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} [DecidableEq α] [Fintype α] {l : List (Perm α)} (h : List.Pairwise Disjoint l) : l.prod.support.card = (List.map (Finset.card ∘ support) l).sum

@[simp]

theorem Equiv.Perm.support_subtype_perm {α : Type u_1} [DecidableEq α] {s : Finset α} (f : Perm α) (h : ∀ (x : α), x ∈ s ↔ f x ∈ s) : (f.subtypePerm h).support = Finset.filter (fun (x : { x : α // x ∈ s }) => f ↑x ≠ ↑x) Finset.univ

Fixed points

theorem Equiv.Perm.fixed_point_card_lt_of_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) : (Finset.filter (fun (x : α) => σ x = x) Finset.univ).card < Fintype.card α - 1

@[simp]

theorem Equiv.Perm.support_conj {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : Perm α} : (σ * τ * σ⁻¹).support = Finset.map (Equiv.toEmbedding σ) τ.support

theorem Equiv.Perm.card_support_conj {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : Perm α} : (σ * τ * σ⁻¹).support.card = τ.support.card