diff options
Diffstat (limited to 'Nominal/Basic.lean')
| -rw-r--r-- | Nominal/Basic.lean | 76 |
1 files changed, 61 insertions, 15 deletions
diff --git a/Nominal/Basic.lean b/Nominal/Basic.lean index 7bc6e1c..1a7f6ac 100644 --- a/Nominal/Basic.lean +++ b/Nominal/Basic.lean @@ -31,17 +31,21 @@ instance : PermSet 𝔸 (FPerm 𝔸) where one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl +class DiscretePermSet (X : Type) extends PermSet 𝔸 X where + is_discrete : ∀ (x : X) (π : FPerm 𝔸), π • x = x + /-- A discrete (FPerm 𝔸)-Set where permutations do not change anything. -/ -def PermSet.discrete (X : Type) : PermSet 𝔸 X where +def PermSet.discrete (X : Type) : DiscretePermSet 𝔸 X where smul π x := x one_smul := by intro; rfl mul_smul := by intro _ _ _; rfl + is_discrete := by intro _ _; rfl /-- We consider Unit a discrete (FPerm 𝔸)-Set. -/ -instance : PermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit +instance : DiscretePermSet 𝔸 Unit := PermSet.discrete 𝔸 Unit /-- We consider Bool a discrete (FPerm 𝔸)-Set. -/ -instance : PermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool +instance : DiscretePermSet 𝔸 Bool := PermSet.discrete 𝔸 Bool end PermSet @@ -117,13 +121,13 @@ end Support /-! ## Basic Nominal Set Definition -Nominal sets are then just G-Sets where all elements are finitely supported. +Nominal sets are then just (FPerm 𝔸)-Sets where all elements are finitely supported. -/ section NominalSet variable (𝔸 : Type) -/-- A G-Set X is nominal if every x ∈ X is finitely supported. -/ +/-- An (FPerm 𝔸)-Set X is nominal if every x ∈ X is finitely supported. -/ class NominalSet (X : Type) extends PermSet 𝔸 X where finsupp : ∀ (x : X), ∃ (S : Set 𝔸), PermSet.HasSupport 𝔸 x S ∧ S.Finite @@ -132,7 +136,7 @@ namespace NominalSet variable {X : Type} [nom : NominalSet 𝔸 X] /-- For every element x of a nominal set, there exists a least finite support, denoted "supp x". --/ -noncomputable def supp (x : X) : Set 𝔸 := +def supp (x : X) : Set 𝔸 := ⋂₀ { S : Set 𝔸 | PermSet.HasSupport 𝔸 x S ∧ S.Finite } /-- The least finite support in a nominal set is always finite. -/ @@ -173,38 +177,80 @@ lemma supp_is_support {x : X} : PermSet.HasSupport 𝔸 x (supp 𝔸 x) := by · intro T hT exact hT.right +lemma support_subset_supp {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → supp 𝔸 x ⊆ S := by + intro hsupp hfin + apply Set.sInter_subset_of_mem + exact ⟨hsupp, hfin⟩ + end NominalSet +private lemma NominalSet.supp_atoms' {a : 𝔸} : PermSet.HasSupport 𝔸 a {a} := by + simp [PermSet.fix'] + /-- The set of atoms is a nominal set, where supp a = {a}. -/ instance : NominalSet 𝔸 𝔸 where finsupp := by intro a use {a} constructor - · intro π hπ - aesop + · exact NominalSet.supp_atoms' 𝔸 · simp --- TODO: Prove supp a = {a} +lemma NominalSet.supp_atoms [Infinite 𝔸] [DecidableEq 𝔸] {a : 𝔸} : supp 𝔸 a = {a} := by + ext b; constructor + · apply support_subset_supp + · apply NominalSet.supp_atoms' + · simp + · suffices : a ∈ supp 𝔸 a + -- TODO: Shorten + · simp; intro h; rw [h]; assumption + · intro S ⟨hsuppS, hfinS⟩ + by_contra + have hfin : ({a} ∪ S).Finite := by + apply Set.finite_union.mpr; simp [hfinS] + obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset hfin.toFinset + have h₁ : c ≠ a := by aesop + have h₂ : c ∉ S := by aesop + have h₃ : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by + intro d hd + rw [show ⸨a,c⸩ • d = (Equiv.swap a c) d from rfl] + apply Equiv.Perm.supp_notin + rw [Equiv.Perm.supp_swap] + aesop + have h₄ : ⸨a, c⸩ • a = c := by + simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] + unfold PermSet.HasSupport at hsuppS + specialize hsuppS h₃ + simp [PermSet.fix'] at hsuppS + aesop + +class DiscreteNominalSet (X : Type) extends NominalSet 𝔸 X, DiscretePermSet 𝔸 X + +private lemma NominalSet.supp_discrete' {X : Type} [disc : DiscretePermSet 𝔸 X] {x : X} : PermSet.HasSupport 𝔸 x ∅ := by + intro π hπ + simp [PermSet.fix'] + exact DiscretePermSet.is_discrete x π /-- Every set can be made into a discrete nominal set where every element has empty support. -/ -def NominalSet.discrete (X : Type) : NominalSet 𝔸 X := +def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X := { PermSet.discrete 𝔸 X with finsupp := by intro x use {} constructor - · intro π hπ - aesop + · intro π hπ; simp [PermSet.fix']; rfl · simp } --- TODO: Prove supp x = ∅ +lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by + rw [← Set.subset_empty_iff] + apply Set.sInter_subset_of_mem + exact ⟨NominalSet.supp_discrete' 𝔸, Set.finite_empty⟩ /-- We consider Unit a discrete nominal set. -/ -instance : NominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit +instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit /-- We consider Bool a discrete nominal set. -/ -instance : NominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool +instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool end NominalSet |