Mathlib.GroupTheory.Perm.Support

Equiv.Perm.Disjoint definition

(f g : Perm α)

Full source

/-- Two permutations `f` and `g` are `Disjoint` if their supports are disjoint, i.e.,
every element is fixed either by `f`, or by `g`. -/
def Disjoint (f g : Perm α) :=
  ∀ x, f x = x ∨ g x = x

Disjoint permutations

Informal description

Two permutations $ f $ and $ g $ of a type $ \alpha $ are called *disjoint* if for every element $ x \in \alpha $, either $ f $ fixes $ x $ (i.e., $ f(x) = x $) or $ g $ fixes $ x $ (i.e., $ g(x) = x $).

Equiv.Perm.Disjoint.symm theorem

: Disjoint f g → Disjoint g f

Full source

@[symm]
theorem Disjoint.symm : Disjoint f g → Disjoint g f := by simp only [Disjoint, or_comm, imp_self]

Symmetry of Disjoint Permutations

Informal description

For any two permutations $ f $ and $ g $ of a type $ \alpha $, if $ f $ and $ g $ are disjoint, then $ g $ and $ f $ are also disjoint.

Equiv.Perm.Disjoint.symmetric theorem

: Symmetric (@Disjoint α)

Full source

theorem Disjoint.symmetric : Symmetric (@Disjoint α) := fun _ _ => Disjoint.symm

Symmetry of Permutation Disjointness Relation

Informal description

The disjointness relation on permutations of a type $\alpha$ is symmetric, meaning that for any two permutations $f$ and $g$ of $\alpha$, if $f$ is disjoint from $g$, then $g$ is disjoint from $f$.

Equiv.Perm.instIsSymmDisjoint instance

: IsSymm (Perm α) Disjoint

Full source

instance : IsSymm (Perm α) Disjoint :=
  ⟨Disjoint.symmetric⟩

Symmetry of Permutation Disjointness

Informal description

The disjointness relation on permutations of a type $\alpha$ is symmetric.

Equiv.Perm.disjoint_comm theorem

: Disjoint f g ↔ Disjoint g f

Full source

theorem disjoint_comm : DisjointDisjoint f g ↔ Disjoint g f :=
  ⟨Disjoint.symm, Disjoint.symm⟩

Symmetry of Permutation Disjointness

Informal description

Two permutations $f$ and $g$ of a type $\alpha$ are disjoint if and only if $g$ and $f$ are disjoint. In other words, the disjointness relation is symmetric.

Equiv.Perm.Disjoint.commute theorem

(h : Disjoint f g) : Commute f g

Full source

theorem Disjoint.commute (h : Disjoint f g) : Commute f g :=
  Equiv.ext fun x =>
    (h x).elim
      (fun hf =>
        (h (g x)).elim (fun hg => by simp [mul_apply, hf, hg]) fun hg => by
          simp [mul_apply, hf, g.injective hg])
      fun hg =>
      (h (f x)).elim (fun hf => by simp [mul_apply, f.injective hf, hg]) fun hf => by
        simp [mul_apply, hf, hg]

Commutation of Disjoint Permutations

Informal description

If two permutations $f$ and $g$ of a type $\alpha$ are disjoint, then they commute, i.e., $f \circ g = g \circ f$.

Equiv.Perm.disjoint_one_left theorem

(f : Perm α) : Disjoint 1 f

Full source

@[simp]
theorem disjoint_one_left (f : Perm α) : Disjoint 1 f := fun _ => Or.inl rfl

Identity Permutation is Disjoint from Any Permutation

Informal description

For any permutation $f$ of a type $\alpha$, the identity permutation $1$ is disjoint from $f$, meaning that for every element $x \in \alpha$, either $1(x) = x$ or $f(x) = x$.

Equiv.Perm.disjoint_one_right theorem

(f : Perm α) : Disjoint f 1

Full source

@[simp]
theorem disjoint_one_right (f : Perm α) : Disjoint f 1 := fun _ => Or.inr rfl

Every permutation is disjoint with the identity permutation

Informal description

For any permutation $f$ of a type $\alpha$, $f$ is disjoint with the identity permutation $1$.

Equiv.Perm.disjoint_iff_eq_or_eq theorem

: Disjoint f g ↔ ∀ x : α, f x = x ∨ g x = x

Full source

theorem disjoint_iff_eq_or_eq : DisjointDisjoint f g ↔ ∀ x : α, f x = x ∨ g x = x :=
  Iff.rfl

Characterization of Disjoint Permutations via Fixed Points

Informal description

Two permutations $f$ and $g$ of a type $\alpha$ are disjoint if and only if for every element $x \in \alpha$, either $f(x) = x$ or $g(x) = x$.

Equiv.Perm.disjoint_refl_iff theorem

: Disjoint f f ↔ f = 1

Full source

@[simp]
theorem disjoint_refl_iff : DisjointDisjoint f f ↔ f = 1 := by
  refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩
  ext x
  rcases h x with hx | hx <;> simp [hx]

Self-Disjointness Characterization of the Identity Permutation

Informal description

For any permutation $f$ of a type $\alpha$, $f$ is disjoint from itself if and only if $f$ is the identity permutation.

Equiv.Perm.Disjoint.inv_left theorem

(h : Disjoint f g) : Disjoint f⁻¹ g

Full source

theorem Disjoint.inv_left (h : Disjoint f g) : Disjoint f⁻¹ g := by
  intro x
  rw [inv_eq_iff_eq, eq_comm]
  exact h x

Inverse of First Permutation Preserves Disjointness

Informal description

If two permutations $ f $ and $ g $ of a type $ \alpha $ are disjoint, then their inverses $ f^{-1} $ and $ g $ are also disjoint.

Equiv.Perm.Disjoint.inv_right theorem

(h : Disjoint f g) : Disjoint f g⁻¹

Full source

theorem Disjoint.inv_right (h : Disjoint f g) : Disjoint f g⁻¹ :=
  h.symm.inv_left.symm

Inverse of Second Permutation Preserves Disjointness

Informal description

If two permutations $f$ and $g$ of a type $\alpha$ are disjoint, then $f$ and the inverse permutation $g^{-1}$ are also disjoint.

Equiv.Perm.disjoint_inv_left_iff theorem

: Disjoint f⁻¹ g ↔ Disjoint f g

Full source

@[simp]
theorem disjoint_inv_left_iff : DisjointDisjoint f⁻¹ g ↔ Disjoint f g := by
  refine ⟨fun h => ?_, Disjoint.inv_left⟩
  convert h.inv_left

Disjointness of Inverse Permutation: $f^{-1} \perp g \leftrightarrow f \perp g$

Informal description

For any permutations $f$ and $g$ of a type $\alpha$, the inverse permutation $f^{-1}$ is disjoint from $g$ if and only if $f$ is disjoint from $g$. In other words, $f^{-1}$ and $g$ are disjoint precisely when $f$ and $g$ are disjoint.

Equiv.Perm.disjoint_inv_right_iff theorem

: Disjoint f g⁻¹ ↔ Disjoint f g

Full source

@[simp]
theorem disjoint_inv_right_iff : DisjointDisjoint f g⁻¹ ↔ Disjoint f g := by
  rw [disjoint_comm, disjoint_inv_left_iff, disjoint_comm]

Disjointness of Permutation and Inverse: $f \perp g^{-1} \leftrightarrow f \perp g$

Informal description

For any permutations $f$ and $g$ of a type $\alpha$, the permutation $f$ is disjoint from the inverse permutation $g^{-1}$ if and only if $f$ is disjoint from $g$. In other words, $f$ and $g^{-1}$ are disjoint precisely when $f$ and $g$ are disjoint.

Equiv.Perm.Disjoint.mul_left theorem

(H1 : Disjoint f h) (H2 : Disjoint g h) : Disjoint (f * g) h

Full source

theorem Disjoint.mul_left (H1 : Disjoint f h) (H2 : Disjoint g h) : Disjoint (f * g) h := fun x =>
  by cases H1 x <;> cases H2 x <;> simp [*]

Disjointness is preserved under left multiplication

Informal description

If permutations $f$ and $h$ are disjoint, and permutations $g$ and $h$ are disjoint, then the product permutation $f \circ g$ is disjoint from $h$.

Equiv.Perm.Disjoint.mul_right theorem

(H1 : Disjoint f g) (H2 : Disjoint f h) : Disjoint f (g * h)

Full source

theorem Disjoint.mul_right (H1 : Disjoint f g) (H2 : Disjoint f h) : Disjoint f (g * h) := by
  rw [disjoint_comm]
  exact H1.symm.mul_left H2.symm

Disjointness is preserved under right composition

Informal description

For any permutations $f$, $g$, and $h$ of a type $\alpha$, if $f$ is disjoint from $g$ and $f$ is disjoint from $h$, then $f$ is disjoint from the composition $g \circ h$.

Equiv.Perm.disjoint_conj theorem

