Mathlib.GroupTheory.Perm.Basic

Module docstring

{"# Extra lemmas about permutations

This file proves miscellaneous lemmas about Equiv.Perm.

TODO

Most of the content of this file was moved to Algebra.Group.End in https://github.com/leanprover-community/mathlib4/pull/22141. It would be good to merge the remaining lemmas with other files, eg GroupTheory.Perm.ViaEmbedding looks like it could benefit from such a treatment (splitting into the algebra and non-algebra parts) "}

Equiv.Perm.image_inv theorem

(f : Perm α) (s : Set α) : ↑f⁻¹ '' s = f ⁻¹' s

Full source

@[simp] lemma image_inv (f : Perm α) (s : Set α) : ↑f⁻¹ '' s = f ⁻¹' s := f⁻¹.image_eq_preimage _

Image under Inverse Permutation Equals Preimage under Permutation

Informal description

For any permutation $f$ of a type $\alpha$ and any subset $s \subseteq \alpha$, the image of $s$ under the inverse permutation $f^{-1}$ is equal to the preimage of $s$ under $f$, i.e., $f^{-1}(s) = f^{-1}(s)$.

Equiv.Perm.preimage_inv theorem

(f : Perm α) (s : Set α) : ↑f⁻¹ ⁻¹' s = f '' s

Full source

@[simp] lemma preimage_inv (f : Perm α) (s : Set α) : ↑f⁻¹ ⁻¹' s = f '' s :=
  (f.image_eq_preimage _).symm

Preimage under Inverse Permutation Equals Image under Permutation

Informal description

For any permutation $f$ of a type $\alpha$ and any subset $s \subseteq \alpha$, the preimage of $s$ under the inverse permutation $f^{-1}$ is equal to the image of $s$ under $f$, i.e., $f^{-1}(s) = f(s)$.

Equiv.swap_smul_self_smul theorem

[MulAction (Perm α) β] (i j : α) (x : β) : swap i j • swap i j • x = x

Full source

@[simp]
theorem swap_smul_self_smul [MulAction (Perm α) β] (i j : α) (x : β) :
    swap i j • swap i j • x = x := by simp [smul_smul]

Double swap action returns original element

Informal description

Let $\alpha$ and $\beta$ be types with a multiplicative action of the permutation group $\text{Perm}(\alpha)$ on $\beta$. For any elements $i, j \in \alpha$ and any $x \in \beta$, applying the swap permutation $\text{swap}(i,j)$ twice to $x$ via the action returns $x$ itself, i.e., $\text{swap}(i,j) \cdot (\text{swap}(i,j) \cdot x) = x$.

Equiv.swap_smul_involutive theorem

[MulAction (Perm α) β] (i j : α) : Function.Involutive (swap i j • · : β → β)

Full source

theorem swap_smul_involutive [MulAction (Perm α) β] (i j : α) :
    Function.Involutive (swap i j • · : β → β) := swap_smul_self_smul i j

Involutivity of Swap Action: $(\text{swap}(i,j) \cdot)^2 = \text{id}$

Informal description

Let $\alpha$ and $\beta$ be types with a multiplicative action of the permutation group $\text{Perm}(\alpha)$ on $\beta$. For any elements $i, j \in \alpha$, the function $x \mapsto \text{swap}(i,j) \cdot x$ from $\beta$ to $\beta$ is involutive, meaning that applying it twice returns the original element, i.e., $\text{swap}(i,j) \cdot (\text{swap}(i,j) \cdot x) = x$ for all $x \in \beta$.

Set.BijOn.perm_inv theorem

(hf : BijOn f s s) : BijOn (↑(f⁻¹)) s s

Full source

lemma BijOn.perm_inv (hf : BijOn f s s) : BijOn ↑(f⁻¹) s s := hf.symm f.invOn

Bijectivity of Inverse Permutation on a Set

Informal description

Let $f$ be a function from a set $s$ to itself. If $f$ is bijective on $s$, then its inverse function $f^{-1}$ is also bijective on $s$.

Set.MapsTo.perm_pow theorem

: MapsTo f s s → ∀ n : ℕ, MapsTo (f ^ n) s s

Full source

lemma MapsTo.perm_pow : MapsTo f s s → ∀ n : ℕ, MapsTo (f ^ n) s s := by
  simp_rw [Equiv.Perm.coe_pow]; exact MapsTo.iterate

Iterated Function Preserves Mapping Property on a Set

Informal description

Let $f$ be a function from a set $s$ to itself. If $f$ maps $s$ into $s$ (i.e., $f(x) \in s$ for all $x \in s$), then for any natural number $n$, the $n$-th iterate of $f$ (denoted $f^n$) also maps $s$ into $s$.

Set.SurjOn.perm_pow theorem

: SurjOn f s s → ∀ n : ℕ, SurjOn (f ^ n) s s

Full source

lemma SurjOn.perm_pow : SurjOn f s s → ∀ n : ℕ, SurjOn (f ^ n) s s := by
  simp_rw [Equiv.Perm.coe_pow]; exact SurjOn.iterate

Iterated Function Preserves Surjectivity on a Set

Informal description

Let $f$ be a function from a set $s$ to itself. If $f$ is surjective on $s$, then for any natural number $n$, the $n$-th iterate of $f$ (denoted $f^n$) is also surjective on $s$.

Set.BijOn.perm_pow theorem

: BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s

Full source

lemma BijOn.perm_pow : BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s := by
  simp_rw [Equiv.Perm.coe_pow]; exact BijOn.iterate

Iterated Bijections Preserve Bijectivity on a Set

Informal description

Let $f$ be a function that is bijective on a set $s$ (i.e., $f$ is both injective and surjective when restricted to $s$). Then for any natural number $n$, the $n$-th iterate of $f$ (denoted $f^n$) is also bijective on $s$.

Set.BijOn.perm_zpow theorem

(hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s

Full source

lemma BijOn.perm_zpow (hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s
  | Int.ofNat n => hf.perm_pow n
  | Int.negSucc n => (hf.perm_pow (n + 1)).perm_inv

Integer Iterates Preserve Bijectivity on a Set

Informal description

Let $f$ be a function from a set $s$ to itself. If $f$ is bijective on $s$, then for any integer $n$, the $n$-th iterate of $f$ (denoted $f^n$) is also bijective on $s$.