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
|
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]
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_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 [supp]
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
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
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
|