(h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹) ↔ Disjoint f g

Full source

theorem disjoint_conj (h : Perm α) : DisjointDisjoint (h * f * h⁻¹) (h * g * h⁻¹) ↔ Disjoint f g :=
  (h⁻¹).forall_congr fun {_} ↦ by simp only [mul_apply, eq_inv_iff_eq]

Conjugation Preserves Disjointness of Permutations

Informal description

For any permutation $h$ of a type $\alpha$, the conjugate permutations $h f h^{-1}$ and $h g h^{-1}$ are disjoint if and only if the original permutations $f$ and $g$ are disjoint. In other words, disjointness of permutations is preserved under conjugation.

Equiv.Perm.Disjoint.conj theorem

(H : Disjoint f g) (h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹)

Full source

theorem Disjoint.conj (H : Disjoint f g) (h : Perm α) : Disjoint (h * f * h⁻¹) (h * g * h⁻¹) :=
  (disjoint_conj h).2 H

Conjugation Preserves Disjointness of Permutations

Informal description

If two permutations $f$ and $g$ of a type $\alpha$ are disjoint, then for any permutation $h$ of $\alpha$, the conjugate permutations $h f h^{-1}$ and $h g h^{-1}$ are also disjoint.

Equiv.Perm.disjoint_prod_right theorem

(l : List (Perm α)) (h : ∀ g ∈ l, Disjoint f g) : Disjoint f l.prod

Full source

theorem disjoint_prod_right (l : List (Perm α)) (h : ∀ g ∈ l, Disjoint f g) :
    Disjoint f l.prod := by
  induction' l with g l ih
  · exact disjoint_one_right _
  · rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Disjointness Preserved Under Product of Permutations

Informal description

For any permutation $f$ of a type $\alpha$ and any list of permutations $l$ of $\alpha$, if $f$ is disjoint from every permutation $g$ in $l$, then $f$ is disjoint from the product of all permutations in $l$.

Equiv.Perm.disjoint_noncommProd_right theorem

 {ι : Type*} {k : ι → Perm α} {s : Finset ι} (hs : Set.Pairwise s fun i j ↦ Commute (k i) (k j))
  (hg : ∀ i ∈ s, g.Disjoint (k i)) : Disjoint g (s.noncommProd k (hs))

Full source

theorem disjoint_noncommProd_right {ι : Type*} {k : ι → Perm α} {s : Finset ι}
    (hs : Set.Pairwise s fun i j ↦ Commute (k i) (k j))
    (hg : ∀ i ∈ s, g.Disjoint (k i)) :
    Disjoint g (s.noncommProd k (hs)) :=
  noncommProd_induction s k hs g.Disjoint (fun _ _ ↦ Disjoint.mul_right) (disjoint_one_right g) hg

Disjointness Preserved Under Commutative Product of Permutations

Informal description

Let $\alpha$ be a type, $\iota$ an index type, and $k : \iota \to \text{Perm}(\alpha)$ a family of permutations. For any finite subset $s \subseteq \iota$ where the permutations $\{k_i\}_{i \in s}$ pairwise commute (i.e., $k_i \circ k_j = k_j \circ k_i$ for all $i,j \in s$), and for any permutation $g \in \text{Perm}(\alpha)$ that is disjoint from each $k_i$ (i.e., $g$ and $k_i$ are disjoint for all $i \in s$), then $g$ is disjoint from the noncommutative product $\prod_{i \in s} k_i$ (taken in any order due to the commutativity assumption).

Equiv.Perm.disjoint_prod_perm theorem

{l₁ l₂ : List (Perm α)} (hl : l₁.Pairwise Disjoint) (hp : l₁ ~ l₂) : l₁.prod = l₂.prod

Full source

theorem disjoint_prod_perm {l₁ l₂ : List (Perm α)} (hl : l₁.Pairwise Disjoint) (hp : l₁ ~ l₂) :
    l₁.prod = l₂.prod :=
  hp.prod_eq' <| hl.imp Disjoint.commute

Product of Permutations is Invariant under Permutation of Disjoint Lists

Informal description

Let $l_1$ and $l_2$ be two lists of permutations of a type $\alpha$ such that the permutations in $l_1$ are pairwise disjoint (i.e., any two distinct permutations in $l_1$ are disjoint). If $l_1$ is a permutation of $l_2$ (i.e., $l_1 \sim l_2$), then the product of the permutations in $l_1$ is equal to the product of the permutations in $l_2$.

Equiv.Perm.nodup_of_pairwise_disjoint theorem

{l : List (Perm α)} (h1 : (1 : Perm α) ∉ l) (h2 : l.Pairwise Disjoint) : l.Nodup

Full source

theorem nodup_of_pairwise_disjoint {l : List (Perm α)} (h1 : (1 : Perm α) ∉ l)
    (h2 : l.Pairwise Disjoint) : l.Nodup := by
  refine List.Pairwise.imp_of_mem ?_ h2
  intro τ σ h_mem _ h_disjoint _
  subst τ
  suffices (σ : Perm α) = 1 by
    rw [this] at h_mem
    exact h1 h_mem
  exact ext fun a => or_self_iff.mp (h_disjoint a)

No Duplicates in List of Disjoint Non-Identity Permutations

Informal description

Let $l$ be a list of permutations of a type $\alpha$ such that the identity permutation $1$ is not in $l$ and every pair of distinct permutations in $l$ is disjoint. Then $l$ has no duplicate elements.

Equiv.Perm.pow_apply_eq_self_of_apply_eq_self theorem

