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.

def Equiv.Perm.Disjoint {α : Type u_1} (f : Equiv.Perm α) (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

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

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

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

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

Equations

• @Equiv.Perm.instIsSymmPermDisjoint = @Equiv.Perm.instIsSymmPermDisjoint.proof_1

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

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

@[simp]

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

@[simp]

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

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_refl_iff {α : Type u_1} {f : Equiv.Perm α} : Equiv.Perm.Disjoint f f ↔ f = 1

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

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

@[simp]

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

@[simp]

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

theorem Equiv.Perm.Disjoint.mul_left {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} {h : Equiv.Perm α} (H1 : Equiv.Perm.Disjoint f h) (H2 : Equiv.Perm.Disjoint g h) : Equiv.Perm.Disjoint (f * g) h

theorem Equiv.Perm.Disjoint.mul_right {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} {h : Equiv.Perm α} (H1 : Equiv.Perm.Disjoint f g) (H2 : Equiv.Perm.Disjoint f h) : Equiv.Perm.Disjoint f (g * h)

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

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

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

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₂) : List.prod l₁ = List.prod 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) : List.Nodup 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} [DecidableEq α] (f : Equiv.Perm α) : Prop

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

Equations

• Equiv.Perm.IsSwap f = ∃ 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 : 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} [DecidableEq α] {p : α → Prop} [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} [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} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) : Finset α

The Finset of nonfixed points of a permutation.

Equations

• Equiv.Perm.support f = Finset.filter (fun x => ↑f x ≠ x) Finset.univ

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Equiv.Perm.exists_mem_support_of_mem_support_prod {α : Type u_1} [DecidableEq α] [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} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) (n : ℕ) : Equiv.Perm.support (σ ^ n) ≤ Equiv.Perm.support σ

@[simp]

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

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

@[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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {n : ℕ} {x : α} : ↑(f ^ n) x ∈ Equiv.Perm.support f ↔ x ∈ Equiv.Perm.support f

@[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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {n : ℤ} {x : α} : ↑(f ^ n) x ∈ Equiv.Perm.support f ↔ x ∈ Equiv.Perm.support f

theorem Equiv.Perm.pow_eq_on_of_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : ∀ (x : α), x ∈ Equiv.Perm.support f ∩ Equiv.Perm.support g → ↑f x = ↑g x) (k : ℕ) (x : α) : x ∈ Equiv.Perm.support f ∩ Equiv.Perm.support g → ↑(f ^ k) x = ↑(g ^ k) x

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

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

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

theorem Equiv.Perm.support_prod_of_pairwise_disjoint {α : Type u_1} [DecidableEq α] [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} [DecidableEq α] [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} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) (n : ℤ) : Equiv.Perm.support (σ ^ n) ≤ Equiv.Perm.support σ

@[simp]

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

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

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

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

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

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

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

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

theorem Equiv.Perm.Disjoint.mono {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} {x : Equiv.Perm α} {y : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) (hf : Equiv.Perm.support x ≤ Equiv.Perm.support f) (hg : Equiv.Perm.support y ≤ Equiv.Perm.support g) : Equiv.Perm.Disjoint x y

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

@[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 : Equiv.Perm α} : Equiv.Perm.support (Equiv.Perm.extendDomain g f) = Finset.map (Equiv.asEmbedding f) (Equiv.Perm.support g)

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 : Equiv.Perm α} : Finset.card (Equiv.Perm.support (Equiv.Perm.extendDomain g f)) = Finset.card (Equiv.Perm.support g)

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

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

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

@[simp]

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

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

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

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

@[simp]

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

theorem Equiv.Perm.Disjoint.card_support_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) : Finset.card (Equiv.Perm.support (f * g)) = Finset.card (Equiv.Perm.support f) + Finset.card (Equiv.Perm.support g)

theorem Equiv.Perm.card_support_prod_list_of_pairwise_disjoint {α : Type u_1} [DecidableEq α] [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} [DecidableEq α] {s : Finset α} (f : Equiv.Perm α) (h : ∀ (x : α), x ∈ s ↔ ↑f x ∈ s) : Equiv.Perm.support (Equiv.Perm.subtypePerm f h) = Finset.filter (fun x => decide (↑f ↑x ≠ ↑x) = true) (Finset.attach s)