From d75abcb4dc8bdc9feb93941f05d2e162abaf0af3 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 23 Oct 2025 13:24:26 +0200 Subject: add equivariant instances --- Nominal/Permutations.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'Nominal/Permutations.lean') diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index c8fdd86..4a3e88f 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -141,16 +141,21 @@ class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] -/-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/ +/-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 𝔸 where smul π a := π a one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl -/-- The set of finite permutations forms a (FPerm 𝔸)-Set. -/ +/-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/ instance : PermSet 𝔸 (FPerm 𝔸) where smul π τ := π * τ one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl +open Pointwise + +/-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/ +instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where + end PermSet -- cgit v1.3.1