{x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x

Full source

theorem pow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x
  | 0 => rfl
  | n + 1 => by rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

Iterates of a Permutation Preserve Fixed Points

Informal description

Let $f$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be a fixed point of $f$ (i.e., $f(x) = x$). Then for every natural number $n$, the $n$-th iterate of $f$ applied to $x$ satisfies $(f^n)(x) = x$.

Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self theorem

{x : α} (hfx : f x = x) : ∀ n : ℤ, (f ^ n) x = x

Full source

theorem zpow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℤ, (f ^ n) x = x
  | (n : ℕ) => pow_apply_eq_self_of_apply_eq_self hfx n
  | Int.negSucc n => by rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

Integer Iterates of a Permutation Preserve Fixed Points

Informal description

Let $f$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be a fixed point of $f$ (i.e., $f(x) = x$). Then for every integer $n$, the $n$-th iterate of $f$ applied to $x$ satisfies $(f^n)(x) = x$.

Equiv.Perm.pow_apply_eq_of_apply_apply_eq_self theorem

{x : α} (hffx : f (f x) = x) : ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x

Full source

theorem pow_apply_eq_of_apply_apply_eq_self {x : α} (hffx : f (f x) = x) :
    ∀ n : ℕ, (f ^ n) x = x ∨ (f ^ n) x = f x
  | 0 => Or.inl rfl
  | n + 1 =>
    (pow_apply_eq_of_apply_apply_eq_self hffx n).elim
      (fun h => Or.inr (by rw [pow_succ', mul_apply, h]))
      fun h => Or.inl (by rw [pow_succ', mul_apply, h, hffx])

Behavior of Permutation Iterates on Elements of Order 2

Informal description

Let $f$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be such that $f(f(x)) = x$. Then for every natural number $n$, the $n$-th iterate of $f$ applied to $x$ satisfies $(f^n)(x) = x$ or $(f^n)(x) = f(x)$.

Equiv.Perm.zpow_apply_eq_of_apply_apply_eq_self theorem

{x : α} (hffx : f (f x) = x) : ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x

Full source

theorem zpow_apply_eq_of_apply_apply_eq_self {x : α} (hffx : f (f x) = x) :
    ∀ i : ℤ, (f ^ i) x = x ∨ (f ^ i) x = f x
  | (n : ℕ) => pow_apply_eq_of_apply_apply_eq_self hffx n
  | Int.negSucc n => by
    rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm,
      inv_eq_iff_eq, ← mul_apply, ← pow_succ, @eq_comm _ x, or_comm]
    exact pow_apply_eq_of_apply_apply_eq_self hffx _

Behavior of Integer Iterates of a Permutation on Elements of Order 2

Informal description

Let $f$ be a permutation of a type $\alpha$ and let $x \in \alpha$ be such that $f(f(x)) = x$. Then for every integer $i$, the $i$-th iterate of $f$ applied to $x$ satisfies $(f^i)(x) = x$ or $(f^i)(x) = f(x)$.

Equiv.Perm.Disjoint.mul_apply_eq_iff theorem

{σ τ : Perm α} (hστ : Disjoint σ τ) {a : α} : (σ * τ) a = a ↔ σ a = a ∧ τ a = a

Full source

theorem Disjoint.mul_apply_eq_iff {σ τ : Perm α} (hστ : Disjoint σ τ) {a : α} :
    (σ * τ) a = a ↔ σ a = a ∧ τ a = a := by
  refine ⟨fun h => ?_, fun h => by rw [mul_apply, h.2, h.1]⟩
  rcases hστ a with hσ | hτ
  · exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
  · exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩

Composition of Disjoint Permutations Fixes an Element if and only if Both Permutations Fix It

Informal description

Let $\sigma$ and $\tau$ be two disjoint permutations of a type $\alpha$. For any element $a \in \alpha$, the composition $\sigma \circ \tau$ fixes $a$ (i.e., $(\sigma \circ \tau)(a) = a$) if and only if both $\sigma$ and $\tau$ fix $a$ (i.e., $\sigma(a) = a$ and $\tau(a) = a$).

Equiv.Perm.Disjoint.mul_eq_one_iff theorem

{σ τ : Perm α} (hστ : Disjoint σ τ) : σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Full source

theorem Disjoint.mul_eq_one_iff {σ τ : Perm α} (hστ : Disjoint σ τ) :
    σ * τ = 1 ↔ σ = 1 ∧ τ = 1 := by
  simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]

Composition of Disjoint Permutations is Identity if and only if Both are Identity

Informal description

For two disjoint permutations $\sigma$ and $\tau$ of a type $\alpha$, the composition $\sigma \circ \tau$ is the identity permutation if and only if both $\sigma$ and $\tau$ are the identity permutation.

Equiv.Perm.Disjoint.zpow_disjoint_zpow theorem

{σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℤ) : Disjoint (σ ^ m) (τ ^ n)

Full source

theorem Disjoint.zpow_disjoint_zpow {σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℤ) :
    Disjoint (σ ^ m) (τ ^ n) := fun x =>
  Or.imp (fun h => zpow_apply_eq_self_of_apply_eq_self h m)
    (fun h => zpow_apply_eq_self_of_apply_eq_self h n) (hστ x)

Integer Powers of Disjoint Permutations Remain Disjoint

Informal description

Let $\sigma$ and $\tau$ be two disjoint permutations of a type $\alpha$. Then for any integers $m$ and $n$, the permutations $\sigma^m$ and $\tau^n$ are also disjoint.

Equiv.Perm.Disjoint.pow_disjoint_pow theorem

{σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℕ) : Disjoint (σ ^ m) (τ ^ n)

Full source

theorem Disjoint.pow_disjoint_pow {σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℕ) :
    Disjoint (σ ^ m) (τ ^ n) :=
  hστ.zpow_disjoint_zpow m n

Natural Powers of Disjoint Permutations Remain Disjoint

Informal description

For any two disjoint permutations $\sigma$ and $\tau$ of a type $\alpha$, and for any natural numbers $m$ and $n$, the permutations $\sigma^m$ and $\tau^n$ are also disjoint.

Equiv.Perm.IsSwap definition

(f : Perm α) : Prop

Full source

/-- `f.IsSwap` indicates that the permutation `f` is a transposition of two elements. -/
def IsSwap (f : Perm α) : Prop :=
  ∃ x y, x ≠ y ∧ f = swap x y

Transposition of a permutation

Informal description

A permutation $ f $ of a type $ \alpha $ is called a transposition if there exist distinct elements $ x $ and $ y $ in $ \alpha $ such that $ f $ is equal to the swap of $ x $ and $ y $. In other words, $ f $ is a transposition if it can be expressed as $ f = \text{swap } x y $ for some $ x \neq y $.

Equiv.Perm.ofSubtype_swap_eq theorem

{p : α → Prop} [DecidablePred p] (x y : Subtype p) : ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y

Full source

@[simp]
theorem ofSubtype_swap_eq {p : α → Prop} [DecidablePred p] (x y : Subtype p) :
    ofSubtype (Equiv.swap x y) = Equiv.swap ↑x ↑y :=
  Equiv.ext fun z => by
    by_cases hz : p z
    · rw [swap_apply_def, ofSubtype_apply_of_mem _ hz]
      split_ifs with hzx hzy
      · simp_rw [hzx, Subtype.coe_eta, swap_apply_left]
      · simp_rw [hzy, Subtype.coe_eta, swap_apply_right]
      · rw [swap_apply_of_ne_of_ne] <;>
        simp [Subtype.ext_iff, *]
    · rw [ofSubtype_apply_of_not_mem _ hz, swap_apply_of_ne_of_ne]
      · intro h
        apply hz
        rw [h]
        exact Subtype.prop x
      intro h
      apply hz
      rw [h]
      exact Subtype.prop y

Lifting of Transposition from Subtype to Parent Type

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on a type $\alpha$, and let $x, y$ be elements of the subtype $\{a \in \alpha \mid p(a)\}$. Then the permutation obtained by lifting the transposition of $x$ and $y$ in the subtype equals the transposition of the underlying elements $x$ and $y$ in $\alpha$. In other words, $\mathrm{ofSubtype}(\mathrm{swap}\ x\ y) = \mathrm{swap}\ x\ y$.

Equiv.Perm.IsSwap.of_subtype_isSwap theorem

{p : α → Prop} [DecidablePred p] {f : Perm (Subtype p)} (h : f.IsSwap) : (ofSubtype f).IsSwap

Full source

theorem IsSwap.of_subtype_isSwap {p : α → Prop} [DecidablePred p] {f : Perm (Subtype p)}
    (h : f.IsSwap) : (ofSubtype f).IsSwap :=
  let ⟨⟨x, hx⟩, ⟨y, hy⟩, hxy⟩ := h
  ⟨x, y, by
    simp only [Ne, Subtype.ext_iff] at hxy
    exact hxy.1, by
    rw [hxy.2, ofSubtype_swap_eq]⟩

Lifting Preserves Transposition Property

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on a type $\alpha$, and let $f$ be a permutation of the subtype $\{a \in \alpha \mid p(a)\}$. If $f$ is a transposition (i.e., $f$ swaps two distinct elements of the subtype), then the permutation obtained by lifting $f$ to $\alpha$ (via `ofSubtype`) is also a transposition on $\alpha$.

Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self theorem

{f : Perm α} {x y : α} (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x

Full source

theorem ne_and_ne_of_swap_mul_apply_ne_self {f : Perm α} {x y : α} (hy : (swap x (f x) * f) y ≠ y) :
    f y ≠ yf y ≠ y ∧ y ≠ x := by
  simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
  by_cases h : f y = x
  · constructor <;> intro <;> simp_all only [if_true, eq_self_iff_true, not_true, Ne]
  · split_ifs at hy with h <;> try { simp [*] at * }

Non-fixed Points under Composition with Transposition

Informal description

For any permutation $f$ on a type $\alpha$ and elements $x, y \in \alpha$, if the composition of the transposition $\mathrm{swap}(x, f(x))$ with $f$ does not fix $y$ (i.e., $(\mathrm{swap}(x, f(x)) \circ f)(y) \neq y$), then $f$ does not fix $y$ and $y$ is not equal to $x$. In other words, $f(y) \neq y$ and $y \neq x$.

Equiv.Perm.set_support_inv_eq theorem

: {x | p⁻¹ x ≠ x} = {x | p x ≠ x}

Full source

theorem set_support_inv_eq : { x | p⁻¹ x ≠ x } = { x | p x ≠ x } := by
  ext x
  simp only [Set.mem_setOf_eq, Ne]
  rw [inv_def, symm_apply_eq, eq_comm]

Invariance of Support Under Permutation Inverse

Informal description

For any permutation $p$ on a type $\alpha$, the set of elements not fixed by the inverse permutation $p^{-1}$ is equal to the set of elements not fixed by $p$. In other words: $$\{x \in \alpha \mid p^{-1}(x) \neq x\} = \{x \in \alpha \mid p(x) \neq x\}$$

Equiv.Perm.set_support_apply_mem theorem

{p : Perm α} {a : α} : p a ∈ {x | p x ≠ x} ↔ a ∈ {x | p x ≠ x}

Full source

theorem set_support_apply_mem {p : Perm α} {a : α} :
    p a ∈ { x | p x ≠ x }p a ∈ { x | p x ≠ x } ↔ a ∈ { x | p x ≠ x } := by simp

Support Membership under Permutation Application: $p(a) \in \mathrm{supp}(p) \leftrightarrow a \in \mathrm{supp}(p)$

Informal description

For any permutation $p$ on a type $\alpha$ and any element $a \in \alpha$, the image $p(a)$ belongs to the support of $p$ (i.e., the set $\{x \in \alpha \mid p(x) \neq x\}$) if and only if $a$ itself belongs to the support of $p$.

Equiv.Perm.set_support_zpow_subset theorem

(n : ℤ) : {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}

Full source

theorem set_support_zpow_subset (n : ℤ) : { x | (p ^ n) x ≠ x }{ x | (p ^ n) x ≠ x } ⊆ { x | p x ≠ x } := by
  intro x
  simp only [Set.mem_setOf_eq, Ne]
  intro hx H
  simp [zpow_apply_eq_self_of_apply_eq_self H] at hx

Support of Permutation Powers is Contained in Original Support

Informal description

For any integer $n$ and any permutation $p$ of a type $\alpha$, the set of elements not fixed by the $n$-th power of $p$ is contained in the set of elements not fixed by $p$. In other words: $$\{x \in \alpha \mid (p^n)(x) \neq x\} \subseteq \{x \in \alpha \mid p(x) \neq x\}$$

Equiv.Perm.set_support_mul_subset theorem

: {x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}

Full source

theorem set_support_mul_subset : { x | (p * q) x ≠ x }{ x | (p * q) x ≠ x } ⊆ { x | p x ≠ x } ∪ { x | q x ≠ x } := by
  intro x
  simp only [Perm.coe_mul, Function.comp_apply, Ne, Set.mem_union, Set.mem_setOf_eq]
  by_cases hq : q x = x <;> simp [hq]

Support of Permutation Composition is Contained in Union of Supports

Informal description

For any permutations $p$ and $q$ on a type $\alpha$, the set of elements $x \in \alpha$ that are not fixed by the composition $p \circ q$ is contained in the union of the sets of elements not fixed by $p$ and not fixed by $q$. In other words, $\{x \mid (p \circ q)(x) \neq x\} \subseteq \{x \mid p(x) \neq x\} \cup \{x \mid q(x) \neq x\}$.

Equiv.Perm.apply_pow_apply_eq_iff theorem

(f : Perm α) (n : ℕ) {x : α} : f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Full source

@[simp]
theorem apply_pow_apply_eq_iff (f : Perm α) (n : ℕ) {x : α} :
    f ((f ^ n) x) = (f ^ n) x ↔ f x = x := by
  rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]

Fixed Point Criterion for Permutation Powers

Informal description

For any permutation $f$ of a type $\alpha$, any natural number $n$, and any element $x \in \alpha$, we have $f(f^n(x)) = f^n(x)$ if and only if $f(x) = x$.

Equiv.Perm.apply_zpow_apply_eq_iff theorem

(f : Perm α) (n : ℤ) {x : α} : f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Full source

@[simp]
theorem apply_zpow_apply_eq_iff (f : Perm α) (n : ℤ) {x : α} :
    f ((f ^ n) x) = (f ^ n) x ↔ f x = x := by
  rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]

Fixed Point Criterion for Permutation Powers

Informal description

For any permutation $f$ of a type $\alpha$, any integer $n$, and any element $x \in \alpha$, we have $f(f^n(x)) = f^n(x)$ if and only if $f(x) = x$.

Equiv.Perm.support definition

(f : Perm α) : Finset α

Full source

/-- The `Finset` of nonfixed points of a permutation. -/
def support (f : Perm α) : Finset α := {x | f x ≠ x}

Support of a permutation

Informal description

For a permutation $ f $ of a type $ \alpha $, the support of $ f $ is the finite set of elements $ x \in \alpha $ such that $ f(x) \neq x $.

Equiv.Perm.mem_support theorem

{x : α} : x ∈ f.support ↔ f x ≠ x

Full source

@[simp]
theorem mem_support {x : α} : x ∈ f.supportx ∈ f.support ↔ f x ≠ x := by
  rw [support, mem_filter, and_iff_right (mem_univ x)]

Characterization of Permutation Support Membership

Informal description

For a permutation $f$ of a type $\alpha$ and an element $x \in \alpha$, $x$ is in the support of $f$ if and only if $f(x) \neq x$.

Equiv.Perm.not_mem_support theorem

{x : α} : x ∉ f.support ↔ f x = x

Full source

theorem not_mem_support {x : α} : x ∉ f.supportx ∉ f.support ↔ f x = x := by simp

Characterization of Non-Support Elements for Permutations

Informal description

For a permutation $f$ of a type $\alpha$ and an element $x \in \alpha$, $x$ is not in the support of $f$ if and only if $f$ fixes $x$, i.e., $f(x) = x$.

Equiv.Perm.coe_support_eq_set_support theorem

(f : Perm α) : (f.support : Set α) = {x | f x ≠ x}

Full source

theorem coe_support_eq_set_support (f : Perm α) : (f.support : Set α) = { x | f x ≠ x } := by
  ext
  simp

Support of a Permutation as Set of Non-Fixed Points

Informal description

For any permutation $f$ of a type $\alpha$, the underlying set of its support (the finite set of elements not fixed by $f$) is equal to the set $\{x \in \alpha \mid f(x) \neq x\}$.

Equiv.Perm.support_eq_empty_iff theorem

{σ : Perm α} : σ.support = ∅ ↔ σ = 1

Full source

@[simp]
theorem support_eq_empty_iff {σ : Perm α} : σ.support = ∅ ↔ σ = 1 := by
  simp_rw [Finset.ext_iff, mem_support, Finset.not_mem_empty, iff_false, not_not,
    Equiv.Perm.ext_iff, one_apply]

Empty Support Characterization of Identity Permutation

Informal description

For any permutation $\sigma$ of a type $\alpha$, the support of $\sigma$ is empty if and only if $\sigma$ is the identity permutation.

Equiv.Perm.support_one theorem

: (1 : Perm α).support = ∅

Full source

@[simp]
theorem support_one : (1 : Perm α).support = ∅ := by rw [support_eq_empty_iff]

Empty Support of Identity Permutation

Informal description

The support of the identity permutation $1$ on a type $\alpha$ is the empty set, i.e., $\text{supp}(1) = \emptyset$.

Equiv.Perm.support_refl theorem

: support (Equiv.refl α) = ∅

Full source

@[simp]
theorem support_refl : support (Equiv.refl α) = ∅ :=
  support_one

Empty Support of Identity Permutation

Informal description

The support of the identity permutation $\text{refl}_\alpha$ on a type $\alpha$ is the empty set, i.e., $\text{supp}(\text{refl}_\alpha) = \emptyset$.

Equiv.Perm.support_congr theorem

(h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g

Full source

theorem support_congr (h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g := by
  ext x
  by_cases hx : x ∈ g.support
  · exact h' x hx
  · rw [not_mem_support.mp hx, ← not_mem_support]
    exact fun H => hx (h H)

Permutation Equality via Support and Agreement on Support

Informal description

Let $f$ and $g$ be permutations of a type $\alpha$. If the support of $f$ is contained in the support of $g$ (i.e., $\text{supp}(f) \subseteq \text{supp}(g)$), and for every $x$ in the support of $g$ we have $f(x) = g(x)$, then $f = g$.

Equiv.Perm.mem_support_iff_of_commute theorem

{g c : Perm α} (hgc : Commute g c) (x : α) : x ∈ c.support ↔ g x ∈ c.support

Full source

/-- If g and c commute, then g stabilizes the support of c -/
theorem mem_support_iff_of_commute {g c : Perm α} (hgc : Commute g c) (x : α) :
    x ∈ c.supportx ∈ c.support ↔ g x ∈ c.support := by
  simp only [mem_support, not_iff_not, ← mul_apply]
  rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

Commuting Permutations Preserve Support Membership

Informal description

For any permutations $ g $ and $ c $ of a type $ \alpha $ that commute (i.e., $ g \circ c = c \circ g $), an element $ x \in \alpha $ is in the support of $ c $ if and only if $ g(x) $ is in the support of $ c $. In other words, $ x \in \text{supp}(c) \leftrightarrow g(x) \in \text{supp}(c) $.

Equiv.Perm.support_mul_le theorem

(f g : Perm α) : (f * g).support ≤ f.support ⊔ g.support

Full source

theorem support_mul_le (f g : Perm α) : (f * g).support ≤ f.support ⊔ g.support := fun x => by
  simp only [sup_eq_union]
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  rintro ⟨hf, hg⟩
  rw [hg, hf]

Support of Permutation Composition is Contained in Union of Supports

Informal description

For any permutations $f$ and $g$ of a type $\alpha$, the support of their composition $f \circ g$ is contained in the union of their individual supports, i.e., $\text{supp}(f \circ g) \subseteq \text{supp}(f) \cup \text{supp}(g)$.

Equiv.Perm.exists_mem_support_of_mem_support_prod theorem

{l : List (Perm α)} {x : α} (hx : x ∈ l.prod.support) : ∃ f : Perm α, f ∈ l ∧ x ∈ f.support

Full source

theorem exists_mem_support_of_mem_support_prod {l : List (Perm α)} {x : α}
    (hx : x ∈ l.prod.support) : ∃ f : Perm α, f ∈ l ∧ x ∈ f.support := by
  contrapose! hx
  simp_rw [mem_support, not_not] at hx ⊢
  induction' l with f l ih
  · rfl
  · rw [List.prod_cons, mul_apply, ih, hx]
    · simp only [List.find?, List.mem_cons, true_or]
    intros f' hf'
    refine hx f' ?_
    simp only [List.find?, List.mem_cons]
    exact Or.inr hf'

Existence of Permutation in List with Non-Fixed Point in Product Support

Informal description

For any list of permutations $ l $ of a type $ \alpha $ and any element $ x \in \alpha $, if $ x $ is in the support of the product of the permutations in $ l $, then there exists a permutation $ f $ in $ l $ such that $ x $ is in the support of $ f $.

Equiv.Perm.support_pow_le theorem

(σ : Perm α) (n : ℕ) : (σ ^ n).support ≤ σ.support

Full source

theorem support_pow_le (σ : Perm α) (n : ℕ) : (σ ^ n).support ≤ σ.support := fun _ h1 =>
  mem_support.mpr fun h2 => mem_support.mp h1 (pow_apply_eq_self_of_apply_eq_self h2 n)

Support of Permutation Iterates is Contained in Original Support

Informal description

For any permutation $\sigma$ of a type $\alpha$ and any natural number $n$, the support of $\sigma^n$ is a subset of the support of $\sigma$. In other words, if an element $x \in \alpha$ is fixed by $\sigma$ (i.e., $\sigma(x) = x$), then it is also fixed by all iterates $\sigma^n$ of $\sigma$.

Equiv.Perm.support_inv theorem

(σ : Perm α) : support σ⁻¹ = σ.support

Full source

@[simp]
theorem support_inv (σ : Perm α) : support σ⁻¹ = σ.support := by
  simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

Support of Permutation Inverse Equals Support of Permutation

Informal description

For any permutation $\sigma$ of a type $\alpha$, the support of its inverse $\sigma^{-1}$ is equal to the support of $\sigma$. That is, $\text{support}(\sigma^{-1}) = \text{support}(\sigma)$.

Equiv.Perm.apply_mem_support theorem

{x : α} : f x ∈ f.support ↔ x ∈ f.support

Full source

theorem apply_mem_support {x : α} : f x ∈ f.supportf x ∈ f.support ↔ x ∈ f.support := by
  rw [mem_support, mem_support, Ne, Ne, apply_eq_iff_eq]

Permutation Support Invariance Under Application

Informal description

For a permutation $f$ of a type $\alpha$ and an element $x \in \alpha$, the image $f(x)$ belongs to the support of $f$ if and only if $x$ itself belongs to the support of $f$. In other words, $f(x) \neq f(x)$ if and only if $x \neq f(x)$.

Equiv.Perm.isInvariant_of_support_le theorem

{c : Perm α} {s : Finset α} (hcs : c.support ≤ s) (x : α) : x ∈ s ↔ c x ∈ s

Full source

/-- The support of a permutation is invariant -/
theorem isInvariant_of_support_le {c : Perm α} {s : Finset α} (hcs : c.support ≤ s) (x : α) :
    x ∈ sx ∈ s ↔ c x ∈ s := by
  by_cases hx' : x ∈ c.support
  · simp only [hcs hx', true_iff, hcs (apply_mem_support.mpr hx')]
  · rw [not_mem_support.mp hx']

Invariance of Finite Set Under Permutation with Contained Support

Informal description

For a permutation $c$ of a type $\alpha$ and a finite subset $s \subseteq \alpha$, if the support of $c$ is contained in $s$ (i.e., $\text{supp}(c) \subseteq s$), then for any element $x \in \alpha$, $x$ belongs to $s$ if and only if its image under $c$ belongs to $s$. In other words, $s$ is invariant under the action of $c$.

Equiv.Perm.ofSubtype_eq_iff theorem

 {g c : Equiv.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

Full source

/-- 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 -/
lemma ofSubtype_eq_iff {g c : Equiv.Perm α} {s : Finset α}
    (hg : ∀ x, x ∈ sx ∈ s ↔ g x ∈ s) :
    ofSubtypeofSubtype (g.subtypePerm hg) = c ↔
      c.support ≤ s ∧
      ∀ (hc' : ∀ x, x ∈ s ↔ c x ∈ s), c.subtypePerm hc' = g.subtypePerm hg := by
  simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
  constructor
  · intro h
    constructor
    · intro a ha
      by_contra ha'
      rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
      exact ha rfl
    · intro _ a ha
      rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
  · rintro ⟨hc, h⟩ a
    specialize h (isInvariant_of_support_le hc)
    by_cases ha : a ∈ s
    · rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha, eq_comm, ← not_mem_support]
      exact Finset.not_mem_mono hc ha

Characterization of Permutation Extension from Subtype via Support and Restriction

Informal description

Let $g$ and $c$ be permutations of a type $\alpha$, and let $s$ be a finite subset of $\alpha$ such that $s$ is invariant under $g$ (i.e., $x \in s \leftrightarrow g(x) \in s$ for all $x \in \alpha$). Then the permutation $c$ is equal to the extension of the restriction of $g$ to $s$ if and only if the following two conditions hold: 1. The support of $c$ is contained in $s$ (i.e., $\text{supp}(c) \subseteq s$). 2. For any permutation $c'$ whose support is also contained in $s$ and which leaves $s$ invariant, the restriction of $c'$ to $s$ equals the restriction of $g$ to $s$.

Equiv.Perm.support_ofSubtype theorem

 {p : α → Prop} [DecidablePred p] (u : Perm (Subtype p)) :
  (ofSubtype u).support = u.support.map (Function.Embedding.subtype p)

Full source

theorem support_ofSubtype {p : α → Prop} [DecidablePred p] (u : Perm (Subtype p)) :
    (ofSubtype u).support = u.support.map (Function.Embedding.subtype p) := by
  ext x
  simp only [mem_support, ne_eq, Finset.mem_map, Function.Embedding.coe_subtype, Subtype.exists,
    exists_and_right, exists_eq_right, not_iff_comm, not_exists, not_not]
  by_cases hx : p x
  · simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]
  · simp only [forall_prop_of_false hx, true_iff, ofSubtype_apply_of_not_mem u hx]

Support of Induced Permutation via Subtype

Informal description

For any decidable predicate $p$ on a type $\alpha$ and any permutation $u$ of the subtype $\{x \in \alpha \mid p(x)\}$, the support of the permutation $\text{ofSubtype}\, u$ (the permutation of $\alpha$ induced by $u$) is equal to the image of the support of $u$ under the canonical embedding of the subtype into $\alpha$.

Equiv.Perm.mem_support_of_mem_noncommProd_support theorem

 {α β : Type*} [DecidableEq β] [Fintype β] {s : Finset α} {f : α → Perm β} {comm : (s : Set α).Pairwise (Commute on f)}
  {x : β} (hx : x ∈ (s.noncommProd f comm).support) : ∃ a ∈ s, x ∈ (f a).support

Full source

theorem mem_support_of_mem_noncommProd_support {α β : Type*} [DecidableEq β] [Fintype β]
    {s : Finset α} {f : α → Perm β}
    {comm : (s : Set α).Pairwise (CommuteCommute on f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) :
    ∃ a ∈ s, x ∈ (f a).support := by
  contrapose! hx
  classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_not_mem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.not_mem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩

Support Element in Noncommutative Product Implies Support in Factor

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ finite and decidable equality. Given a finite set $s \subseteq \alpha$, a family of permutations $f : \alpha \to \text{Perm}(\beta)$, and a pairwise commutativity condition on $f$ over $s$, if an element $x \in \beta$ is in the support of the noncommutative product $\prod_{a \in s} f(a)$, then there exists some $a \in s$ such that $x$ is in the support of $f(a)$.

Equiv.Perm.pow_apply_mem_support theorem

{n : ℕ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

Full source

theorem pow_apply_mem_support {n : ℕ} {x : α} : (f ^ n) x ∈ f.support(f ^ n) x ∈ f.support ↔ x ∈ f.support := by
  simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]

Support Invariance under Powers of a Permutation

Informal description

For any natural number $n$ and any element $x \in \alpha$, the element $(f^n)(x)$ is in the support of $f$ if and only if $x$ is in the support of $f$.

Equiv.Perm.zpow_apply_mem_support theorem

{n : ℤ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

Full source

theorem zpow_apply_mem_support {n : ℤ} {x : α} : (f ^ n) x ∈ f.support(f ^ n) x ∈ f.support ↔ x ∈ f.support := by
  simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]

Support Invariance under Integer Powers of a Permutation

Informal description

For any integer $n$ and any element $x \in \alpha$, the element $(f^n)(x)$ is in the support of $f$ if and only if $x$ is in the support of $f$.

Equiv.Perm.pow_eq_on_of_mem_support theorem

(h : ∀ x ∈ f.support ∩ g.support, f x = g x) (k : ℕ) : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x

Full source

theorem pow_eq_on_of_mem_support (h : ∀ x ∈ f.support ∩ g.support, f x = g x) (k : ℕ) :
    ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x := by
  induction' k with k hk
  · simp
  · intro x hx
    rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
    rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]

Agreement of Permutation Powers on Common Support

Informal description

For permutations $f$ and $g$ of a finite type $\alpha$, if $f(x) = g(x)$ for all $x$ in the intersection of their supports, then for any natural number $k$, the $k$-th powers of $f$ and $g$ agree on all elements in the intersection of their supports, i.e., $(f^k)(x) = (g^k)(x)$ for all $x \in \text{support}(f) \cap \text{support}(g)$.

Equiv.Perm.disjoint_iff_disjoint_support theorem

: Disjoint f g ↔ _root_.Disjoint f.support g.support

Full source

theorem disjoint_iff_disjoint_support : DisjointDisjoint f g ↔ _root_.Disjoint f.support g.support := by
  simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, not_and_or,
    imp_iff_not_or]

Disjoint Permutations iff Disjoint Supports

Informal description

Two permutations $f$ and $g$ of a type $\alpha$ are disjoint if and only if their supports are disjoint as sets, i.e., $f \text{ and } g \text{ are disjoint} \leftrightarrow \text{support}(f) \cap \text{support}(g) = \emptyset$.

Equiv.Perm.Disjoint.disjoint_support theorem

(h : Disjoint f g) : _root_.Disjoint f.support g.support

Full source

theorem Disjoint.disjoint_support (h : Disjoint f g) : _root_.Disjoint f.support g.support :=
  disjoint_iff_disjoint_support.1 h

Disjoint Permutations Have Disjoint Supports

Informal description

If two permutations $f$ and $g$ of a type $\alpha$ are disjoint, then their supports are disjoint as sets, i.e., $\text{support}(f) \cap \text{support}(g) = \emptyset$.

Equiv.Perm.Disjoint.support_mul theorem

(h : Disjoint f g) : (f * g).support = f.support ∪ g.support

Full source

theorem Disjoint.support_mul (h : Disjoint f g) : (f * g).support = f.support ∪ g.support := by
  refine le_antisymm (support_mul_le _ _) fun a => ?_
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  exact
    (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
      ⟨(congr_arg f hg).symm.trans h, hg⟩

Support of Composition of Disjoint Permutations Equals Union of Supports

Informal description

If two permutations $f$ and $g$ of a type $\alpha$ are disjoint, then the support of their composition $f \circ g$ is equal to the union of their individual supports, i.e., $\text{supp}(f \circ g) = \text{supp}(f) \cup \text{supp}(g)$.

Equiv.Perm.support_prod_of_pairwise_disjoint theorem

(l : List (Perm α)) (h : l.Pairwise Disjoint) : l.prod.support = (l.map support).foldr (· ⊔ ·) ⊥

Full source

theorem support_prod_of_pairwise_disjoint (l : List (Perm α)) (h : l.Pairwise Disjoint) :
    l.prod.support = (l.map support).foldr (· ⊔ ·) ⊥ := by
  induction' l with hd tl hl
  · simp
  · rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]

Support of Product of Pairwise Disjoint Permutations Equals Union of Supports

Informal description

For any list $l$ of permutations of a type $\alpha$, if the permutations in $l$ are pairwise disjoint, then the support of their product is equal to the union of their individual supports. That is, \[ \text{supp}\left(\prod_{f \in l} f\right) = \bigcup_{f \in l} \text{supp}(f). \]

Equiv.Perm.support_noncommProd theorem

 {ι : Type*} {k : ι → Perm α} {s : Finset ι} (hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j)) :
  (s.noncommProd k (hs.imp (fun _ _ ↦ Perm.Disjoint.commute))).support = s.biUnion fun i ↦ (k i).support

Full source

theorem support_noncommProd {ι : Type*} {k : ι → Perm α} {s : Finset ι}
    (hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j)) :
    (s.noncommProd k (hs.imp (fun _ _ ↦ Perm.Disjoint.commute))).support =
      s.biUnion fun i ↦ (k i).support := by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

Support of Noncommutative Product of Pairwise Disjoint Permutations Equals Union of Supports

Informal description

Let $\alpha$ be a type, $\iota$ an index type, and $k : \iota \to \text{Perm}(\alpha)$ a family of permutations. For any finite subset $s \subseteq \iota$ where the permutations $\{k_i\}_{i \in s}$ are pairwise disjoint (i.e., $k_i$ and $k_j$ are disjoint for all $i,j \in s$ with $i \neq j$), the support of the noncommutative product $\prod_{i \in s} k_i$ is equal to the union of the supports of the individual permutations $k_i$ for $i \in s$.

Equiv.Perm.support_prod_le theorem

(l : List (Perm α)) : l.prod.support ≤ (l.map support).foldr (· ⊔ ·) ⊥

Full source

theorem support_prod_le (l : List (Perm α)) : l.prod.support ≤ (l.map support).foldr (· ⊔ ·) ⊥ := by
  induction' l with hd tl hl
  · simp
  · rw [List.prod_cons, List.map_cons, List.foldr_cons]
    refine (support_mul_le hd tl.prod).trans ?_
    exact sup_le_sup le_rfl hl

Support of Permutation Product is Contained in Union of Supports

Informal description

For any list $l$ of permutations of a type $\alpha$, the support of the product of permutations in $l$ is contained in the union of their individual supports, i.e., $\text{supp}(\prod_{f \in l} f) \subseteq \bigcup_{f \in l} \text{supp}(f)$.

Equiv.Perm.support_zpow_le theorem

(σ : Perm α) (n : ℤ) : (σ ^ n).support ≤ σ.support

Full source

theorem support_zpow_le (σ : Perm α) (n : ℤ) : (σ ^ n).support ≤ σ.support := fun _ h1 =>
  mem_support.mpr fun h2 => mem_support.mp h1 (zpow_apply_eq_self_of_apply_eq_self h2 n)

Support of Permutation Powers is Contained in Original Support

Informal description

For any permutation $\sigma$ of a type $\alpha$ and any integer $n$, the support of the $n$-th power of $\sigma$ is contained in the support of $\sigma$, i.e., $(\sigma^n).\text{support} \subseteq \sigma.\text{support}$.

Equiv.Perm.support_swap theorem

{x y : α} (h : x ≠ y) : support (swap x y) = { x, y }

Full source

@[simp]
theorem support_swap {x y : α} (h : x ≠ y) : support (swap x y) = {x, y} := by
  ext z
  by_cases hx : z = x
  any_goals simpa [hx] using h.symm
  by_cases hy : z = y
  · simpa [swap_apply_of_ne_of_ne, hx, hy] using h
  · simp [swap_apply_of_ne_of_ne, hx, hy]

Support of a Transposition is the Pair of Swapped Elements

Informal description

For any distinct elements $x$ and $y$ in a type $\alpha$, the support of the permutation $\operatorname{swap}(x, y)$ is the set $\{x, y\}$.

Equiv.Perm.support_swap_iff theorem

(x y : α) : support (swap x y) = { x, y } ↔ x ≠ y

Full source

theorem support_swap_iff (x y : α) : supportsupport (swap x y) = {x, y} ↔ x ≠ y := by
  refine ⟨fun h => ?_, fun h => support_swap h⟩
  rintro rfl
  simp [Finset.ext_iff] at h

Support of a Transposition Equals $\{x, y\}$ if and only if $x \neq y$

Informal description

For any elements $x$ and $y$ in a type $\alpha$, the support of the permutation $\operatorname{swap}(x, y)$ is equal to the set $\{x, y\}$ if and only if $x \neq y$.

Equiv.Perm.support_swap_mul_swap theorem

{x y z : α} (h : List.Nodup [x, y, z]) : support (swap x y * swap y z) = { x, y, z }

Full source

theorem support_swap_mul_swap {x y z : α} (h : List.Nodup [x, y, z]) :
    support (swap x y * swap y z) = {x, y, z} := by
  simp only [List.not_mem_nil, and_true, List.mem_cons, not_false_iff, List.nodup_cons,
    List.mem_singleton, and_self_iff, List.nodup_nil] at h
  push_neg at h
  apply le_antisymm
  · convert support_mul_le (swap x y) (swap y z) using 1
    rw [support_swap h.left.left, support_swap h.right.left]
    simp [Finset.ext_iff]
  · intro
    simp only [mem_insert, mem_singleton]
    rintro (rfl | rfl | rfl | _) <;>
      simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

Support of Composition of Two Transpositions on Three Distinct Elements

Informal description

For any distinct elements $x, y, z$ in a type $\alpha$, the support of the composition of transpositions $\operatorname{swap}(x, y) \circ \operatorname{swap}(y, z)$ is the set $\{x, y, z\}$.

Equiv.Perm.support_swap_mul_ge_support_diff theorem

(f : Perm α) (x y : α) : f.support \ { x, y } ≤ (swap x y * f).support

Full source

theorem support_swap_mul_ge_support_diff (f : Perm α) (x y : α) :
    f.support \ {x, y} ≤ (swap x y * f).support := by
  intro
  simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
    mem_singleton]
  push_neg
  rintro ha ⟨hx, hy⟩ H
  rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
  exact ha H

Support of Composed Permutation Contains Support Difference

Informal description

For any permutation $f$ of a type $\alpha$ and any elements $x, y \in \alpha$, the set difference of the support of $f$ and the set $\{x, y\}$ is a subset of the support of the composition $\operatorname{swap}(x, y) \circ f$. In other words, if an element $z$ is in the support of $f$ but not equal to $x$ or $y$, then $z$ is also in the support of $\operatorname{swap}(x, y) \circ f$.

Equiv.Perm.support_swap_mul_eq theorem

(f : Perm α) (x : α) (h : f (f x) ≠ x) : (swap x (f x) * f).support = f.support \ { x }

Full source

theorem support_swap_mul_eq (f : Perm α) (x : α) (h : f (f x) ≠ x) :
    (swap x (f x) * f).support = f.support \ {x} := by
  by_cases hx : f x = x
  · simp [hx, sdiff_singleton_eq_erase, not_mem_support.mpr hx, erase_eq_of_not_mem]
  ext z
  by_cases hzx : z = x
  · simp [hzx]
  by_cases hzf : z = f x
  · simp [hzf, hx, h, swap_apply_of_ne_of_ne]
  by_cases hzfx : f z = x
  · simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
  · simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]

