diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Instances.lean | 91 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 40 | ||||
| -rw-r--r-- | Nominal/Support.lean (renamed from Nominal/Basic.lean) | 131 |
3 files changed, 139 insertions, 123 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean new file mode 100644 index 0000000..793baa4 --- /dev/null +++ b/Nominal/Instances.lean @@ -0,0 +1,91 @@ +import Nominal.Permutations +import Nominal.Support + +/-! +# Instances + +This file contains common instances of (FPerm 饾敻)-sets and nominal sets. +-/ + +variable (饾敻 : Type) + +/-! +## Atoms + +The set 饾敻 of atoms itself is a nominal set, where supp a = {a}. +-/ +section Atoms + +private lemma NominalSet.supp_atoms' {a : 饾敻} : PermSet.HasSupport 饾敻 a {a} := by + simp [PermSet.HasSupport, PermSet.fix, PermSet.fix'] + +instance : NominalSet 饾敻 饾敻 where + fin_supp := by + intro a + use {a} + constructor + 路 exact NominalSet.supp_atoms' 饾敻 + 路 simp + +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 + 路 simp; intro h; rw [h]; assumption + 路 intro S 鉄╤suppS, hfinS鉄 + by_contra ha + obtain 鉄╟, hc鉄 := Infinite.exists_notMem_finset ({a} 鈭 hfinS.toFinset) + simp at hc + have hfix : 飧╝, c飧 鈭 PermSet.fix 饾敻 S := by + intro d hd + rw [show 飧╝,c飧 鈥 d = (Equiv.swap a c) d from rfl] + apply Equiv.Perm.supp_notin + simp [Equiv.Perm.supp_swap, Ne.symm hc.left] + exact 鉄╪e_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right鉄 + have ha鈧 : 飧╝, c飧 鈥 a = c := by + simp [show 飧╝,c飧 鈥 a = (Equiv.swap a c) a from rfl] + have ha鈧 : 飧╝, c飧 鈥 a = a := by + specialize hsuppS hfix + simpa [PermSet.fix'] + rw [ha鈧乚 at ha鈧 + exact hc.left ha鈧 + +end Atoms + +/-! +## Discrete Nominal Sets + +Every set can be made into a discrete nominal set, where supp x = 鈭. +-/ +section Discrete + +def NominalSet.discrete (X : Type) : DiscreteNominalSet 饾敻 X where + smul 蟺 x := x + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl + is_discrete := by intro _ _; rfl + fin_supp := by + intro x + use {} + constructor + 路 intro 蟺 h蟺; simp [PermSet.fix']; rfl + 路 simp + +lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 饾敻 X] {x : X} : supp 饾敻 x = 鈭 := by + rw [鈫 Set.subset_empty_iff] + apply Set.sInter_subset_of_mem + constructor + 路 intro 蟺 h蟺 + simp [PermSet.fix'] + exact DiscreteNominalSet.is_discrete x 蟺 + 路 exact Set.finite_empty + +/-- We consider Unit a discrete nominal set. -/ +instance : DiscreteNominalSet 饾敻 Unit := NominalSet.discrete 饾敻 Unit + +/-- We consider Bool a discrete nominal set. -/ +instance : DiscreteNominalSet 饾敻 Bool := NominalSet.discrete 饾敻 Bool + +end Discrete diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 5f62ec0..6819c67 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -103,15 +103,14 @@ namespace Equiv.Perm /-- The support of a transposition (x y). -/ lemma supp_swap {x y : X} : (Equiv.swap x y).supp = if x 鈮 y then {x, y} else 鈭 := by - if h : (x 鈮 y) then - ext z + by_cases h : x = y + 路 simp [h, supp] + 路 simp [h]; ext z by_cases hx : z = x - 路 aesop + 路 simp [hx, Ne.symm h] 路 by_cases hy : z = y - 路 simp [hy] + 路 simp [hy, h] 路 simp [Equiv.swap_apply_of_ne_of_ne, hx, hy] - else - aesop end Equiv.Perm @@ -120,8 +119,7 @@ namespace FPerm def swap (x y : X) : FPerm X := 鉄‥quiv.swap x y, by apply Set.Finite.subset 路 apply ({x, y} : Finset X).finite_toSet - 路 simp [Equiv.Perm.supp_swap] - aesop鉄 + 路 by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]鉄 notation "飧" a "," b "飧" => FPerm.swap a b @@ -130,3 +128,29 @@ end FPerm example : FPerm 鈩 := 飧1, 2飧 * 飧3, 4飧 * 飧2, 3飧 end Transposition + +/-! +## (FPerm 饾敻)-Sets + +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 + +/-- The set of atoms itself forms a (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. -/ +instance : PermSet 饾敻 (FPerm 饾敻) where + smul 蟺 蟿 := 蟺 * 蟿 + one_smul := by intro; rfl + mul_smul := by intro _ _ _; rfl + +end PermSet diff --git a/Nominal/Basic.lean b/Nominal/Support.lean index 66f43b1..7875ad3 100644 --- a/Nominal/Basic.lean +++ b/Nominal/Support.lean @@ -1,53 +1,14 @@ import Mathlib.Tactic import Nominal.Permutations import Nominal.Helpers.Finset -/-! -# Basic Definitions - -This file provides basic definitions for nominal sets. --/ /-! -## (FPerm 饾敻)-Sets +# Support -Sets equipped with a permutation operation. +This file provides basic definitions for support of (FPerm 饾敻)-sets and nominal sets. -/ -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 - -/-- The set of atoms itself forms a (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. -/ -instance : PermSet 饾敻 (FPerm 饾敻) where - smul 蟺 蟿 := 蟺 * 蟿 - 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) : 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 : DiscretePermSet 饾敻 Unit := PermSet.discrete 饾敻 Unit - -/-- We consider Bool a discrete (FPerm 饾敻)-Set. -/ -instance : DiscretePermSet 饾敻 Bool := PermSet.discrete 饾敻 Bool - -end PermSet +variable (饾敻 : Type) /-! ## Support Definitions @@ -56,7 +17,7 @@ We can define the notion of "supports" on elements of (FPerm 饾敻)-Sets as the a -/ section Support -variable (饾敻 : Type) {X : Type} [PermSet 饾敻 X] +variable {X : Type} [PermSet 饾敻 X] namespace PermSet @@ -72,7 +33,7 @@ def fix (A : Set X) : Set (FPerm 饾敻) := def HasSupport (x : X) (S : Set 饾敻) : Prop := fix 饾敻 S 鈯 fix' 饾敻 x -@[simp] +/-- Alternative definition with fix 饾敻 S unfolded. -/ lemma support_iff {x : X} {S : Set 饾敻} : HasSupport 饾敻 x S 鈫 鈭 (蟺 : FPerm 饾敻), (鈭 x 鈭 S, 蟺 x = x) 鈫 蟺 鈭 fix' 饾敻 x := by constructor 路 intro hsupp 蟺 h蟺 @@ -80,7 +41,8 @@ lemma support_iff {x : X} {S : Set 饾敻} : HasSupport 饾敻 x S 鈫 鈭 (蟺 : FPe 路 intro hsupp 蟺 h蟺 exact hsupp 蟺 h蟺 -lemma support_subset {x : X} {S T : Set 饾敻} : HasSupport 饾敻 x S 鈫 S 鈯 T 鈫 HasSupport 饾敻 x T := by +/-- If a support is a subset of another set, that set is also a support. -/ +lemma support_superset {x : X} {S T : Set 饾敻} : HasSupport 饾敻 x S 鈫 S 鈯 T 鈫 HasSupport 饾敻 x T := by intro hS hsub 蟺 h蟺 apply hS intro a ha @@ -229,7 +191,7 @@ end PermSet end Support /-! -## Basic Nominal Set Definition +## Nominal Sets Nominal sets are then just (FPerm 饾敻)-Sets where all elements are finitely supported. -/ @@ -239,7 +201,11 @@ variable (饾敻 : Type) /-- 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 + fin_supp : 鈭 (x : X), 鈭 (S : Set 饾敻), PermSet.HasSupport 饾敻 x S 鈭 S.Finite + +/-- A discrete nominal set where permutations do not change anything. -/ +class DiscreteNominalSet (X : Type) extends NominalSet 饾敻 X where + is_discrete : 鈭 (x : X) (蟺 : FPerm 饾敻), 蟺 鈥 x = x namespace NominalSet @@ -252,14 +218,14 @@ def supp (x : X) : Set 饾敻 := /-- The least finite support in a nominal set is always finite. -/ lemma supp_finite {x : X} : (supp 饾敻 x).Finite := by unfold supp - obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.finsupp x + obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.fin_supp x apply Set.Finite.subset 路 exact hfinS 路 grind /-- The least finite support is itself a support. -/ lemma supp_is_support [Infinite 饾敻] {x : X} : PermSet.HasSupport 饾敻 x (supp 饾敻 x) := by - obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.finsupp x + obtain 鉄⊿, 鉄╤suppS, hfinS鉄┾煩 := nom.fin_supp x have suppf : (supp 饾敻 x = 鈰傗個 { T : Set 饾敻 | T 鈯 S 鈭 PermSet.HasSupport 饾敻 x T 鈭 T.Finite }) := by unfold supp; ext a constructor @@ -287,6 +253,7 @@ lemma supp_is_support [Infinite 饾敻] {x : X} : PermSet.HasSupport 饾敻 x (supp 路 intro T hT exact hT.right +/-- If S is a finite support for x, then supp x is a subset of it. -/ 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 @@ -294,70 +261,4 @@ lemma support_subset_supp {x : X} {S : Set 饾敻} : PermSet.HasSupport 饾敻 x S 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 - 路 exact NominalSet.supp_atoms' 饾敻 - 路 simp - -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 - 路 simp; intro h; rw [h]; assumption - 路 intro S 鉄╤suppS, hfinS鉄 - by_contra ha - obtain 鉄╟, hc鉄 := Infinite.exists_notMem_finset ({a} 鈭 hfinS.toFinset) - simp at hc - have hfix : 飧╝, c飧 鈭 PermSet.fix 饾敻 S := by - intro d hd - rw [show 飧╝,c飧 鈥 d = (Equiv.swap a c) d from rfl] - apply Equiv.Perm.supp_notin - simp [Equiv.Perm.supp_swap, Ne.symm hc.left] - exact 鉄╪e_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right鉄 - have ha鈧 : 飧╝, c飧 鈥 a = c := by - simp [show 飧╝,c飧 鈥 a = (Equiv.swap a c) a from rfl] - have ha鈧 : 飧╝, c飧 鈥 a = a := by - specialize hsuppS hfix - simpa [PermSet.fix'] - rw [ha鈧乚 at ha鈧 - exact hc.left ha鈧 - -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) : DiscreteNominalSet 饾敻 X := -{ PermSet.discrete 饾敻 X with - finsupp := by - intro x - use {} - constructor - 路 intro 蟺 h蟺; simp [PermSet.fix']; rfl - 路 simp -} - -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 鉄∟ominalSet.supp_discrete' 饾敻, Set.finite_empty鉄 - -/-- We consider Unit a discrete nominal set. -/ -instance : DiscreteNominalSet 饾敻 Unit := NominalSet.discrete 饾敻 Unit - -/-- We consider Bool a discrete nominal set. -/ -instance : DiscreteNominalSet 饾敻 Bool := NominalSet.discrete 饾敻 Bool - end NominalSet |