Permutations

This file defines finite permutations and related operations.

structure NominalSets.Perm (𝔸 : Type u_1) : Type u_1

The type of finite permutations on a type 𝔸.

• toFun : 𝔸 → 𝔸

  The forward permutation.

• invFun : 𝔸 → 𝔸

  The inverse permutation.

• right_inverse' (a : 𝔸) : self.toFun (self.invFun a) = a

  invFun is a right inverse of toFun.

• left_inverse' (a : 𝔸) : self.invFun (self.toFun a) = a

  invFun is a left inverse of toFun.

• has_supp' : ∃ (A : Finset 𝔸), ∀ a ∉ A, self.toFun a = a

  toFun is finitely supported.

instance NominalSets.Perm.instFunLike {𝔸 : Type u_1} : FunLike (Perm 𝔸) 𝔸 𝔸

Equations

• NominalSets.Perm.instFunLike = { coe := NominalSets.Perm.toFun, coe_injective' := ⋯ }

instance NominalSets.Perm.instInv {𝔸 : Type u_1} : Inv (Perm 𝔸)

Equations

• NominalSets.Perm.instInv = { inv := fun (π : NominalSets.Perm 𝔸) => { toFun := π.invFun, invFun := π.toFun, right_inverse' := ⋯, left_inverse' := ⋯, has_supp' := ⋯ } }

def NominalSets.Perm.Simps.coe {𝔸 : Type u_1} (π : Perm 𝔸) : 𝔸 → 𝔸

A simps projection for function coercion.

Equations

• NominalSets.Perm.Simps.coe π = ⇑π

def NominalSets.Perm.Simps.inv_coe {𝔸 : Type u_1} (π : Perm 𝔸) : 𝔸 → 𝔸

A simps projection for inverse function coercion.

Equations

• NominalSets.Perm.Simps.inv_coe π = ⇑π⁻¹

@[simp]

theorem NominalSets.Perm.right_inverse {𝔸 : Type u_1} (π : Perm 𝔸) (a : 𝔸) : π (π⁻¹ a) = a

@[simp]

theorem NominalSets.Perm.left_inverse {𝔸 : Type u_1} (π : Perm 𝔸) (a : 𝔸) : π⁻¹ (π a) = a

theorem NominalSets.Perm.has_supp {𝔸 : Type u_1} (π : Perm 𝔸) : ∃ (A : Finset 𝔸), ∀ a ∉ A, π a = a

instance NominalSets.Perm.instOne {𝔸 : Type u_1} : One (Perm 𝔸)

Equations

• NominalSets.Perm.instOne = { one := { toFun := fun (a : 𝔸) => a, invFun := fun (a : 𝔸) => a, right_inverse' := ⋯, left_inverse' := ⋯, has_supp' := ⋯ } }

@[simp]

theorem NominalSets.Perm.one_coe {𝔸 : Type u_1} (a : 𝔸) : 1 a = a

@[simp]

theorem NominalSets.Perm.one_inv_coe {𝔸 : Type u_1} (a : 𝔸) : 1⁻¹ a = a

instance NominalSets.Perm.instMul {𝔸 : Type u_1} : Mul (Perm 𝔸)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NominalSets.Perm.mul_inv_coe {𝔸 : Type u_1} (π₁ π₂ : Perm 𝔸) (a : 𝔸) : (π₁ * π₂)⁻¹ a = π₂⁻¹ (π₁⁻¹ a)

@[simp]

theorem NominalSets.Perm.mul_coe {𝔸 : Type u_1} (π₁ π₂ : Perm 𝔸) (a : 𝔸) : (π₁ * π₂) a = π₁ (π₂ a)

def NominalSets.Perm.swap {𝔸 : Type u_1} (a b : 𝔸) [DecidableEq 𝔸] : Perm 𝔸

The permutation that simply swaps two elements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NominalSets.Perm.swap_coe {𝔸 : Type u_1} (a b : 𝔸) [DecidableEq 𝔸] (c : 𝔸) : (swap a b) c = if a = c then b else if b = c then a else c

@[simp]

theorem NominalSets.Perm.swap_inv_coe {𝔸 : Type u_1} (a b : 𝔸) [DecidableEq 𝔸] (c : 𝔸) : (swap a b)⁻¹ c = if a = c then b else if b = c then a else c

def NominalSets.Perm.seq {𝔸 : Type u_1} [DecidableEq 𝔸] : List (𝔸 × 𝔸) → Perm 𝔸

A sequence of pairs induces a permutation constructed as a sequences of swaps.

Equations

• NominalSets.Perm.seq [] = 1
• NominalSets.Perm.seq ((a, b) :: xs) = NominalSets.Perm.swap a b * NominalSets.Perm.seq xs