Support of $\operatorname{swap}(x, f(x)) \circ f$ Equals $f.\text{support} \setminus \{x\}$ When $f(f(x)) \neq x$

Informal description

For a permutation $f$ of a type $\alpha$ and an element $x \in \alpha$ such that $f(f(x)) \neq x$, the support of the permutation $\operatorname{swap}(x, f(x)) \circ f$ is equal to the support of $f$ minus the singleton set $\{x\}$.

Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne theorem

{x y : α} (hy : y ∈ support (swap x (f x) * f)) : y ∈ support f ∧ y ≠ x

Full source

theorem mem_support_swap_mul_imp_mem_support_ne {x y : α} (hy : y ∈ support (swap x (f x) * f)) :
    y ∈ support fy ∈ support f ∧ y ≠ x := by
  simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
  by_cases h : f y = x
  · constructor <;> intro <;> simp_all only [if_true, eq_self_iff_true, not_true, Ne]
  · split_ifs at hy with heq
    · subst heq; exact ⟨h, hy⟩
    · exact ⟨hy, heq⟩

Membership in Support of Composed Permutation Implies Membership in Original Support and Distinctness

Informal description

For any elements $x, y$ in a type $\alpha$ and a permutation $f$ of $\alpha$, if $y$ is in the support of the permutation $\operatorname{swap}(x, f(x)) \circ f$, then $y$ is in the support of $f$ and $y \neq x$.

