chore(group_theory/subgroup/basic): split out some self-contained sec…

…tions (#17862)

This is a very big file by mathlib standards at over 3000 lines. It seems helpful to reduce that by splitting some of the less fundamental definitions into their own files.

src/algebra/periodic.lean

@@ -8,6 +8,7 @@ import algebra.module.basic
 import algebra.order.archimedean
 import data.int.parity
 import group_theory.coset
+import group_theory.subgroup.zpowers
 
 /-!
 # Periodicity

src/group_theory/coset.lean

@@ -6,6 +6,7 @@ Authors: Mitchell Rowett, Scott Morrison
 
 import algebra.quotient
 import group_theory.group_action.basic
+import group_theory.subgroup.mul_opposite
 import tactic.group
 
 /-!

src/group_theory/group_action/conj_act.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import group_theory.group_action.basic
-import group_theory.subgroup.basic
+import group_theory.subgroup.zpowers
 import algebra.group_ring_action.basic
 /-!
 # Conjugation action of a group on itself

src/group_theory/group_action/fixing_subgroup.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
 
-import group_theory.subgroup.basic
+import group_theory.subgroup.actions
 import group_theory.group_action.basic
 
 /-!

src/group_theory/solvable.lean

@@ -7,6 +7,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 import data.fin.vec_notation
 import group_theory.abelianization
 import group_theory.perm.via_embedding
+import group_theory.subgroup.simple
 import set_theory.cardinal.basic
 
 /-!

src/group_theory/specific_groups/alternating.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson
 
 import algebra.group.conj_finite
 import group_theory.perm.fin
+import group_theory.subgroup.simple
 import tactic.interval_cases
 
 /-!

src/group_theory/specific_groups/cyclic.lean

@@ -7,6 +7,7 @@ Authors: Johannes Hölzl
 import algebra.big_operators.order
 import data.nat.totient
 import group_theory.order_of_element
+import group_theory.subgroup.simple
 import tactic.group
 import group_theory.exponent
 

src/group_theory/subgroup/actions.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import group_theory.subgroup.basic
+
+/-!
+# Actions by `subgroup`s
+
+These are just copies of the definitions about `submonoid` starting from `submonoid.mul_action`.
+
+## Tags
+subgroup, subgroups
+
+-/
+
+namespace subgroup
+
+variables {G : Type*} [group G]
+variables {α β : Type*}
+
+/-- The action by a subgroup is the action by the underlying group. -/
+@[to_additive /-"The additive action by an add_subgroup is the action by the underlying
+add_group. "-/]
+instance [mul_action G α] (S : subgroup G) : mul_action S α :=
+S.to_submonoid.mul_action
+
+@[to_additive]
+lemma smul_def [mul_action G α] {S : subgroup G} (g : S) (m : α) : g • m = (g : G) • m := rfl
+
+@[to_additive]
+instance smul_comm_class_left
+  [mul_action G β] [has_smul α β] [smul_comm_class G α β] (S : subgroup G) :
+  smul_comm_class S α β :=
+S.to_submonoid.smul_comm_class_left
+
+@[to_additive]
+instance smul_comm_class_right
+  [has_smul α β] [mul_action G β] [smul_comm_class α G β] (S : subgroup G) :
+  smul_comm_class α S β :=
+S.to_submonoid.smul_comm_class_right
+
+/-- Note that this provides `is_scalar_tower S G G` which is needed by `smul_mul_assoc`. -/
+instance
+  [has_smul α β] [mul_action G α] [mul_action G β] [is_scalar_tower G α β] (S : subgroup G) :
+  is_scalar_tower S α β :=
+S.to_submonoid.is_scalar_tower
+
+instance [mul_action G α] [has_faithful_smul G α] (S : subgroup G) :
+  has_faithful_smul S α :=
+S.to_submonoid.has_faithful_smul
+
+/-- The action by a subgroup is the action by the underlying group. -/
+instance [add_monoid α] [distrib_mul_action G α] (S : subgroup G) : distrib_mul_action S α :=
+S.to_submonoid.distrib_mul_action
+
+/-- The action by a subgroup is the action by the underlying group. -/
+instance [monoid α] [mul_distrib_mul_action G α] (S : subgroup G) : mul_distrib_mul_action S α :=
+S.to_submonoid.mul_distrib_mul_action
+
+/-- The center of a group acts commutatively on that group. -/
+instance center.smul_comm_class_left : smul_comm_class (center G) G G :=
+submonoid.center.smul_comm_class_left
+
+/-- The center of a group acts commutatively on that group. -/
+instance center.smul_comm_class_right : smul_comm_class G (center G) G :=
+submonoid.center.smul_comm_class_right
+
+end subgroup