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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
|
import Mathlib
/-!
# Finitely supported permutations
This file defines `FPerm`, the subgroup of permutations with finite support.
It also provides basic lemmas about permutation supports and transpositions.
-/
/-!
## Support Definition
Support is defined on Equiv.Perm which also includes infinitely supported permutations.
-/
section Support
variable {X : Type}
namespace Equiv.Perm
/--
The support of a permutation; i.e., the set of elements the permutation actually changes.
Note that, while there is an Equiv.Perm.support, it only works for finite types and thus finite supports.
-/
def supp (π : Equiv.Perm X) : Set X :=
{x | π x ≠ x}
@[simp]
theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := by rfl
/-- If an element does not occur in the support, the permutation doesn't move it. -/
lemma supp_notin {π : Equiv.Perm X} {x : X} : x ∉ π.supp → π x = x := by
rw [show (π x = x) ↔ ¬(π x ≠ x) by simp only [ne_eq, not_not]]
simp [← (mem_supp π x).not]
/-- 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 [supp, set_support_symm_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 only [supp, coe_mul, Function.comp_apply, ne_eq]
apply set_support_mul_subset
end Equiv.Perm
end Support
/-!
## FPerm Group
The FPerm group is the subgroup of finitely supported permutations.
-/
section Subgroup
/-- 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 Equiv.Perm.supp_mul_subset π τ
one_mem' := by
simp [Equiv.Perm.supp_one]
inv_mem' {x} hx := by
simp [Equiv.Perm.supp_inv]
exact hx
variable {X : Type}
namespace FPerm
lemma mem_mul {π τ : Equiv.Perm X} (hπ : π ∈ FPerm X) (hτ : τ ∈ FPerm X) : (π * τ) ∈ FPerm X :=
(FPerm X).mul_mem hπ hτ
lemma mem_inv {π : Equiv.Perm X} (hπ : π ∈ FPerm X) : π⁻¹ ∈ FPerm X :=
(FPerm X).inv_mem hπ
end FPerm
/-- Since FPerm is a subset of Equiv.Perm, we can coerce it into a function. -/
instance (X : Type) : CoeFun (FPerm X) (fun _ => X → X) where
coe π := (↑π : Equiv.Perm X)
end Subgroup
/-!
## Transpositions
Transpositions are a special case of finite permutations, where only (at most) two elements are swapped.
-/
section Transposition
variable {X : Type} [DecidableEq X]
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
by_cases h : x = y
· simp [h, supp]
· simp [h]; ext z
by_cases hx : z = x
· simp [hx, Ne.symm h]
· by_cases hy : z = y
· simp [hy, h]
· simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
end Equiv.Perm
namespace FPerm
/-- Extensionality lemma for finite permutations. -/
lemma ext {X : Type} {π₁ π₂ : FPerm X} : π₁.val = π₂.val → π₁ = π₂ := by
intro h; ext; rw [h]
/-- Transpositions are finite permutations. -/
def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
apply Set.Finite.subset
· apply ({x, y} : Finset X).finite_toSet
· by_cases h : x = y <;> all_goals simp [Equiv.Perm.supp_swap, h]⟩
notation "⸨" a "," b "⸩" => FPerm.swap a b
/-- Lifting of Equiv.mul_swap_eq_swap_mul to finite permutations. -/
lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, π b⸩ * π := by
apply ext
apply Equiv.mul_swap_eq_swap_mul
/-- Lifting of Equiv.swap_mul_self to finite permutations. -/
lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by
apply ext
simp [swap]
/-- Lifting of Equiv.swap_self to finite permutations.-/
lemma swap_self {a : X} : ⸨a, a⸩ = 1 := by
ext
simp [swap]
/-- Lifting of Equiv.swap_comm to finite permutations. -/
lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by
apply ext
simp [swap, Equiv.swap_comm]
/-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/
lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by
intro ha hb
simp [swap, Equiv.swap_apply_of_ne_of_ne, ha, hb]
/-- Lifting of Equiv.swap_apply_left to finite permutations. -/
@[simp]
lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by
simp [swap]
/-- Lifting of Equiv.swap_apply_right to finite permutations. -/
@[simp]
lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by
simp [swap]
/-- Lifting of Equiv.swap_inv to finite permutations. -/
@[simp]
lemma swap_inv (a b : X) : ⸨a, b⸩⁻¹ = ⸨a, b⸩ := by
apply ext
simp [swap]
end FPerm
example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩
end Transposition
/-!
## (FPerm 𝔸)-Sets
Sets equipped with a permutation operation.
-/
section PermSet
/-- A set X equipped with a group action •: (FPerm 𝔸) × X → X. -/
class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) extends MulAction (FPerm 𝔸) X
variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
/-- An (FPerm 𝔸)-set is orbit-finite if there are only finitely many different orbits. -/
class OrbitFinite (X : Type) [PermSet 𝔸 X] where
fin_orbits : Finite (Quotient (MulAction.orbitRel (FPerm 𝔸) X))
/-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 𝔸 where
smul π a := π a
one_smul := by intro; rfl
mul_smul := by intro _ _ _; rfl
instance : OrbitFinite 𝔸 𝔸 where
fin_orbits := Finite.of_equiv Unit
{ toFun _ := Quotient.mk _ (inferInstance : Nonempty 𝔸).some
invFun _ := ()
right_inv := by
let chosen := (inferInstance : Nonempty 𝔸).some
apply Quotient.ind; intro a
rw [Quotient.eq]
show chosen ∈ MulAction.orbit (FPerm 𝔸) a
use ⸨chosen, a⸩
exact FPerm.swap_apply_right chosen a
}
/-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/
instance : PermSet 𝔸 (FPerm 𝔸) where
smul π τ := π * τ
one_smul := by intro; rfl
mul_smul := by intro _ _ _; rfl
open Pointwise
/-- The powerset of an (FPerm 𝔸)-Set forms an (FPerm 𝔸)-Set using pointwise permutation. -/
instance {X : Type} [PermSet 𝔸 X] : PermSet 𝔸 (Set X) where
/-- Simplification for swaps applied to an atom. -/
@[simp] lemma PermSet.atom_swap {a b c : 𝔸} : ⸨a, b⸩ • c = (Equiv.swap a b) c := by rfl
/-- Given x = (a b) y, we also know y = (a b) x. -/
lemma PermSet.swap_switch {X : Type} [PermSet 𝔸 X] {a b : 𝔸} {x y : X} : x = ⸨a, b⸩ • y → y = ⸨a, b⸩ • x := by
intro h
have h' : ⸨a, b⸩ • x = ⸨a, b⸩ • ⸨a, b⸩ • y := by congr
rw [← mul_smul, FPerm.swap_mul_self, one_smul] at h'
exact h'.symm
/-- If the element is not affected by the swap, membership of it is the same as before the swap. -/
lemma PermSet.atom_set_swap_ne_ne {a b c : 𝔸} {S : Set 𝔸} : c ≠ a → c ≠ b → (c ∈ S ↔ c ∈ ⸨a, b⸩ • S) := by
intro ha hb
constructor
· intro h
rw [← FPerm.swap_apply_of_ne_of_ne ha hb]
exact Set.smul_mem_smul_set h
· intro h
have h' : ⸨a, b⸩ c ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
rw [FPerm.swap_apply_of_ne_of_ne ha hb, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
exact h'
/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
lemma PermSet.atom_set_swap_left {a b : 𝔸} {S : Set 𝔸} : a ∈ S ↔ b ∈ ⸨a, b⸩ • S := by
constructor
· intro h
have h' : ⸨a, b⸩ a ∈ ⸨a, b⸩ • S := Set.smul_mem_smul_set h
rw [FPerm.swap_apply_left] at h'
exact h'
· intro h
have h' : ⸨a, b⸩ b ∈ ⸨a, b⸩ • ⸨a, b⸩ • S := Set.smul_mem_smul_set h
rw [FPerm.swap_apply_right, ← mul_smul, FPerm.swap_mul_self, one_smul] at h'
exact h'
/-- If an element is swapped, its membership is exactly that of the other element in the swapped set. -/
lemma PermSet.atom_set_swap_right {a b : 𝔸} {S : Set 𝔸} : b ∈ S ↔ a ∈ ⸨a, b⸩ • S := by
rw [FPerm.swap_comm, atom_set_swap_left]
end PermSet
|
