blob: eb10b44d6df60dfbb5b757ec4b7a57c07229a469 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
import Mathlib.Tactic
import Nominal.Permutations
/-!
# Basic Definitions
This file provides basic definitions for nominal sets.
-/
/-!
## (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 G-Set. -/
instance : PermSet ๐ธ ๐ธ where
smul ฯ a := ฯ a
one_smul := by aesop
mul_smul := by aesop
/-- The set of finite permutations forms a G-Set. -/
instance : PermSet ๐ธ (FPerm ๐ธ) where
smul ฯ ฯ := ฯ * ฯ
one_smul := by aesop
mul_smul := by aesop
/-- A discrete (FPerm ๐ธ)-Set where permutations do not change anything. -/
instance PermSet.discrete (X : Type) : PermSet ๐ธ X where
smul ฯ x := x
one_smul := by aesop
mul_smul := by aesop
/-- We consider Unit a discrete (FPerm ๐ธ)-Set. -/
instance : PermSet ๐ธ Unit := PermSet.discrete ๐ธ Unit
/-- We consider Bool a discrete (FPerm ๐ธ)-Set. -/
instance : PermSet ๐ธ Bool := PermSet.discrete ๐ธ Bool
end PermSet
/-!
## Support Definitions
We can define the notion of "supports" on elements of (FPerm ๐ธ)-Sets as the atoms which need to be left unchanged to also fix the element.
-/
section Support
variable (๐ธ : Type) {X : Type} [PermSet ๐ธ X]
namespace PermSet
/-- The permutations that leave an element x unchanged. -/
def fix' (x : X) : Set (FPerm ๐ธ) :=
{ ฯ : FPerm ๐ธ | ฯ โข x = x }
/-- The permutations that leave all elements in A unchanged. -/
def fix (A : Set X) : Set (FPerm ๐ธ) :=
{ ฯ : FPerm ๐ธ | โ x โ A, ฯ โข x = x }
/-- A set S โ ๐ธ is a support for x if every permutation that fixes S also leaves x unchanged. -/
def HasSupport (x : X) (S : Set ๐ธ) : Prop :=
fix ๐ธ S โ fix' ๐ธ x
@[simp]
lemma support_iff {x : X} {S : Set ๐ธ} : HasSupport ๐ธ x S โ fix ๐ธ S โ fix' ๐ธ x := by
rfl
lemma support_subset {x : X} {S T : Set ๐ธ} : HasSupport ๐ธ x S โ S โ T โ HasSupport ๐ธ x T := by
intro hS hsub ฯ hฯ
apply hS
intro a
aesop
lemma support_inter {x : X} {S T : Set ๐ธ} : HasSupport ๐ธ x S โ S.Finite โ HasSupport ๐ธ x T โ T.Finite โ HasSupport ๐ธ x (S โฉ T) := by
sorry
end PermSet
end Support
/-!
## Basic Nominal Set Definition
Nominal sets are then just G-Sets where all elements are finitely supported.
-/
section NominalSet
variable (๐ธ : Type)
/-- A G-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
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 ๐ธ :=
โโ { S : Set ๐ธ | PermSet.HasSupport ๐ธ x S }
/-- The least finite support in a nominal set is always finite. -/
lemma supp_finite {x : X} : (supp ๐ธ x).Finite := by
unfold supp
obtain โจS, โจhsuppS, hfinSโฉโฉ := nom.finsupp x
apply Set.Finite.subset
ยท exact hfinS
ยท grind
/-- The least finite support is itself a support. -/
lemma supp_is_support {x : X} : PermSet.HasSupport ๐ธ x (supp ๐ธ x) := sorry
end NominalSet
/-- 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
ยท simp
-- TODO: Prove supp a = {a}
/-- Every set can be made into a discrete nominal set where every element has empty support. -/
instance NominalSet.discrete (X : Type) : NominalSet ๐ธ X where
finsupp := by
intro x
use {}
constructor
ยท intro ฯ hฯ
aesop
ยท simp
-- TODO: Prove supp x = โ
/-- We consider Unit a discrete nominal set. -/
instance : NominalSet ๐ธ Unit := NominalSet.discrete ๐ธ Unit
/-- We consider Bool a discrete nominal set. -/
instance : NominalSet ๐ธ Bool := NominalSet.discrete ๐ธ Bool
end NominalSet
|
