-
Notifications
You must be signed in to change notification settings - Fork 251
/
FixingSubgroup.lean
183 lines (137 loc) · 7.58 KB
/
FixingSubgroup.lean
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
/-
Copyright (c) 2022 Antoine Chambert-Loir. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Chambert-Loir
-/
import Mathlib.Algebra.Group.Subgroup.Actions
import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.GroupTheory.GroupAction.FixedPoints
#align_import group_theory.group_action.fixing_subgroup from "leanprover-community/mathlib"@"f93c11933efbc3c2f0299e47b8ff83e9b539cbf6"
/-!
# Fixing submonoid, fixing subgroup of an action
In the presence of an action of a monoid or a group,
this file defines the fixing submonoid or the fixing subgroup,
and relates it to the set of fixed points via a Galois connection.
## Main definitions
* `fixingSubmonoid M s` : in the presence of `MulAction M α` (with `Monoid M`)
it is the `Submonoid M` consisting of elements which fix `s : Set α` pointwise.
* `fixingSubmonoid_fixedPoints_gc M α` is the `GaloisConnection`
that relates `fixingSubmonoid` with `fixedPoints`.
* `fixingSubgroup M s` : in the presence of `MulAction M α` (with `Group M`)
it is the `Subgroup M` consisting of elements which fix `s : Set α` pointwise.
* `fixingSubgroup_fixedPoints_gc M α` is the `GaloisConnection`
that relates `fixingSubgroup` with `fixedPoints`.
TODO :
* Maybe other lemmas are useful
* Treat semigroups ?
* add `to_additive` for the various lemmas
-/
section Monoid
open MulAction
variable (M : Type*) {α : Type*} [Monoid M] [MulAction M α]
/-- The submonoid fixing a set under a `MulAction`. -/
@[to_additive " The additive submonoid fixing a set under an `AddAction`. "]
def fixingSubmonoid (s : Set α) : Submonoid M where
carrier := { ϕ : M | ∀ x : s, ϕ • (x : α) = x }
one_mem' _ := one_smul _ _
mul_mem' {x y} hx hy z := by rw [mul_smul, hy z, hx z]
#align fixing_submonoid fixingSubmonoid
#align fixing_add_submonoid fixingAddSubmonoid
theorem mem_fixingSubmonoid_iff {s : Set α} {m : M} :
m ∈ fixingSubmonoid M s ↔ ∀ y ∈ s, m • y = y :=
⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩
#align mem_fixing_submonoid_iff mem_fixingSubmonoid_iff
variable (α)
/-- The Galois connection between fixing submonoids and fixed points of a monoid action -/
theorem fixingSubmonoid_fixedPoints_gc :
GaloisConnection (OrderDual.toDual ∘ fixingSubmonoid M)
((fun P : Submonoid M => fixedPoints P α) ∘ OrderDual.ofDual) :=
fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩
#align fixing_submonoid_fixed_points_gc fixingSubmonoid_fixedPoints_gc
theorem fixingSubmonoid_antitone : Antitone fun s : Set α => fixingSubmonoid M s :=
(fixingSubmonoid_fixedPoints_gc M α).monotone_l
#align fixing_submonoid_antitone fixingSubmonoid_antitone
theorem fixedPoints_antitone : Antitone fun P : Submonoid M => fixedPoints P α :=
(fixingSubmonoid_fixedPoints_gc M α).monotone_u.dual_left
#align fixed_points_antitone fixedPoints_antitone
/-- Fixing submonoid of union is intersection -/
theorem fixingSubmonoid_union {s t : Set α} :
fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t :=
(fixingSubmonoid_fixedPoints_gc M α).l_sup
#align fixing_submonoid_union fixingSubmonoid_union
/-- Fixing submonoid of iUnion is intersection -/
theorem fixingSubmonoid_iUnion {ι : Sort*} {s : ι → Set α} :
fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i) :=
(fixingSubmonoid_fixedPoints_gc M α).l_iSup
#align fixing_submonoid_Union fixingSubmonoid_iUnion
/-- Fixed points of sup of submonoids is intersection -/
theorem fixedPoints_submonoid_sup {P Q : Submonoid M} :
fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
(fixingSubmonoid_fixedPoints_gc M α).u_inf
#align fixed_points_submonoid_sup fixedPoints_submonoid_sup
/-- Fixed points of iSup of submonoids is intersection -/
theorem fixedPoints_submonoid_iSup {ι : Sort*} {P : ι → Submonoid M} :
fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α :=
(fixingSubmonoid_fixedPoints_gc M α).u_iInf
#align fixed_points_submonoid_supr fixedPoints_submonoid_iSup
end Monoid
section Group
open MulAction
variable (M : Type*) {α : Type*} [Group M] [MulAction M α]
/-- The subgroup fixing a set under a `MulAction`. -/
@[to_additive " The additive subgroup fixing a set under an `AddAction`. "]
def fixingSubgroup (s : Set α) : Subgroup M :=
{ fixingSubmonoid M s with inv_mem' := fun hx z => by rw [inv_smul_eq_iff, hx z] }
#align fixing_subgroup fixingSubgroup
#align fixing_add_subgroup fixingAddSubgroup
theorem mem_fixingSubgroup_iff {s : Set α} {m : M} : m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y :=
⟨fun hg y hy => hg ⟨y, hy⟩, fun h ⟨y, hy⟩ => h y hy⟩
#align mem_fixing_subgroup_iff mem_fixingSubgroup_iff
theorem mem_fixingSubgroup_iff_subset_fixedBy {s : Set α} {m : M} :
m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m := by
simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]
theorem mem_fixingSubgroup_compl_iff_movedBy_subset {s : Set α} {m : M} :
m ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s := by
rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]
variable (α)
/-- The Galois connection between fixing subgroups and fixed points of a group action -/
theorem fixingSubgroup_fixedPoints_gc :
GaloisConnection (OrderDual.toDual ∘ fixingSubgroup M)
((fun P : Subgroup M => fixedPoints P α) ∘ OrderDual.ofDual) :=
fun _s _P => ⟨fun h s hs p => h p.2 ⟨s, hs⟩, fun h p hp s => h s.2 ⟨p, hp⟩⟩
#align fixing_subgroup_fixed_points_gc fixingSubgroup_fixedPoints_gc
theorem fixingSubgroup_antitone : Antitone (fixingSubgroup M : Set α → Subgroup M) :=
(fixingSubgroup_fixedPoints_gc M α).monotone_l
#align fixing_subgroup_antitone fixingSubgroup_antitone
theorem fixedPoints_subgroup_antitone : Antitone fun P : Subgroup M => fixedPoints P α :=
(fixingSubgroup_fixedPoints_gc M α).monotone_u.dual_left
#align fixed_points_subgroup_antitone fixedPoints_subgroup_antitone
/-- Fixing subgroup of union is intersection -/
theorem fixingSubgroup_union {s t : Set α} :
fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t :=
(fixingSubgroup_fixedPoints_gc M α).l_sup
#align fixing_subgroup_union fixingSubgroup_union
/-- Fixing subgroup of iUnion is intersection -/
theorem fixingSubgroup_iUnion {ι : Sort*} {s : ι → Set α} :
fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i) :=
(fixingSubgroup_fixedPoints_gc M α).l_iSup
#align fixing_subgroup_Union fixingSubgroup_iUnion
/-- Fixed points of sup of subgroups is intersection -/
theorem fixedPoints_subgroup_sup {P Q : Subgroup M} :
fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
(fixingSubgroup_fixedPoints_gc M α).u_inf
#align fixed_points_subgroup_sup fixedPoints_subgroup_sup
/-- Fixed points of iSup of subgroups is intersection -/
theorem fixedPoints_subgroup_iSup {ι : Sort*} {P : ι → Subgroup M} :
fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α :=
(fixingSubgroup_fixedPoints_gc M α).u_iInf
#align fixed_points_subgroup_supr fixedPoints_subgroup_iSup
/-- The orbit of the fixing subgroup of `sᶜ` (ie. the moving subgroup of `s`) is a subset of `s` -/
theorem orbit_fixingSubgroup_compl_subset {s : Set α} {a : α} (a_in_s : a ∈ s) :
MulAction.orbit (fixingSubgroup M sᶜ) a ⊆ s := by
intro b b_in_orbit
let ⟨⟨g, g_fixing⟩, g_eq⟩ := MulAction.mem_orbit_iff.mp b_in_orbit
rw [Submonoid.mk_smul] at g_eq
rw [mem_fixingSubgroup_compl_iff_movedBy_subset] at g_fixing
rwa [← g_eq, smul_mem_of_set_mem_fixedBy (set_mem_fixedBy_of_movedBy_subset g_fixing)]
end Group