diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 79a5042..0a4974a 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -187,12 +187,29 @@ class PermSet (๐ธ : Type) [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] variable (๐ธ : Type) [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] +/-- An (FPerm ๐ธ)-set is orbit-finite if there are only finitely many different orbits. -/ +class OrbitFinite (X : Type) [PermSet ๐ธ X] where + fin_orbits : Finite (Quotient (MulAction.orbitRel (FPerm ๐ธ) X)) + /-- 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 +instance : OrbitFinite ๐ธ ๐ธ where + fin_orbits := Finite.of_equiv Unit + { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty ๐ธ)).some + invFun _ := () + right_inv := by + let chosen := (inferInstanceAs (Nonempty ๐ธ)).some + apply Quotient.ind; intro a + rw [Quotient.eq] + show chosen โ MulAction.orbit (FPerm ๐ธ) a + use โธจchosen, aโธฉ + exact FPerm.swap_apply_right chosen a + } + /-- The set of finite permutations forms an (FPerm ๐ธ)-Set. -/ instance : PermSet ๐ธ (FPerm ๐ธ) where smul ฯ ฯ := ฯ * ฯ |