refactor(group_theory/subgroup,linear_algebra/basic): put pointwise a…

…ctions in their own files to match submonoid (#9312)

src/algebra/algebra/operations.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import algebra.algebra.basic
+import algebra.module.submodule_pointwise
 
 /-!
 # Multiplication and division of submodules of an algebra.

src/algebra/category/Group/limits.lean

@@ -8,7 +8,7 @@ import algebra.category.Group.preadditive
 import category_theory.over
 import category_theory.limits.concrete_category
 import category_theory.limits.shapes.concrete_category
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # The category of (commutative) (additive) groups has all limits

src/algebra/direct_sum/basic.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau
 -/
 import data.dfinsupp
 import group_theory.submonoid.operations
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Direct sum

src/algebra/direct_sum/ring.lean

@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import algebra.algebra.basic
 import algebra.algebra.operations
 import algebra.direct_sum.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Additively-graded multiplicative structures on `⨁ i, A i`

src/algebra/group_ring_action.lean

@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import group_theory.group_action.group
+import algebra.pointwise
 import data.equiv.ring
+import group_theory.group_action.group
+import group_theory.submonoid.pointwise
+import group_theory.subgroup.pointwise
 import ring_theory.subring
-import algebra.pointwise
 
 /-!
 # Group action on rings

src/algebra/module/submodule_pointwise.lean

@@ -0,0 +1,97 @@
+/-
+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.pointwise
+import linear_algebra.basic
+
+/-! # Pointwise instances on `submodule`s
+
+This file provides the actions
+
+* `submodule.pointwise_distrib_mul_action`
+* `submodule.pointwise_mul_action_with_zero`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+-/
+
+namespace submodule
+
+variables {α : Type*} {R : Type*} {M : Type*}
+variables [semiring R] [add_comm_monoid M] [module R M]
+
+
+instance pointwise_add_comm_monoid : add_comm_monoid (submodule R M) :=
+{ add := (⊔),
+  add_assoc := λ _ _ _, sup_assoc,
+  zero := ⊥,
+  zero_add := λ _, bot_sup_eq,
+  add_zero := λ _, sup_bot_eq,
+  add_comm := λ _ _, sup_comm }
+
+@[simp] lemma add_eq_sup (p q : submodule R M) : p + q = p ⊔ q := rfl
+@[simp] lemma zero_eq_bot : (0 : submodule R M) = ⊥ := rfl
+
+
+section
+variables [monoid α] [distrib_mul_action α M] [smul_comm_class α R M]
+
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_distrib_mul_action : distrib_mul_action α (submodule R M) :=
+{ smul := λ a S, S.map (distrib_mul_action.to_linear_map _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact one_smul α)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact mul_smul _ _)).trans (S.map_comp _ _),
+  smul_zero := λ a, map_bot _,
+  smul_add := λ a S₁ S₂, map_sup _ _ _ }
+
+localized "attribute [instance] submodule.pointwise_distrib_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : submodule R M) : ↑(a • S) = a • (S : set M) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : submodule R M) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+@[simp] lemma pointwise_smul_to_add_subgroup {R M : Type*}
+  [ring R] [add_comm_group M] [distrib_mul_action α M] [module R M] [smul_comm_class α R M]
+  (a : α) (S : submodule R M) :
+  (a • S).to_add_subgroup = a • S.to_add_subgroup := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
+
+@[simp] lemma smul_le_self_of_tower {α : Type*}
+  [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
+  (a : α) (S : submodule R M) : a • S ≤ S :=
+begin
+  rintro y ⟨x, hx, rfl⟩,
+  exact smul_of_tower_mem _ a hx,
+end
+
+end
+
+section
+variables [semiring α] [module α M] [smul_comm_class α R M]
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale.
+
+This is a stronger version of `submodule.pointwise_distrib_mul_action`. Note that `add_smul` does
+not hold so this cannot be stated as a `module`. -/
+protected def pointwise_mul_action_with_zero : mul_action_with_zero α (submodule R M) :=
+{ zero_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact zero_smul α)).trans S.map_zero,
+  .. submodule.pointwise_distrib_mul_action }
+
+localized "attribute [instance] submodule.pointwise_mul_action_with_zero" in pointwise
+
+end
+
+end submodule

src/deprecated/subgroup.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro,
   Michael Howes
 -/
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import deprecated.submonoid
 /-!
 # Unbundled subgroups

src/group_theory/archimedean.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Heather Macbeth, Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Patrick Massot
 -/
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import algebra.archimedean
 
 /-!

src/group_theory/coset.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mitchell Rowett, Scott Morrison
 -/
 
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Cosets