Equiv.Perm.Disjoint.mem_imp theorem

(h : Disjoint f g) {x : α} (hx : x ∈ f.support) : x ∉ g.support

Full source

theorem Disjoint.mem_imp (h : Disjoint f g) {x : α} (hx : x ∈ f.support) : x ∉ g.support :=
  disjoint_left.mp h.disjoint_support hx

Disjoint Permutations Have Mutually Exclusive Supports

Informal description

For any two disjoint permutations $f$ and $g$ of a type $\alpha$, if an element $x \in \alpha$ belongs to the support of $f$, then $x$ does not belong to the support of $g$.

Equiv.Perm.Disjoint.mono theorem

{x y : Perm α} (h : Disjoint f g) (hf : x.support ≤ f.support) (hg : y.support ≤ g.support) : Disjoint x y

Full source

theorem Disjoint.mono {x y : Perm α} (h : Disjoint f g) (hf : x.support ≤ f.support)
    (hg : y.support ≤ g.support) : Disjoint x y := by
  rw [disjoint_iff_disjoint_support] at h ⊢
  exact h.mono hf hg

Monotonicity of Disjoint Permutations under Support Containment

Informal description

Let $f$ and $g$ be disjoint permutations of a type $\alpha$, and let $x$ and $y$ be permutations of $\alpha$ such that the support of $x$ is contained in the support of $f$ and the support of $y$ is contained in the support of $g$. Then $x$ and $y$ are disjoint permutations.

