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
152
153
154
155
|
import Mathlib.Tactic
section Permutations
variable {X : Type}
notation "⸨" a "," b "⸩" => Equiv.swap a b
-- The support of a permutation; i.e., the set of elements where the permutation actually maps the element to a different one.
def Equiv.Perm.supp (π : Equiv.Perm X) : Set X :=
{x | π x ≠ x}
@[simp]
theorem mem_support (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by
simp [Equiv.Perm.supp]
-- The support of the identity function is the empty set.
lemma supp_one : (1 : Equiv.Perm X).supp = ∅ := by
rw [Set.eq_empty_iff_forall_notMem]
intro x hx
contradiction
-- The support of the inverse function is the same as the function's support.
lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by
simp [Equiv.Perm.supp, Equiv.Perm.set_support_inv_eq]
-- The support of two concatenated permutations is a subset of the individual supports as a union.
lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by
simp [Equiv.Perm.supp]
apply Equiv.Perm.set_support_mul_subset
lemma supp_swap [DecidableEq X] {x y : X} (h : x ≠ y) : ⸨x, y⸩.supp = {x, y} := by
ext z
by_cases hx : z = x
· simpa [hx] using h.symm
· by_cases hy : z = y
· simpa [Equiv.swap_apply_of_ne_of_ne, hx, hy] using h
· simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
-- The group of (finitely supported) permutations.
def FPerm (X: Type) : Subgroup (Equiv.Perm X) where
carrier := {π | π.supp.Finite}
mul_mem' {π τ} hπ hτ := by
apply (hπ.union hτ).subset
exact supp_mul_subset π τ
one_mem' := by
simp [supp_one]
inv_mem' {x} hx := by
simp [supp_inv]
exact hx
lemma supp_swap_finite [DecidableEq X] (x y : X) : ⸨x, y⸩ ∈ FPerm X := by
by_cases hx : x = y
· rw [<-Equiv.swap_eq_one_iff] at hx
simp [hx]
· simp [FPerm, supp_swap hx]
lemma supp_mul_finite {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
(FPerm X).mul_mem hπ hτ
lemma supp_inv_finite {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
(FPerm X).inv_mem hπ
-- Since FPerm is a subgroup of Perm, it is also a group.
instance (X : Type) : Group (FPerm X) :=
Subgroup.toGroup (FPerm X)
-- Since FPerm is a subset of Perm, we can coerce it into a function.
instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
coe π := (↑π : Equiv.Perm X)
example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [supp_swap_finite, supp_mul_finite]⟩
end Permutations
section GSets
variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
-- A G-set is a set X equipped with a group action •: (FPerm 𝔸) × X → X.
class GSet (X : Type) extends MulAction (FPerm 𝔸) X
instance : GSet 𝔸 𝔸 where
smul π a := π a
one_smul := by aesop
mul_smul := by aesop
instance discreteGSet (X : Type) : GSet 𝔸 X where
smul π x := x
one_smul := by aesop
mul_smul := by aesop
instance : GSet 𝔸 Unit := discreteGSet 𝔸 Unit
instance : GSet 𝔸 Bool := discreteGSet 𝔸 Bool
variable {X : Type} [GSet 𝔸 X]
-- 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
end GSets
section NominalSets
variable (𝔸 : Type)
-- A G-Set X is nominal if every x ∈ X is finitely supported.
class Nominal (X : Type) extends GSet 𝔸 X where
finsupp : ∀ (x : X), ∃ (S : Set 𝔸), HasSupport 𝔸 x S ∧ S.Finite
instance : Nominal 𝔸 𝔸 where
finsupp := by
intro a
use {a}
constructor
· intro π hπ
aesop
· simp
instance discreteNominal (X : Type) : Nominal 𝔸 X where
finsupp := by
intro x
use {}
constructor
· intro π hπ
aesop
· simp
instance : Nominal 𝔸 Unit := discreteNominal 𝔸 Unit
instance : Nominal 𝔸 Bool := discreteNominal 𝔸 Bool
variable {X : Type} [nom : Nominal 𝔸 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 𝔸 | HasSupport 𝔸 x S }
-- The least finite support in a nominal set is always finite.
theorem supp_finite (x : X) : (supp 𝔸 x).Finite := by
unfold supp
obtain ⟨S, ⟨hsuppS, hfinS⟩⟩ := nom.finsupp x
apply Set.Finite.subset
· exact hfinS
· grind
end NominalSets
|
