Finite Permutations

This file defines finite permutations of atoms - permutations that only move finitely many atoms. This is the key structure for nominal set theory.

Main definitions

• FinPerm - Finite permutations (bijections on atoms with finite support)
• FinPerm.swap - Transposition of two atoms

Implementation notes

Since Atom is infinite (not Fintype), we cannot use Mathlib's Perm.support directly (which requires Fintype). Instead, we define a predicate IsFinitelySupported that states a permutation has finite support, and define FinPerm as the subtype of permutations satisfying this predicate.

Key insight: in nominal set theory, we only work with finitely-supported permutations, even though the set of atoms is infinite.

References

• Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013, Chapter 2.
• Larsen and Schürmann, Nominal State-Separating Proofs, IACR ePrint 2025/598 — the SSProve Nominal/ layer this development ports.
• SSProve theories/Crypt/nominal/Nominal.v

def CatCrypt.Nominal.IsFinitelySupported (π : Equiv.Perm Atom) : Prop

A permutation is finitely supported if there exists a finite set outside of which it acts as the identity.

Equations

• CatCrypt.Nominal.IsFinitelySupported π = ∃ (s : Finset CatCrypt.Nominal.Atom), ∀ a ∉ s, π a = a

def CatCrypt.Nominal.FinPerm : Type

The type of finitely-supported permutations of atoms.

Equations

• CatCrypt.Nominal.FinPerm = { π : Equiv.Perm CatCrypt.Nominal.Atom // CatCrypt.Nominal.IsFinitelySupported π }

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instCoeOutPermAtom : CoeOut FinPerm (Equiv.Perm Atom)

Coercion to underlying permutation

Equations

• CatCrypt.Nominal.FinPerm.instCoeOutPermAtom = { coe := Subtype.val }

def CatCrypt.Nominal.FinPerm.apply (π : FinPerm) (a : Atom) : Atom

Apply permutation to an atom

Equations

• π.apply a = ↑π a

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instCoeFunForallAtom : CoeFun FinPerm fun (x : FinPerm) => Atom → Atom

Equations

• CatCrypt.Nominal.FinPerm.instCoeFunForallAtom = { coe := CatCrypt.Nominal.FinPerm.apply }

@[simp]

theorem CatCrypt.Nominal.FinPerm.apply_def (π : FinPerm) (a : Atom) : π.apply a = ↑π a

theorem CatCrypt.Nominal.FinPerm.val_injective : Function.Injective Subtype.val

theorem CatCrypt.Nominal.FinPerm.ext {π₁ π₂ : FinPerm} (h : ∀ (a : Atom), π₁.apply a = π₂.apply a) : π₁ = π₂

theorem CatCrypt.Nominal.FinPerm.ext_iff {π₁ π₂ : FinPerm} : π₁ = π₂ ↔ ∀ (a : Atom), π₁.apply a = π₂.apply a

noncomputable def CatCrypt.Nominal.FinPerm.suppWitness (π : FinPerm) : Finset Atom

A witness of finite support for a permutation

Equations

• π.suppWitness = Classical.choose ⋯

theorem CatCrypt.Nominal.FinPerm.suppWitness_spec (π : FinPerm) (a : Atom) : a ∉ π.suppWitness → π.apply a = a

def CatCrypt.Nominal.FinPerm.one : FinPerm

Identity permutation

Equations

• CatCrypt.Nominal.FinPerm.one = ⟨1, CatCrypt.Nominal.FinPerm.one._proof_1⟩

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instOne : One FinPerm

Equations

• CatCrypt.Nominal.FinPerm.instOne = { one := CatCrypt.Nominal.FinPerm.one }

@[simp]

theorem CatCrypt.Nominal.FinPerm.one_apply (a : Atom) : apply 1 a = a

@[simp]

theorem CatCrypt.Nominal.FinPerm.one_val : ↑1 = 1

def CatCrypt.Nominal.FinPerm.mul (π₁ π₂ : FinPerm) : FinPerm

Composition of finite permutations

Equations

• π₁.mul π₂ = ⟨↑π₁ * ↑π₂, ⋯⟩

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instMul : Mul FinPerm

Equations

• CatCrypt.Nominal.FinPerm.instMul = { mul := CatCrypt.Nominal.FinPerm.mul }

@[simp]

theorem CatCrypt.Nominal.FinPerm.mul_apply (π₁ π₂ : FinPerm) (a : Atom) : (π₁ * π₂).apply a = π₁.apply (π₂.apply a)

@[simp]

theorem CatCrypt.Nominal.FinPerm.mul_val (π₁ π₂ : FinPerm) : ↑(π₁ * π₂) = ↑π₁ * ↑π₂

def CatCrypt.Nominal.FinPerm.inv (π : FinPerm) : FinPerm

Inverse of a finite permutation

Equations

• π.inv = ⟨(↑π)⁻¹, ⋯⟩

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instInv : Inv FinPerm

Equations

• CatCrypt.Nominal.FinPerm.instInv = { inv := CatCrypt.Nominal.FinPerm.inv }

@[simp]

theorem CatCrypt.Nominal.FinPerm.inv_apply (π : FinPerm) (a : Atom) : π⁻¹.apply a = (Equiv.symm ↑π) a

@[simp]

theorem CatCrypt.Nominal.FinPerm.inv_val (π : FinPerm) : ↑π⁻¹ = (↑π)⁻¹

@[implicit_reducible]

instance CatCrypt.Nominal.FinPerm.instGroup : Group FinPerm

Finite permutations form a group

Equations

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

noncomputable def CatCrypt.Nominal.FinPerm.swap (a b : Atom) : FinPerm

Transposition: swap two atoms

Equations

• CatCrypt.Nominal.FinPerm.swap a b = ⟨Equiv.swap a b, ⋯⟩

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_apply_left (a b : Atom) : (swap a b).apply a = b

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_apply_right (a b : Atom) : (swap a b).apply b = a

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_apply_of_ne_of_ne {a b c : Atom} (hca : c ≠ a) (hcb : c ≠ b) : (swap a b).apply c = c

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_val (a b : Atom) : ↑(swap a b) = Equiv.swap a b

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_self (a : Atom) : swap a a = 1

theorem CatCrypt.Nominal.FinPerm.swap_comm (a b : Atom) : swap a b = swap b a

theorem CatCrypt.Nominal.FinPerm.swap_swap (a b : Atom) : swap a b * swap a b = 1

@[simp]

theorem CatCrypt.Nominal.FinPerm.swap_inv (a b : Atom) : (swap a b)⁻¹ = swap a b