Equiv.Perm.support_le_prod_of_mem theorem

{l : List (Perm α)} (h : f ∈ l) (hl : l.Pairwise Disjoint) : f.support ≤ l.prod.support

Full source

theorem support_le_prod_of_mem {l : List (Perm α)} (h : f ∈ l) (hl : l.Pairwise Disjoint) :
    f.support ≤ l.prod.support := by
  intro x hx
  rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

Support Containment in Product of Disjoint Permutations

Informal description

Let $l$ be a list of permutations of a type $\alpha$, and let $f$ be a permutation in $l$ such that the permutations in $l$ are pairwise disjoint. Then the support of $f$ is contained in the support of the product of all permutations in $l$.

Equiv.Perm.support_extend_domain theorem

(f : α ≃ Subtype p) {g : Perm α} : support (g.extendDomain f) = g.support.map f.asEmbedding

Full source

@[simp]
theorem support_extend_domain (f : α ≃ Subtype p) {g : Perm α} :
    support (g.extendDomain f) = g.support.map f.asEmbedding := by
  ext b
  simp only [exists_prop, Function.Embedding.coeFn_mk, toEmbedding_apply, mem_map, Ne,
    Function.Embedding.trans_apply, mem_support]
  by_cases pb : p b
  · rw [extendDomain_apply_subtype _ _ pb]
    constructor
    · rintro h
      refine ⟨f.symm ⟨b, pb⟩, ?_, by simp⟩
      contrapose! h
      simp [h]
    · rintro ⟨a, ha, hb⟩
      contrapose! ha
      obtain rfl : a = f.symm ⟨b, pb⟩ := by
        rw [eq_symm_apply]
        exact Subtype.coe_injective hb
      rw [eq_symm_apply]
      exact Subtype.coe_injective ha
  · rw [extendDomain_apply_not_subtype _ _ pb]
    simp only [not_exists, false_iff, not_and, eq_self_iff_true, not_true]
    rintro a _ rfl
    exact pb (Subtype.prop _)