src/group_theory/finiteness.lean

@@ -6,7 +6,7 @@ Authors: Riccardo Brasca
 
 import data.set.finite
 import group_theory.submonoid.operations
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Finitely generated monoids and groups

src/group_theory/free_group.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import data.fintype.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Free groups

src/group_theory/general_commutator.lean

@@ -5,7 +5,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
 
 import data.bracket
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import tactic.group
 
 /-!

src/group_theory/perm/subgroup.lean

@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import group_theory.perm.basic
 import data.fintype.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 /-!
 # Lemmas about subgroups within the permutations (self-equivalences) of a type `α`
 

src/group_theory/semidirect_product.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import data.equiv.mul_add_aut
 import logic.function.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Semidirect product

src/group_theory/subgroup.lean → src/group_theory/subgroup/basic.lean

@@ -5,9 +5,7 @@ Authors: Kexing Ying
 -/
 import group_theory.submonoid
 import group_theory.submonoid.center
-import group_theory.submonoid.pointwise
 import algebra.group.conj
-import algebra.pointwise
 import order.atoms
 
 /-!
@@ -2339,65 +2337,6 @@ end subgroup
 
 end actions
 
-/-! ### Pointwise instances on `subgroup`s -/
-
-section
-variables {α : Type*}
-
-namespace subgroup
-
-variables [monoid α] [mul_distrib_mul_action α G]
-
-/-- The action on a subgroup corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (subgroup G) :=
-{ smul := λ a S, S.map (mul_distrib_mul_action.to_monoid_End _ _ a),
-  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
-
-localized "attribute [instance] subgroup.pointwise_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (a : α) (S : subgroup G) : ↑(a • S) = a • (S : set G) := rfl
-
-@[simp] lemma pointwise_smul_to_submonoid (a : α) (S : subgroup G) :
-  (a • S).to_submonoid = a • S.to_submonoid := rfl
-
-lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
-
-end subgroup
-
-namespace add_subgroup
-
-variables [monoid α] [distrib_mul_action α A]
-
-/-- The action on a additive subgroup corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (add_subgroup A) :=
-{ smul := λ a S, S.map (distrib_mul_action.to_add_monoid_End _ _ a),
-  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
-
-localized "attribute [instance] add_subgroup.pointwise_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (a : α) (S : add_subgroup A) : ↑(a • S) = a • (S : set A) := rfl
-
-@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : add_subgroup A) :
-  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
-
-lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
-
-end add_subgroup
-
-end
-
 /-! ### Saturated subgroups -/
 
 section saturated

src/group_theory/subgroup/pointwise.lean

@@ -0,0 +1,73 @@
+/-
+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
+import group_theory.submonoid.pointwise
+
+/-! # Pointwise instances on `subgroup`s
+
+This file provides the actions
+
+* `subgroup.pointwise_mul_action`
+* `add_subgroup.pointwise_mul_action`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+-/
+
+variables {α : Type*} {G : Type*} {A : Type*} [group G] [add_group A]
+
+namespace subgroup
+
+variables [monoid α] [mul_distrib_mul_action α G]
+
+/-- The action on a subgroup corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_mul_action : mul_action α (subgroup G) :=
+{ smul := λ a S, S.map (mul_distrib_mul_action.to_monoid_End _ _ a),
+  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : subgroup G) : ↑(a • S) = a • (S : set G) := rfl
+
+@[simp] lemma pointwise_smul_to_submonoid (a : α) (S : subgroup G) :
+  (a • S).to_submonoid = a • S.to_submonoid := rfl
+
+lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
+
+end subgroup
+
+namespace add_subgroup
+
+variables [monoid α] [distrib_mul_action α A]
+
+/-- The action on a additive subgroup corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_mul_action : mul_action α (add_subgroup A) :=
+{ smul := λ a S, S.map (distrib_mul_action.to_add_monoid_End _ _ a),
+  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] add_subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : add_subgroup A) : ↑(a • S) = a • (S : set A) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : add_subgroup A) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
+
+end add_subgroup

src/group_theory/submonoid/pointwise.lean

@@ -6,7 +6,18 @@ Authors: Eric Wieser
 import group_theory.submonoid.operations
 import algebra.pointwise
 
-/-! ### Pointwise instances on `submonoid`s and `add_submonoid`s -/
+/-! # Pointwise instances on `submonoid`s and `add_submonoid`s
+
+This file provides the actions
+
+* `submonoid.pointwise_mul_action`
+* `add_submonoid.pointwise_mul_action`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+
+-/
 
 section
 variables {M' : Type*} {α β : Type*}