diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-23 13:24:26 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-23 13:24:26 +0200 |
| commit | d75abcb4dc8bdc9feb93941f05d2e162abaf0af3 (patch) | |
| tree | 142ea01ebabeb41d233686a74bb04551579a0b6d /Nominal/Permutations.lean | |
| parent | fe96f2d6674bda67b66d5c8c5ce7eea4e2b26031 (diff) | |
add equivariant instances
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 9 |
1 files changed, 7 insertions, 2 deletions
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 |