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
|
import Mathlib.Tactic
/-!
# 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
/-- 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
notation "⸨" a "," b "⸩" => Equiv.swap a b
variable {X : Type} [DecidableEq X]
namespace Equiv.Perm
/-- The support of a transposition (x y). -/
lemma supp_swap{x y : X} : ⸨x, y⸩.supp = if x ≠ y then {x, y} else ∅ := by
if h : (x ≠ y) then
ext z
by_cases hx : z = x
· aesop
· by_cases hy : z = y
· simp [hy]
· simp [Equiv.swap_apply_of_ne_of_ne, hx, hy]
else
aesop
end Equiv.Perm
namespace FPerm
lemma mem_swap {x y : X} : ⸨x, y⸩ ∈ FPerm X := by
apply Set.Finite.subset
· apply ({x, y} : Finset X).finite_toSet
· simp [Equiv.Perm.supp_swap]
aesop
end FPerm
example : FPerm ℕ := ⟨⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩, by simp [FPerm.mem_swap, FPerm.mem_mul]⟩
end Transposition
|
