Documentation

Mathlib.GroupTheory.Perm.Support

support of a permutation #

Main definitions #

In the following, f g : Equiv.Perm α.

def Equiv.Perm.Disjoint {α : Type u_1} (f : Equiv.Perm α) (g : Equiv.Perm α) :

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
    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
    theorem Equiv.Perm.Disjoint.commute {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.Disjoint f g) :
    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.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) :
    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) :
    theorem Equiv.Perm.Disjoint.conj {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (H : Equiv.Perm.Disjoint f g) (h : Equiv.Perm α) :
    theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : Equiv.Perm α} (l : List (Equiv.Perm α)) (h : gl, Equiv.Perm.Disjoint f g) :
    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 : List.Perm l₁ l₂) :
    theorem Equiv.Perm.nodup_of_pairwise_disjoint {α : Type u_1} {l : List (Equiv.Perm α)} (h1 : 1l) (h2 : List.Pairwise Equiv.Perm.Disjoint 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 α) :

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

    Equations
    Instances For
      @[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 α) :

      The Finset of nonfixed points of a permutation.

      Equations
      Instances For
        @[simp]
        theorem Equiv.Perm.mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} :
        theorem Equiv.Perm.not_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} :
        xEquiv.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_congr {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm.support f Equiv.Perm.support g) (h' : xEquiv.Perm.support g, f x = g x) :
        f = g
        @[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
        @[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.pow_eq_on_of_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : xEquiv.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.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 : Finset α) => 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 : Finset α) => x x_1) (List.map Equiv.Perm.support l)
        @[simp]
        theorem Equiv.Perm.support_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x : α} {y : α} (h : x y) :
        theorem Equiv.Perm.support_swap_iff {α : Type u_1} [DecidableEq α] [Fintype α] (x : α) (y : α) :
        theorem Equiv.Perm.support_swap_mul_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x : α} {y : α} {z : α} (h : List.Nodup [x, y, z]) :
        theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (h : f (f x) 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)) :
        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) :
        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 ff x = (List.prod l) x
        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) :
        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 α} :
        theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} :
        (Equiv.Perm.support f).card = 0 f = 1
        theorem Equiv.Perm.one_lt_card_support_of_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (h : f 1) :
        @[simp]
        theorem Equiv.Perm.card_support_le_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} :
        (Equiv.Perm.support f).card 1 f = 1
        theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} (hx : f x x) :
        (Equiv.Perm.support (Equiv.swap x (f x) * f)).card < (Equiv.Perm.support f).card
        theorem Equiv.Perm.card_support_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x : α} {y : α} (hxy : x y) :
        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) :
        (Equiv.Perm.support (List.prod l)).card = 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 : { x : α // x s }) => decide (f x x) = true) (Finset.attach s)