Support of Extended Permutation Equals Image of Original Support

Informal description

Let $f : \alpha \to \{x \mid p(x)\}$ be an equivalence, and let $g$ be a permutation of $\alpha$. Then the support of the extended permutation $g.\text{extendDomain}(f)$ is equal to the image of the support of $g$ under the embedding $f.\text{asEmbedding}$.

Equiv.Perm.card_support_extend_domain theorem

(f : α ≃ Subtype p) {g : Perm α} : #(g.extendDomain f).support = #g.support

Full source

theorem card_support_extend_domain (f : α ≃ Subtype p) {g : Perm α} :
    #(g.extendDomain f).support = #g.support := by simp

Cardinality of Support is Preserved Under Permutation Extension

Informal description

Let $f : \alpha \to \{x \mid p(x)\}$ be an equivalence, and let $g$ be a permutation of $\alpha$. Then the cardinality of the support of the extended permutation $g.\text{extendDomain}(f)$ is equal to the cardinality of the support of $g$.

Equiv.Perm.card_support_eq_zero theorem

{f : Perm α} : #f.support = 0 ↔ f = 1

Full source

theorem card_support_eq_zero {f : Perm α} : #f.support#f.support = 0 ↔ f = 1 := by
  rw [Finset.card_eq_zero, support_eq_empty_iff]

Characterization of Identity Permutation via Empty Support

Informal description

For any permutation $f$ of a finite type $\alpha$, the cardinality of the support of $f$ is zero if and only if $f$ is the identity permutation. In other words, $|\text{supp}(f)| = 0 \Leftrightarrow f = 1$.

Equiv.Perm.one_lt_card_support_of_ne_one theorem

{f : Perm α} (h : f ≠ 1) : 1 < #f.support

Full source

theorem one_lt_card_support_of_ne_one {f : Perm α} (h : f ≠ 1) : 1 < #f.support := by
  simp_rw [one_lt_card_iff, mem_support, ← not_or]
  contrapose! h
  ext a
  specialize h (f a) a
  rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

Non-identity Permutations Have Support Size Greater Than One

Informal description

For any permutation $f$ of a finite type $\alpha$, if $f$ is not the identity permutation, then the number of elements in its support is strictly greater than 1, i.e., $| \text{supp}(f) | > 1$.

Equiv.Perm.card_support_ne_one theorem

(f : Perm α) : #f.support ≠ 1

Full source

theorem card_support_ne_one (f : Perm α) : #f.support#f.support ≠ 1 := by
  by_cases h : f = 1
  · exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one
  · exact ne_of_gt (one_lt_card_support_of_ne_one h)

No Permutation Has Support of Size One

Informal description

For any permutation $f$ of a finite type $\alpha$, the cardinality of the support of $f$ is never equal to 1. In other words, $|\text{supp}(f)| \neq 1$.

Equiv.Perm.card_support_le_one theorem

