mathlib3 documentation

group_theory.perm.support

Support of a permutation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

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

source
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
Instances for equiv.perm.disjoint
source
@[symm]
theorem equiv.perm.disjoint.symm {α : Type u_1} {f g : equiv.perm α} :
f.disjoint g → g.disjoint f
source
theorem equiv.perm.disjoint.symmetric {α : Type u_1} :
symmetric equiv.perm.disjoint
source
@[protected, instance]
def equiv.perm.disjoint.is_symm {α : Type u_1} :
is_symm (equiv.perm α) equiv.perm.disjoint
source
theorem equiv.perm.disjoint_comm {α : Type u_1} {f g : equiv.perm α} :
f.disjoint g ↔ g.disjoint f
source
theorem equiv.perm.disjoint.commute {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
commute f g
source
@[simp]
theorem equiv.perm.disjoint_one_left {α : Type u_1} (f : equiv.perm α) :
1.disjoint f
source
@[simp]
theorem equiv.perm.disjoint_one_right {α : Type u_1} (f : equiv.perm α) :
f.disjoint 1
source
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
source
@[simp]
theorem equiv.perm.disjoint_refl_iff {α : Type u_1} {f : equiv.perm α} :
f.disjoint f ↔ f = 1
source
theorem equiv.perm.disjoint.inv_left {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
f⁻¹.disjoint g
source
theorem equiv.perm.disjoint.inv_right {α : Type u_1} {f g : equiv.perm α} (h : f.disjoint g) :
f.disjoint g⁻¹
source
@[simp]
theorem equiv.perm.disjoint_inv_left_iff {α : Type u_1} {f g : equiv.perm α} :
f⁻¹.disjoint g ↔ f.disjoint g
source
@[simp]
theorem equiv.perm.disjoint_inv_right_iff {α : Type u_1} {f g : equiv.perm α} :
f.disjoint g⁻¹ ↔ f.disjoint g
source
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
source
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)
source
theorem equiv.perm.disjoint_prod_right {α : Type u_1} {f : equiv.perm α} (l : list (equiv.perm α)) (h : ∀ (g : equiv.perm α), g ∈ l → f.disjoint g) :
f.disjoint l.prod
source
theorem equiv.perm.disjoint_prod_perm {α : Type u_1} {l₁ l₂ : list (equiv.perm α)} (hl : list.pairwise equiv.perm.disjoint l₁) (hp : l₁ ~ l₂) :
l₁.prod = l₂.prod
source
theorem equiv.perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : list (equiv.perm α)} (h1 : 1 ∉ l) (h2 : list.pairwise equiv.perm.disjoint l) :
l.nodup
source
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
source
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
source
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
source
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
source
theorem equiv.perm.disjoint.mul_apply_eq_iff {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) {a : α} :
⇑(σ * τ) a = a ↔ ⇑σ a = a ∧ ⇑τ a = a
source
theorem equiv.perm.disjoint.mul_eq_one_iff {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :
σ * τ = 1 ↔ σ = 1 ∧ τ = 1
source
theorem equiv.perm.disjoint.zpow_disjoint_zpow {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ℤ) :
(σ ^ m).disjoint (τ ^ n)
source
theorem equiv.perm.disjoint.pow_disjoint_pow {α : Type u_1} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ℕ) :
(σ ^ m).disjoint (τ ^ n)
source
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
source
@[simp]
theorem equiv.perm.of_subtype_swap_eq {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] (x y : subtype p) :
⇑equiv.perm.of_subtype (equiv.swap x y) = equiv.swap ↑x ↑y
source
theorem equiv.perm.is_swap.of_subtype_is_swap {α : Type u_1} [decidable_eq α] {p : α → Prop} [decidable_pred p] {f : equiv.perm (subtype p)} (h : f.is_swap) :
(⇑equiv.perm.of_subtype f).is_swap
source
theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u_1} [decidable_eq α] {f : equiv.perm α} {x y : α} (hy : ⇑(equiv.swap x (⇑f x) * f) y ≠ y) :
⇑f y ≠ y ∧ y ≠ x
source
theorem equiv.perm.set_support_inv_eq {α : Type u_1} (p : equiv.perm α) :
{x : α | ⇑p⁻¹ x ≠ x} = {x : α | ⇑p x ≠ x}
source
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}
source
theorem equiv.perm.set_support_zpow_subset {α : Type u_1} (p : equiv.perm α) (n : ℤ) :
{x : α | ⇑(p ^ n) x ≠ x} ⊆ {x : α | ⇑p x ≠ x}
source
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}
source
def equiv.perm.support {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
finset α

The finset of nonfixed points of a permutation.

Equations
source
@[simp]
theorem equiv.perm.mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
x ∈ f.support ↔ ⇑f x ≠ x
source
theorem equiv.perm.not_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
x ∉ f.support ↔ ⇑f x = x
source
theorem equiv.perm.coe_support_eq_set_support {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
↑(f.support) = {x : α | ⇑f x ≠ x}
source
@[simp]
theorem equiv.perm.support_eq_empty_iff {α : Type u_1} [decidable_eq α] [fintype α] {σ : equiv.perm α} :
σ.support = ∅ ↔ σ = 1
source
@[simp]
theorem equiv.perm.support_one {α : Type u_1} [decidable_eq α] [fintype α] :
1.support = ∅
source
@[simp]
theorem equiv.perm.support_refl {α : Type u_1} [decidable_eq α] [fintype α] :
equiv.perm.support (equiv.refl α) = ∅
source
theorem equiv.perm.support_congr {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.support ⊆ g.support) (h' : ∀ (x : α), x ∈ g.support → ⇑f x = ⇑g x) :
f = g
source
theorem equiv.perm.support_mul_le {α : Type u_1} [decidable_eq α] [fintype α] (f g : equiv.perm α) :
(f * g).support ≤ f.support ⊔ g.support
source
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 : equiv.perm α), f ∈ l ∧ x ∈ f.support
source
theorem equiv.perm.support_pow_le {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) (n : ℕ) :
(σ ^ n).support ≤ σ.support
source
@[simp]
theorem equiv.perm.support_inv {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) :
σ⁻¹.support = σ.support
source
@[simp]
theorem equiv.perm.apply_mem_support {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
⇑f x ∈ f.support ↔ x ∈ f.support
source
@[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
source
@[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
source
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.support → ⇑f x = ⇑g x) (k : ℕ) (x : α) (H : x ∈ f.support ∩ g.support) :
⇑(f ^ k) x = ⇑(g ^ k) x
source
theorem equiv.perm.disjoint_iff_disjoint_support {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} :
f.disjoint g ↔ disjoint f.support g.support
source
theorem equiv.perm.disjoint.disjoint_support {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
disjoint f.support g.support
source
theorem equiv.perm.disjoint.support_mul {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
(f * g).support = f.support ∪ g.support
source
theorem equiv.perm.support_prod_of_pairwise_disjoint {α : Type u_1} [decidable_eq α] [fintype α] (l : list (equiv.perm α)) (h : list.pairwise equiv.perm.disjoint l) :
l.prod.support = list.foldr has_sup.sup ⊥ (list.map equiv.perm.support l)
source
theorem equiv.perm.support_prod_le {α : Type u_1} [decidable_eq α] [fintype α] (l : list (equiv.perm α)) :
l.prod.support ≤ list.foldr has_sup.sup ⊥ (list.map equiv.perm.support l)
source
theorem equiv.perm.support_zpow_le {α : Type u_1} [decidable_eq α] [fintype α] (σ : equiv.perm α) (n : ℤ) :
(σ ^ n).support ≤ σ.support
source
@[simp]
theorem equiv.perm.support_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y : α} (h : x ≠ y) :
(equiv.swap x y).support = {x, y}
source
theorem equiv.perm.support_swap_iff {α : Type u_1} [decidable_eq α] [fintype α] (x y : α) :
(equiv.swap x y).support = {x, y} ↔ x ≠ y
source
theorem equiv.perm.support_swap_mul_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y z : α} (h : [x, y, z].nodup) :
(equiv.swap x y * equiv.swap y z).support = {x, y, z}
source
theorem equiv.perm.support_swap_mul_ge_support_diff {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x y : α) :
f.support \ {x, y} ≤ (equiv.swap x y * f).support
source
theorem equiv.perm.support_swap_mul_eq {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) (x : α) (h : ⇑f (⇑f x) ≠ x) :
(equiv.swap x (⇑f x) * f).support = f.support \ {x}
source
theorem equiv.perm.mem_support_swap_mul_imp_mem_support_ne {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x y : α} (hy : y ∈ (equiv.swap x (⇑f x) * f).support) :
y ∈ f.support ∧ y ≠ x
source
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) :
x ∉ g.support
source
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 : list.pairwise equiv.perm.disjoint l) (x : α) (H : x ∈ f.support) :
⇑f x = ⇑(l.prod) x
source
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) :
x.disjoint y
source
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 : list.pairwise equiv.perm.disjoint l) :
f.support ≤ l.prod.support
source
@[simp]
theorem equiv.perm.support_extend_domain {α : Type u_1} [decidable_eq α] [fintype α] {β : Type u_2} [decidable_eq β] [fintype β] {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) {g : equiv.perm α} :
(g.extend_domain f).support = finset.map f.as_embedding g.support
source
theorem equiv.perm.card_support_extend_domain {α : Type u_1} [decidable_eq α] [fintype α] {β : Type u_2} [decidable_eq β] [fintype β] {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) {g : equiv.perm α} :
(g.extend_domain f).support.card = g.support.card
source
@[simp]
theorem equiv.perm.card_support_eq_zero {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card = 0 ↔ f = 1
source
theorem equiv.perm.one_lt_card_support_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f ≠ 1) :
1 < f.support.card
source
theorem equiv.perm.card_support_ne_one {α : Type u_1} [decidable_eq α] [fintype α] (f : equiv.perm α) :
f.support.card ≠ 1
source
@[simp]
theorem equiv.perm.card_support_le_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card ≤ 1 ↔ f = 1
source
theorem equiv.perm.two_le_card_support_of_ne_one {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f ≠ 1) :
2 ≤ f.support.card
source
theorem equiv.perm.card_support_swap_mul {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hx : ⇑f x ≠ x) :
(equiv.swap x (⇑f x) * f).support.card < f.support.card
source
theorem equiv.perm.card_support_swap {α : Type u_1} [decidable_eq α] [fintype α] {x y : α} (hxy : x ≠ y) :
(equiv.swap x y).support.card = 2
source
@[simp]
theorem equiv.perm.card_support_eq_two {α : Type u_1} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card = 2 ↔ f.is_swap
source
theorem equiv.perm.disjoint.card_support_mul {α : Type u_1} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
(f * g).support.card = f.support.card + g.support.card
source
theorem equiv.perm.card_support_prod_list_of_pairwise_disjoint {α : Type u_1} [decidable_eq α] [fintype α] {l : list (equiv.perm α)} (h : list.pairwise equiv.perm.disjoint l) :
l.prod.support.card = (list.map (finset.card ∘ equiv.perm.support) l).sum
source
@[simp]
theorem equiv.perm.support_subtype_perm {α : Type u_1} [decidable_eq α] {s : finset α} (f : equiv.perm α) (h : ∀ (x : α), x ∈ s ↔ ⇑f x ∈ s) :
(f.subtype_perm h).support = finset.filter (λ (x : {x // x ∈ s}), ⇑f ↑x ≠ ↑x) s.attach