Documentation

Mathlib.GroupTheory.Perm.Support

support of a permutation #

Main definitions #

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

Assume α is a Fintype:

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
  • f.Disjoint g = ∀ (x : α), f x = x g x = x
Instances For
    theorem Equiv.Perm.Disjoint.symm {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} :
    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 : Equiv.Perm α} {g : Equiv.Perm α} :
    f.Disjoint g g.Disjoint f
    theorem Equiv.Perm.Disjoint.commute {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.Disjoint g) :
    @[simp]
    theorem Equiv.Perm.disjoint_one_right {α : Type u_1} (f : Equiv.Perm α) :
    f.Disjoint 1
    theorem Equiv.Perm.disjoint_iff_eq_or_eq {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} :
    f.Disjoint g ∀ (x : α), f x = x g x = x
    @[simp]
    theorem Equiv.Perm.disjoint_refl_iff {α : Type u_1} {f : Equiv.Perm α} :
    f.Disjoint f f = 1
    theorem Equiv.Perm.Disjoint.inv_left {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.Disjoint g) :
    f⁻¹.Disjoint g
    theorem Equiv.Perm.Disjoint.inv_right {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.Disjoint g) :
    f.Disjoint g⁻¹
    @[simp]
    theorem Equiv.Perm.disjoint_inv_left_iff {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} :
    f⁻¹.Disjoint g f.Disjoint g
    @[simp]
    theorem Equiv.Perm.disjoint_inv_right_iff {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} :
    f.Disjoint g⁻¹ f.Disjoint g
    theorem Equiv.Perm.Disjoint.mul_left {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} {h : Equiv.Perm α} (H1 : f.Disjoint h) (H2 : g.Disjoint h) :
    (f * g).Disjoint h
    theorem Equiv.Perm.Disjoint.mul_right {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} {h : Equiv.Perm α} (H1 : f.Disjoint g) (H2 : f.Disjoint h) :
    f.Disjoint (g * h)
    theorem Equiv.Perm.disjoint_conj {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (h : Equiv.Perm α) :
    (h * f * h⁻¹).Disjoint (h * g * h⁻¹) f.Disjoint g
    theorem Equiv.Perm.Disjoint.conj {α : Type u_1} {f : Equiv.Perm α} {g : Equiv.Perm α} (H : f.Disjoint g) (h : Equiv.Perm α) :
    (h * f * h⁻¹).Disjoint (h * g * h⁻¹)
    theorem Equiv.Perm.disjoint_prod_right {α : Type u_1} {f : Equiv.Perm α} (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 : 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στ : σ.Disjoint τ) {a : α} :
    (σ * τ) a = a σ a = a τ a = a
    theorem Equiv.Perm.Disjoint.mul_eq_one_iff {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : σ.Disjoint τ) :
    σ * τ = 1 σ = 1 τ = 1
    theorem Equiv.Perm.Disjoint.zpow_disjoint_zpow {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : σ.Disjoint τ) (m : ) (n : ) :
    (σ ^ m).Disjoint (τ ^ n)
    theorem Equiv.Perm.Disjoint.pow_disjoint_pow {α : Type u_1} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : σ.Disjoint τ) (m : ) (n : ) :
    (σ ^ m).Disjoint (τ ^ 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 : f.IsSwap) :
      (Equiv.Perm.ofSubtype f).IsSwap
      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}
      @[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
      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 : α} :
        x f.support f x x
        theorem Equiv.Perm.not_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} :
        xf.support f x = x
        theorem Equiv.Perm.coe_support_eq_set_support {α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) :
        f.support = {x : α | f x x}
        @[simp]
        theorem Equiv.Perm.support_eq_empty_iff {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} :
        σ.support = σ = 1
        theorem Equiv.Perm.support_congr {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.support g.support) (h' : xg.support, f x = g x) :
        f = g
        theorem Equiv.Perm.mem_support_iff_of_commute {α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} {c : Equiv.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 : Equiv.Perm α) (g : Equiv.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 (Equiv.Perm α)} {x : α} (hx : x l.prod.support) :
        fl, x f.support
        theorem Equiv.Perm.support_pow_le {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) (n : ) :
        (σ ^ n).support σ.support
        @[simp]
        theorem Equiv.Perm.support_inv {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) :
        σ⁻¹.support = σ.support
        theorem Equiv.Perm.apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {x : α} :
        f x f.support x f.support
        theorem Equiv.Perm.isInvariant_of_support_le {α : Type u_1} [DecidableEq α] [Fintype α] {c : Equiv.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 : Equiv.Perm α} {c : Equiv.Perm α} {s : Finset α} (hg : ∀ (x : α), x s g x s) :
        Equiv.Perm.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.pow_apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {n : } {x : α} :
        (f ^ n) x f.support x f.support
        theorem Equiv.Perm.zpow_apply_mem_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.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 : Equiv.Perm α} {g : Equiv.Perm α} (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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} :
        f.Disjoint g Disjoint f.support g.support
        theorem Equiv.Perm.Disjoint.disjoint_support {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.Disjoint g) :
        Disjoint f.support g.support
        theorem Equiv.Perm.Disjoint.support_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.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 (Equiv.Perm α)) (h : List.Pairwise Equiv.Perm.Disjoint l) :
        l.prod.support = List.foldr (fun (x1 x2 : Finset α) => x1 x2) (List.map Equiv.Perm.support l)
        theorem Equiv.Perm.support_prod_le {α : Type u_1} [DecidableEq α] [Fintype α] (l : List (Equiv.Perm α)) :
        l.prod.support List.foldr (fun (x1 x2 : Finset α) => x1 x2) (List.map Equiv.Perm.support l)
        theorem Equiv.Perm.support_zpow_le {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) (n : ) :
        (σ ^ n).support σ.support
        @[simp]
        theorem Equiv.Perm.support_swap {α : Type u_1} [DecidableEq α] [Fintype α] {x : α} {y : α} (h : x y) :
        (Equiv.swap x y).support = {x, y}
        theorem Equiv.Perm.support_swap_iff {α : Type u_1} [DecidableEq α] [Fintype α] (x : α) (y : α) :
        (Equiv.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) :
        (Equiv.swap x y * Equiv.swap y z).support = {x, y, z}
        theorem Equiv.Perm.support_swap_mul_ge_support_diff {α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (x : α) (y : α) :
        f.support \ {x, y} (Equiv.swap x y * f).support
        theorem Equiv.Perm.support_swap_mul_eq {α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {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} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} (h : f.Disjoint g) {x : α} (hx : x f.support) :
        xg.support
        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 f.supportf x = l.prod x
        theorem Equiv.Perm.Disjoint.mono {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.Perm α} {x : Equiv.Perm α} {y : Equiv.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 : Equiv.Perm α} {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} [DecidableEq α] [Fintype α] {β : Type u_2} [DecidableEq β] [Fintype β] {p : βProp} [DecidablePred p] (f : α Subtype p) {g : Equiv.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 : Equiv.Perm α} :
        (g.extendDomain f).support.card = g.support.card
        theorem Equiv.Perm.card_support_eq_zero {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} :
        f.support.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) :
        1 < f.support.card
        theorem Equiv.Perm.card_support_ne_one {α : Type u_1} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) :
        f.support.card 1
        @[simp]
        theorem Equiv.Perm.card_support_le_one {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} :
        f.support.card 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 f.support.card
        theorem Equiv.Perm.card_support_swap_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {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} [DecidableEq α] [Fintype α] {x : α} {y : α} (hxy : x y) :
        (Equiv.swap x y).support.card = 2
        @[simp]
        theorem Equiv.Perm.card_support_eq_two {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} :
        f.support.card = 2 f.IsSwap
        theorem Equiv.Perm.Disjoint.card_support_mul {α : Type u_1} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} {g : Equiv.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 (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} [DecidableEq α] {s : Finset α} (f : Equiv.Perm α) (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} [DecidableEq α] [Fintype α] {σ : Equiv.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 α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
        (σ * τ * σ⁻¹).support = Finset.map (Equiv.toEmbedding σ) τ.support
        theorem Equiv.Perm.card_support_conj {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} {τ : Equiv.Perm α} :
        (σ * τ * σ⁻¹).support.card = τ.support.card