always require infinite, countable, equality-decidable atoms

3 files changed, 12 insertions, 12 deletions

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index 057a0de..dcf079f 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -8,7 +8,7 @@ import Nominal.Support
 This file contains common instances of (FPerm 𝔸)-sets and nominal sets.
 -/
 
-variable (𝔸 : Type)
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 /-!
 ## Atoms
@@ -25,7 +25,7 @@ instance : NominalSet 𝔸 𝔸 where
     intro a; use {a}
     exact ⟨NominalSet.supp_atom' 𝔸, Set.finite_singleton a⟩
 
-lemma NominalSet.supp_atom [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by
+lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
   ext b; constructor
   · apply support_subset_supp 𝔸
     · exact NominalSet.supp_atom' 𝔸
@@ -90,7 +90,7 @@ section Products
 
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where
 
-variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by
   intro π hπ
@@ -135,7 +135,7 @@ section Coproducts
 
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where
 
-variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y] [Infinite 𝔸]
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by
   intro π hπ
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index dd9b9d2..c8fdd86 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -136,10 +136,10 @@ Sets equipped with a permutation operation.
 -/
 section PermSet
 
-variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
-
 /-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
-class PermSet (X : Type) extends MulAction (FPerm 𝔸) X
+class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) extends MulAction (FPerm 𝔸) X
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 /-- The set of atoms itself forms a (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 𝔸 where
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index efed617..78e8b3e 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -8,7 +8,7 @@ import Nominal.Helpers.Finset
 This file provides basic definitions for support of (FPerm 𝔸)-sets and nominal sets.
 -/
 
-variable (𝔸 : Type)
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 /-!
 ## Support Definitions
@@ -54,7 +54,7 @@ lemma support_superset {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S ⊆
   exact hπ a (hsub ha)
 
 /-- For two finite supports, the intersection is also a support. -/
-lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
+lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite → HasSupport 𝔸 x T → T.Finite → HasSupport 𝔸 x (S ∩ T) := by
   intro h_S_support h_S_finite h_T_support h_T_finite π h_π_fix
   let π' := π.val
   let h_π_fin := π.prop
@@ -151,7 +151,7 @@ lemma support_inter [Infinite 𝔸] {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x
     _     = x                               := by rw [h_T_support h_σ_fixT]
 
 /-- For a finite number of finite supports, the intersection is also a support. -/
-lemma support_sInter [Infinite 𝔸] {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
+lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C) := by
   suffices (C : Finset (Set 𝔸)) : C.Nonempty → (∀ S ∈ C, HasSupport 𝔸 x S ∧ S.Finite) → HasSupport 𝔸 x (⋂₀ C.toSet) ∧ (⋂₀ C.toSet).Finite
   · intro hfin
     rw [show C = hfin.toFinset.toSet by simp]
@@ -207,7 +207,7 @@ lemma supp_finite {x : X} : (supp 𝔸 x).Finite := by
     exact Set.mem_sep hsuppS hfinS
 
 /-- We can restrict the supp definition to subsets of a single finite support. -/
-private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite } := by
+private lemma supp_equiv_finite {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x = ⋂₀ { T : Set 𝔸 | T ⊆ S ∧ PermSet.HasSupport 𝔸 x T ∧ T.Finite } := by
   intro hsuppS hfinS
   unfold supp; ext a
   constructor
@@ -223,7 +223,7 @@ private lemma supp_equiv_finite [Infinite 𝔸] {x : X} {S : Set 𝔸} : PermSet
       · exact Set.Finite.inter_of_left hfinS T
 
 /-- The least finite support is itself a support. -/
-lemma supp_is_support [Infinite 𝔸] {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
+lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by
   obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.fin_supp x
   rw [supp_equiv_finite 𝔸 hsuppS hfinS]
   apply PermSet.support_sInter