Skip to content

Commit 5eae12e

Browse files
YaelDilliesYaelDillies
committed
chore: Move group lemmas out of GroupTheory.GroupAction.Group (#14705)
The rest of the file is now purely about `GroupWithZero` and alike, and will be moved under `Algebra.GroupWithZero.Action` in a future PR.
1 parent 126510d commit 5eae12e

File tree

5 files changed

+185
-161
lines changed

5 files changed

+185
-161
lines changed

‎Mathlib.lean

+1
Original file line numberDiff line numberDiff line change
@@ -208,6 +208,7 @@ import Mathlib.Algebra.GCDMonoid.Nat
208208
import Mathlib.Algebra.GeomSum
209209
import Mathlib.Algebra.GradedMonoid
210210
import Mathlib.Algebra.GradedMulAction
211+
import Mathlib.Algebra.Group.Action.Basic
211212
import Mathlib.Algebra.Group.Action.Defs
212213
import Mathlib.Algebra.Group.Action.Opposite
213214
import Mathlib.Algebra.Group.Action.Option

‎Mathlib/Algebra/Group/Action/Basic.lean

+181
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
/-
2+
Copyright (c) 2018 Chris Hughes. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Hughes
5+
-/
6+
import Mathlib.Algebra.Group.Action.Units
7+
import Mathlib.Algebra.Group.Invertible.Basic
8+
import Mathlib.GroupTheory.Perm.Basic
9+
10+
#align_import group_theory.group_action.group from "leanprover-community/mathlib"@"3b52265189f3fb43aa631edffce5d060fafaf82f"
11+
12+
/-!
13+
# More lemmas about group actions
14+
15+
This file contains lemmas about group actions that require more imports than
16+
`Algebra.Group.Action.Defs` offers.
17+
-/
18+
19+
assert_not_exists MonoidWithZero
20+
21+
variable {α β γ : Type*}
22+
23+
section MulAction
24+
25+
section Group
26+
27+
variable [Group α] [MulAction α β]
28+
29+
/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`. -/
30+
@[to_additive (attr := simps)]
31+
def MulAction.toPerm (a : α) : Equiv.Perm β :=
32+
⟨fun x => a • x, fun x => a⁻¹ • x, inv_smul_smul a, smul_inv_smul a⟩
33+
#align mul_action.to_perm MulAction.toPerm
34+
#align add_action.to_perm AddAction.toPerm
35+
#align add_action.to_perm_apply AddAction.toPerm_apply
36+
#align mul_action.to_perm_apply MulAction.toPerm_apply
37+
#align add_action.to_perm_symm_apply AddAction.toPerm_symm_apply
38+
#align mul_action.to_perm_symm_apply MulAction.toPerm_symm_apply
39+
40+
/-- Given an action of an additive group `α` on `β`, each `g : α` defines a permutation of `β`. -/
41+
add_decl_doc AddAction.toPerm
42+
43+
/-- `MulAction.toPerm` is injective on faithful actions. -/
44+
@[to_additive "`AddAction.toPerm` is injective on faithful actions."]
45+
lemma MulAction.toPerm_injective [FaithfulSMul α β] :
46+
Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
47+
(show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp
48+
#align mul_action.to_perm_injective MulAction.toPerm_injective
49+
#align add_action.to_perm_injective AddAction.toPerm_injective
50+
51+
variable (α) (β)
52+
53+
/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
54+
@[simps]
55+
def MulAction.toPermHom : α →* Equiv.Perm β where
56+
toFun := MulAction.toPerm
57+
map_one' := Equiv.ext <| one_smul α
58+
map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
59+
#align mul_action.to_perm_hom MulAction.toPermHom
60+
#align mul_action.to_perm_hom_apply MulAction.toPermHom_apply
61+
62+
/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
63+
`β`. -/
64+
@[simps!]
65+
def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
66+
α →+ Additive (Equiv.Perm β) :=
67+
MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
68+
#align add_action.to_perm_hom AddAction.toPermHom
69+
70+
/-- The tautological action by `Equiv.Perm α` on `α`.
71+
72+
This generalizes `Function.End.applyMulAction`. -/
73+
instance Equiv.Perm.applyMulAction (α : Type*) : MulAction (Equiv.Perm α) α where
74+
smul f a := f a
75+
one_smul _ := rfl
76+
mul_smul _ _ _ := rfl
77+
#align equiv.perm.apply_mul_action Equiv.Perm.applyMulAction
78+
79+
@[simp]
80+
protected lemma Equiv.Perm.smul_def {α : Type*} (f : Equiv.Perm α) (a : α) : f • a = f a :=
81+
rfl
82+
#align equiv.perm.smul_def Equiv.Perm.smul_def
83+
84+
/-- `Equiv.Perm.applyMulAction` is faithful. -/
85+
instance Equiv.Perm.applyFaithfulSMul (α : Type*) : FaithfulSMul (Equiv.Perm α) α :=
86+
⟨Equiv.ext⟩
87+
#align equiv.perm.apply_has_faithful_smul Equiv.Perm.applyFaithfulSMul
88+
89+
variable {α} {β}
90+
91+
@[to_additive]
92+
protected lemma MulAction.bijective (g : α) : Function.Bijective (g • · : β → β) :=
93+
(MulAction.toPerm g).bijective
94+
#align mul_action.bijective MulAction.bijective
95+
#align add_action.bijective AddAction.bijective
96+
97+
@[to_additive]
98+
protected lemma MulAction.injective (g : α) : Function.Injective (g • · : β → β) :=
99+
(MulAction.bijective g).injective
100+
#align mul_action.injective MulAction.injective
101+
#align add_action.injective AddAction.injective
102+
103+
@[to_additive]
104+
protected lemma MulAction.surjective (g : α) : Function.Surjective (g • · : β → β) :=
105+
(MulAction.bijective g).surjective
106+
#align mul_action.surjective MulAction.surjective
107+
#align add_action.surjective AddAction.surjective
108+
109+
@[to_additive]
110+
lemma smul_left_cancel (g : α) {x y : β} (h : g • x = g • y) : x = y := MulAction.injective g h
111+
#align smul_left_cancel smul_left_cancel
112+
#align vadd_left_cancel vadd_left_cancel
113+
114+
@[to_additive (attr := simp)]
115+
lemma smul_left_cancel_iff (g : α) {x y : β} : g • x = g • y ↔ x = y :=
116+
(MulAction.injective g).eq_iff
117+
#align smul_left_cancel_iff smul_left_cancel_iff
118+
#align vadd_left_cancel_iff vadd_left_cancel_iff
119+
120+
@[to_additive]
121+
lemma smul_eq_iff_eq_inv_smul (g : α) {x y : β} : g • x = y ↔ x = g⁻¹ • y :=
122+
(MulAction.toPerm g).apply_eq_iff_eq_symm_apply
123+
#align smul_eq_iff_eq_inv_smul smul_eq_iff_eq_inv_smul
124+
#align vadd_eq_iff_eq_neg_vadd vadd_eq_iff_eq_neg_vadd
125+
126+
end Group
127+
128+
section Monoid
129+
variable [Monoid α] [MulAction α β] (c : α) (x y : β) [Invertible c]
130+
131+
@[simp] lemma invOf_smul_smul : ⅟c • c • x = x := inv_smul_smul (unitOfInvertible c) _
132+
@[simp] lemma smul_invOf_smul : c • (⅟ c • x) = x := smul_inv_smul (unitOfInvertible c) _
133+
134+
variable {c x y}
135+
136+
lemma invOf_smul_eq_iff : ⅟c • x = y ↔ x = c • y := inv_smul_eq_iff (g := unitOfInvertible c)
137+
138+
lemma smul_eq_iff_eq_invOf_smul : c • x = y ↔ x = ⅟c • y :=
139+
smul_eq_iff_eq_inv_smul (g := unitOfInvertible c)
140+
141+
end Monoid
142+
end MulAction
143+
144+
section Arrow
145+
146+
/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
147+
@[to_additive (attr := simps) arrowAddAction
148+
"If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)`"]
149+
def arrowAction {G A B : Type*} [DivisionMonoid G] [MulAction G A] : MulAction G (A → B) where
150+
smul g F a := F (g⁻¹ • a)
151+
one_smul f := by
152+
show (fun x => f ((1 : G)⁻¹ • x)) = f
153+
simp only [inv_one, one_smul]
154+
mul_smul x y f := by
155+
show (fun a => f ((x*y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
156+
simp only [mul_smul, mul_inv_rev]
157+
#align arrow_action arrowAction
158+
#align arrow_add_action arrowAddAction
159+
160+
end Arrow
161+
162+
namespace IsUnit
163+
variable [Monoid α] [MulAction α β]
164+
165+
@[to_additive]
166+
lemma smul_left_cancel {a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y :=
167+
let ⟨u, hu⟩ := ha
168+
hu ▸ smul_left_cancel_iff u
169+
#align is_unit.smul_left_cancel IsUnit.smul_left_cancel
170+
#align is_add_unit.vadd_left_cancel IsAddUnit.vadd_left_cancel
171+
172+
end IsUnit
173+
174+
section SMul
175+
variable [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β]
176+
177+
@[simp] lemma isUnit_smul_iff (g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m :=
178+
⟨fun h => inv_smul_smul g m ▸ h.smul g⁻¹, IsUnit.smul g⟩
179+
#align is_unit_smul_iff isUnit_smul_iff
180+
181+
end SMul

‎Mathlib/GroupTheory/GroupAction/Embedding.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Eric Wieser
55
-/
6+
import Mathlib.Algebra.Group.Action.Basic
67
import Mathlib.Algebra.Group.Action.Pi
7-
import Mathlib.GroupTheory.GroupAction.Group
88

99
#align_import group_theory.group_action.embedding from "leanprover-community/mathlib"@"a437a2499163d85d670479f69f625f461cc5fef9"
1010

‎Mathlib/GroupTheory/GroupAction/Group.lean

+1-159
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Hughes
55
-/
66
import Mathlib.Algebra.Group.Aut
7+
import Mathlib.Algebra.Group.Action.Basic
78
import Mathlib.Algebra.Group.Invertible.Basic
89
import Mathlib.Algebra.GroupWithZero.Units.Basic
910
import Mathlib.GroupTheory.GroupAction.Units
@@ -22,130 +23,6 @@ universe u v w
2223
variable {α : Type u} {β : Type v} {γ : Type w}
2324

2425
section MulAction
25-
section Group
26-
27-
variable [Group α] [MulAction α β]
28-
29-
/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`. -/
30-
@[to_additive (attr := simps)]
31-
def MulAction.toPerm (a : α) : Equiv.Perm β :=
32-
⟨fun x => a • x, fun x => a⁻¹ • x, inv_smul_smul a, smul_inv_smul a⟩
33-
#align mul_action.to_perm MulAction.toPerm
34-
#align add_action.to_perm AddAction.toPerm
35-
#align add_action.to_perm_apply AddAction.toPerm_apply
36-
#align mul_action.to_perm_apply MulAction.toPerm_apply
37-
#align add_action.to_perm_symm_apply AddAction.toPerm_symm_apply
38-
#align mul_action.to_perm_symm_apply MulAction.toPerm_symm_apply
39-
40-
/-- Given an action of an additive group `α` on `β`, each `g : α` defines a permutation of `β`. -/
41-
add_decl_doc AddAction.toPerm
42-
43-
/-- `MulAction.toPerm` is injective on faithful actions. -/
44-
@[to_additive "`AddAction.toPerm` is injective on faithful actions."]
45-
theorem MulAction.toPerm_injective [FaithfulSMul α β] :
46-
Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
47-
(show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp
48-
#align mul_action.to_perm_injective MulAction.toPerm_injective
49-
#align add_action.to_perm_injective AddAction.toPerm_injective
50-
51-
variable (α) (β)
52-
53-
/-- Given an action of a group `α` on a set `β`, each `g : α` defines a permutation of `β`. -/
54-
@[simps]
55-
def MulAction.toPermHom : α →* Equiv.Perm β where
56-
toFun := MulAction.toPerm
57-
map_one' := Equiv.ext <| one_smul α
58-
map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : α) u₂
59-
#align mul_action.to_perm_hom MulAction.toPermHom
60-
#align mul_action.to_perm_hom_apply MulAction.toPermHom_apply
61-
62-
/-- Given an action of an additive group `α` on a set `β`, each `g : α` defines a permutation of
63-
`β`. -/
64-
@[simps!]
65-
def AddAction.toPermHom (α : Type*) [AddGroup α] [AddAction α β] :
66-
α →+ Additive (Equiv.Perm β) :=
67-
MonoidHom.toAdditive'' <| MulAction.toPermHom (Multiplicative α) β
68-
#align add_action.to_perm_hom AddAction.toPermHom
69-
70-
/-- The tautological action by `Equiv.Perm α` on `α`.
71-
72-
This generalizes `Function.End.applyMulAction`. -/
73-
instance Equiv.Perm.applyMulAction (α : Type*) : MulAction (Equiv.Perm α) α where
74-
smul f a := f a
75-
one_smul _ := rfl
76-
mul_smul _ _ _ := rfl
77-
#align equiv.perm.apply_mul_action Equiv.Perm.applyMulAction
78-
79-
@[simp]
80-
protected theorem Equiv.Perm.smul_def {α : Type*} (f : Equiv.Perm α) (a : α) : f • a = f a :=
81-
rfl
82-
#align equiv.perm.smul_def Equiv.Perm.smul_def
83-
84-
/-- `Equiv.Perm.applyMulAction` is faithful. -/
85-
instance Equiv.Perm.applyFaithfulSMul (α : Type*) : FaithfulSMul (Equiv.Perm α) α :=
86-
⟨Equiv.ext⟩
87-
#align equiv.perm.apply_has_faithful_smul Equiv.Perm.applyFaithfulSMul
88-
89-
variable {α} {β}
90-
91-
@[to_additive]
92-
protected theorem MulAction.bijective (g : α) : Function.Bijective (g • · : β → β) :=
93-
(MulAction.toPerm g).bijective
94-
#align mul_action.bijective MulAction.bijective
95-
#align add_action.bijective AddAction.bijective
96-
97-
@[to_additive]
98-
protected theorem MulAction.injective (g : α) : Function.Injective (g • · : β → β) :=
99-
(MulAction.bijective g).injective
100-
#align mul_action.injective MulAction.injective
101-
#align add_action.injective AddAction.injective
102-
103-
@[to_additive]
104-
protected theorem MulAction.surjective (g : α) : Function.Surjective (g • · : β → β) :=
105-
(MulAction.bijective g).surjective
106-
#align mul_action.surjective MulAction.surjective
107-
#align add_action.surjective AddAction.surjective
108-
109-
@[to_additive]
110-
theorem smul_left_cancel (g : α) {x y : β} (h : g • x = g • y) : x = y :=
111-
MulAction.injective g h
112-
#align smul_left_cancel smul_left_cancel
113-
#align vadd_left_cancel vadd_left_cancel
114-
115-
@[to_additive (attr := simp)]
116-
theorem smul_left_cancel_iff (g : α) {x y : β} : g • x = g • y ↔ x = y :=
117-
(MulAction.injective g).eq_iff
118-
#align smul_left_cancel_iff smul_left_cancel_iff
119-
#align vadd_left_cancel_iff vadd_left_cancel_iff
120-
121-
@[to_additive]
122-
theorem smul_eq_iff_eq_inv_smul (g : α) {x y : β} : g • x = y ↔ x = g⁻¹ • y :=
123-
(MulAction.toPerm g).apply_eq_iff_eq_symm_apply
124-
#align smul_eq_iff_eq_inv_smul smul_eq_iff_eq_inv_smul
125-
#align vadd_eq_iff_eq_neg_vadd vadd_eq_iff_eq_neg_vadd
126-
127-
end Group
128-
129-
section Monoid
130-
131-
variable [Monoid α] [MulAction α β]
132-
variable (c : α) (x y : β) [Invertible c]
133-
134-
@[simp]
135-
theorem invOf_smul_smul : ⅟c • c • x = x := inv_smul_smul (unitOfInvertible c) _
136-
137-
@[simp]
138-
theorem smul_invOf_smul : c • (⅟ c • x) = x := smul_inv_smul (unitOfInvertible c) _
139-
140-
variable {c x y}
141-
142-
theorem invOf_smul_eq_iff : ⅟c • x = y ↔ x = c • y :=
143-
inv_smul_eq_iff (g := unitOfInvertible c)
144-
145-
theorem smul_eq_iff_eq_invOf_smul : c • x = y ↔ x = ⅟c • y :=
146-
smul_eq_iff_eq_inv_smul (g := unitOfInvertible c)
147-
148-
end Monoid
14926

15027
/-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/
15128
instance CancelMonoidWithZero.faithfulSMul [CancelMonoidWithZero α] [Nontrivial α] :
@@ -298,22 +175,6 @@ end MulDistribMulAction
298175

299176
section Arrow
300177

301-
/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g • F) a = F (g⁻¹ • a)`. -/
302-
@[to_additive (attr := simps) arrowAddAction
303-
"If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)`"]
304-
def arrowAction {G A B : Type*} [DivisionMonoid G] [MulAction G A] : MulAction G (A → B) where
305-
smul g F a := F (g⁻¹ • a)
306-
one_smul := by
307-
intro f
308-
show (fun x => f ((1 : G)⁻¹ • x)) = f
309-
simp only [inv_one, one_smul]
310-
mul_smul := by
311-
intros x y f
312-
show (fun a => f ((x*y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
313-
simp only [mul_smul, mul_inv_rev]
314-
#align arrow_action arrowAction
315-
#align arrow_add_action arrowAddAction
316-
317178
attribute [local instance] arrowAction
318179

319180
/-- When `B` is a monoid, `ArrowAction` is additionally a `MulDistribMulAction`. -/
@@ -338,19 +199,6 @@ end Arrow
338199

339200
namespace IsUnit
340201

341-
section MulAction
342-
343-
variable [Monoid α] [MulAction α β]
344-
345-
@[to_additive]
346-
theorem smul_left_cancel {a : α} (ha : IsUnit a) {x y : β} : a • x = a • y ↔ x = y :=
347-
let ⟨u, hu⟩ := ha
348-
hu ▸ smul_left_cancel_iff u
349-
#align is_unit.smul_left_cancel IsUnit.smul_left_cancel
350-
#align is_add_unit.vadd_left_cancel IsAddUnit.vadd_left_cancel
351-
352-
end MulAction
353-
354202
section DistribMulAction
355203

356204
variable [Monoid α] [AddMonoid β] [DistribMulAction α β]
@@ -368,12 +216,6 @@ section SMul
368216

369217
variable [Group α] [Monoid β]
370218

371-
@[simp]
372-
theorem isUnit_smul_iff [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α)
373-
(m : β) : IsUnit (g • m) ↔ IsUnit m :=
374-
⟨fun h => inv_smul_smul g m ▸ h.smul g⁻¹, IsUnit.smul g⟩
375-
#align is_unit_smul_iff isUnit_smul_iff
376-
377219
theorem IsUnit.smul_sub_iff_sub_inv_smul [AddGroup β] [DistribMulAction α β] [IsScalarTower α β β]
378220
[SMulCommClass α β β] (r : α) (a : β) : IsUnit (r • (1 : β) - a) ↔ IsUnit (1 - r⁻¹ • a) := by
379221
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]

0 commit comments

Comments
 (0)