{f : Perm α} : #f.support ≤ 1 ↔ f = 1

Full source

@[simp]
theorem card_support_le_one {f : Perm α} : #f.support#f.support ≤ 1 ↔ f = 1 := by
  rw [le_iff_lt_or_eq, Nat.lt_succ_iff, Nat.le_zero, card_support_eq_zero, or_iff_not_imp_right,
    imp_iff_right f.card_support_ne_one]

Characterization of Identity Permutation via Small Support

Informal description

For any permutation $f$ of a finite type $\alpha$, the cardinality of the support of $f$ is at most 1 if and only if $f$ is the identity permutation. In other words, $|\text{supp}(f)| \leq 1 \Leftrightarrow f = 1$.

Equiv.Perm.two_le_card_support_of_ne_one theorem

{f : Perm α} (h : f ≠ 1) : 2 ≤ #f.support

Full source

theorem two_le_card_support_of_ne_one {f : Perm α} (h : f ≠ 1) : 2 ≤ #f.support :=
  one_lt_card_support_of_ne_one h

Non-identity Permutations Have Support of Size at Least Two

Informal description

For any permutation $f$ of a finite type $\alpha$, if $f$ is not the identity permutation, then the support of $f$ has at least two elements, i.e., $|\text{supp}(f)| \geq 2$.

Equiv.Perm.card_support_swap_mul theorem

{f : Perm α} {x : α} (hx : f x ≠ x) : #(swap x (f x) * f).support < #f.support

Full source

theorem card_support_swap_mul {f : Perm α} {x : α} (hx : f x ≠ x) :
    #(swap x (f x) * f).support < #f.support :=
  Finset.card_lt_card
    ⟨fun _ hz => (mem_support_swap_mul_imp_mem_support_ne hz).left, fun h =>
      absurd (h (mem_support.2 hx)) (mt mem_support.1 (by simp))⟩

Decrease in Support Cardinality under Swap Composition

Informal description

For any permutation $f$ of a finite type $\alpha$ and any element $x \in \alpha$ such that $f(x) \neq x$, the support of the permutation $\operatorname{swap}(x, f(x)) \circ f$ has strictly smaller cardinality than the support of $f$.

Equiv.Perm.card_support_swap theorem

{x y : α} (hxy : x ≠ y) : #(swap x y).support = 2

Full source

theorem card_support_swap {x y : α} (hxy : x ≠ y) : #(swap x y).support = 2 :=
  show #(swap x y).support = #⟨x ::ₘ y ::ₘ 0, by simp [hxy]⟩ from
    congr_arg card <| by simp [support_swap hxy, *, Finset.ext_iff]

Cardinality of Support of a Transposition is Two

Informal description

For any distinct elements $x$ and $y$ in a type $\alpha$, the support of the transposition $\operatorname{swap}(x, y)$ has cardinality 2, i.e., $|\operatorname{supp}(\operatorname{swap}(x, y))| = 2$.

Equiv.Perm.card_support_eq_two theorem

{f : Perm α} : #f.support = 2 ↔ IsSwap f

Full source

@[simp]
theorem card_support_eq_two {f : Perm α} : #f.support#f.support = 2 ↔ IsSwap f := by
  constructor <;> intro h
  · obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
    obtain ⟨y, rfl⟩ := card_eq_one.1 ht
    rw [mem_singleton] at hmem
    refine ⟨x, y, hmem, ?_⟩
    ext a
    have key : ∀ b, f b ≠ bf b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
    by_cases ha : f a = a
    · have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
      rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
    · have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
      obtain rfl | rfl := (key a).mp ha
      · rw [Or.resolve_left ha' ha, swap_apply_left]
      · rw [Or.resolve_right ha' ha, swap_apply_right]
  · obtain ⟨x, y, hxy, rfl⟩ := h
    exact card_support_swap hxy

Transposition Characterization via Support Cardinality: $|\operatorname{supp}(f)| = 2 \leftrightarrow f \text{ is a transposition}$

Informal description

For a permutation $f$ of a finite type $\alpha$, the support of $f$ has cardinality 2 if and only if $f$ is a transposition (i.e., there exist distinct elements $x, y \in \alpha$ such that $f = \operatorname{swap}(x, y)$).

Equiv.Perm.Disjoint.card_support_mul theorem

(h : Disjoint f g) : #(f * g).support = #f.support + #g.support

Full source

theorem Disjoint.card_support_mul (h : Disjoint f g) :
    #(f * g).support = #f.support + #g.support := by
  rw [← Finset.card_union_of_disjoint]
  · congr
    ext
    simp [h.support_mul]
  · simpa using h.disjoint_support

Cardinality of Support of Composition of Disjoint Permutations Equals Sum of Supports

Informal description

For two disjoint permutations $f$ and $g$ of a finite type $\alpha$, the cardinality of the support of their composition $f \circ g$ is equal to the sum of the cardinalities of their individual supports, i.e., $|\operatorname{supp}(f \circ g)| = |\operatorname{supp}(f)| + |\operatorname{supp}(g)|$.

Equiv.Perm.card_support_prod_list_of_pairwise_disjoint theorem

{l : List (Perm α)} (h : l.Pairwise Disjoint) : #l.prod.support = (l.map (card ∘ support)).sum

Full source

theorem card_support_prod_list_of_pairwise_disjoint {l : List (Perm α)} (h : l.Pairwise Disjoint) :
    #l.prod.support = (l.map (cardcard ∘ support)).sum := by
  induction' l with a t ih
  · exact card_support_eq_zero.mpr rfl
  · obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul

Cardinality of Support of Product of Pairwise Disjoint Permutations Equals Sum of Supports

Informal description

For a list $l$ of pairwise disjoint permutations of a finite type $\alpha$, the cardinality of the support of their product is equal to the sum of the cardinalities of their individual supports, i.e., $$|\operatorname{supp}(\prod l)| = \sum_{f \in l} |\operatorname{supp}(f)|.$$

Equiv.Perm.support_subtype_perm theorem

[DecidableEq α] {s : Finset α} (f : Perm α) (h) : (f.subtypePerm h : Perm s).support = ({x | f x ≠ x} : Finset s)

Full source

@[simp]
theorem support_subtype_perm [DecidableEq α] {s : Finset α} (f : Perm α) (h) :
    (f.subtypePerm h : Perm s).support = ({x | f x ≠ x} : Finset s) := by
  ext; simp [Subtype.ext_iff]

Support of Restricted Permutation Equals Non-Fixed Points in Subset

Informal description

Let $\alpha$ be a type with decidable equality and let $s$ be a finite subset of $\alpha$. For any permutation $f$ of $\alpha$ satisfying the condition $h$ (that $f$ preserves $s$), the support of the restricted permutation $f_{\mid s}$ (as a permutation of $s$) is equal to the set $\{x \in s \mid f(x) \neq x\}$.

Equiv.Perm.fixed_point_card_lt_of_ne_one theorem

[DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) : #{x | σ x = x} < Fintype.card α - 1

Full source

theorem fixed_point_card_lt_of_ne_one [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ ≠ 1) :
    #{x | σ x = x} < Fintype.card α - 1 := by
  rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]
  exact one_lt_card_support_of_ne_one h

Non-identity Permutations Have Fewer Than $|\alpha| - 1$ Fixed Points

Informal description

Let $\alpha$ be a finite type with decidable equality, and let $\sigma$ be a permutation of $\alpha$ that is not the identity permutation. Then the number of fixed points of $\sigma$ is strictly less than $|\alpha| - 1$, i.e., $$|\{x \in \alpha \mid \sigma(x) = x\}| < |\alpha| - 1.$$

Equiv.Perm.support_conj theorem

: (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding

Full source

@[simp]
theorem support_conj : (σ * τ * σ⁻¹).support = τ.support.map σ.toEmbedding := by
  ext
  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support,
    Equiv.eq_symm_apply, inv_def]

Support of Conjugate Permutation Equals Image of Support

Informal description

For any permutations $\sigma$ and $\tau$ of a type $\alpha$, the support of the conjugate permutation $\sigma \tau \sigma^{-1}$ is equal to the image of the support of $\tau$ under the embedding induced by $\sigma$. That is, $\text{supp}(\sigma \tau \sigma^{-1}) = \sigma(\text{supp}(\tau))$.

Equiv.Perm.card_support_conj theorem

: #(σ * τ * σ⁻¹).support = #τ.support

Full source

theorem card_support_conj : #(σ * τ * σ⁻¹).support = #τ.support := by simp

Cardinality of Support is Preserved Under Conjugation

Informal description

For any permutations $\sigma$ and $\tau$ of a finite type $\alpha$, the cardinality of the support of the conjugate permutation $\sigma \tau \sigma^{-1}$ is equal to the cardinality of the support of $\tau$. That is, $|\text{supp}(\sigma \tau \sigma^{-1})| = |\text{supp}(\tau)|$.

Main definitions