[Merged by Bors] - chore(Algebra/Group/Submonoid/Operations): move instances to new file

Mathlib.lean

@@ -354,6 +354,7 @@ import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Algebra.Group.Submonoid.DistribMulAction
 import Mathlib.Algebra.Group.Submonoid.Finsupp
 import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.Group.Submonoid.MulAction
 import Mathlib.Algebra.Group.Submonoid.MulOpposite
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Group.Submonoid.Pointwise

Mathlib/Algebra/Group/Submonoid/MulAction.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.Group.Submonoid.Defs
+import Mathlib.Algebra.Group.Action.Defs
+
+/-!
+# Actions by `Submonoid`s
+
+These instances transfer the action by an element `m : M` of a monoid `M` written as `m • a` onto
+the action by an element `s : S` of a submonoid `S : Submonoid M` such that `s • a = (s : M) • a`.
+
+These instances work particularly well in conjunction with `Monoid.toMulAction`, enabling
+`s • m` as an alias for `↑s * m`.
+-/
+
+namespace Submonoid
+
+variable {M' : Type*} {α β : Type*}
+
+section MulOneClass
+
+variable [MulOneClass M']
+
+@[to_additive]
+instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
+  SMul.comp _ S.subtype
+
+@[to_additive]
+instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
+    (S : Submonoid M') : SMulCommClass S α β :=
+  ⟨fun a _ _ => smul_comm (a : M') _ _⟩
+
+@[to_additive]
+instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
+    (S : Submonoid M') : SMulCommClass α S β :=
+  ⟨fun a s => smul_comm a (s : M')⟩
+
+/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
+instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β]
+      (S : Submonoid M') :
+    IsScalarTower S α β :=
+  ⟨fun a => smul_assoc (a : M')⟩
+
+section SMul
+variable [SMul M' α] {S : Submonoid M'}
+
+@[to_additive] lemma smul_def (g : S) (a : α) : g • a = (g : M') • a := rfl
+
+@[to_additive (attr := simp)]
+lemma mk_smul (g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl
+
+end SMul
+end MulOneClass
+
+variable [Monoid M']
+
+/-- The action by a submonoid is the action by the underlying monoid. -/
+@[to_additive
+      "The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. "]
+instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α where
+  one_smul := one_smul M'
+  mul_smul m₁ m₂ := mul_smul (m₁ : M') m₂
+
+example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
+
+end Submonoid

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Group.Action.Faithful
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Submonoid.Basic
+import Mathlib.Algebra.Group.Submonoid.MulAction
 import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
@@ -973,75 +974,10 @@ theorem Submonoid.equivMapOfInjective_coe_mulEquiv (e : M ≃* N) :
   ext
   rfl
 
-section Actions
-
-/-! ### Actions by `Submonoid`s
-
-These instances transfer the action by an element `m : M` of a monoid `M` written as `m • a` onto
-the action by an element `s : S` of a submonoid `S : Submonoid M` such that `s • a = (s : M) • a`.
-
-These instances work particularly well in conjunction with `Monoid.toMulAction`, enabling
-`s • m` as an alias for `↑s * m`.
--/
-
-
-namespace Submonoid
-
-variable {M' : Type*} {α β : Type*}
-
-section MulOneClass
-
-variable [MulOneClass M']
-
-@[to_additive]
-instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
-  SMul.comp _ S.subtype
-
-@[to_additive]
-instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
-    (S : Submonoid M') : SMulCommClass S α β :=
-  ⟨fun a _ _ => smul_comm (a : M') _ _⟩
-
-@[to_additive]
-instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
-    (S : Submonoid M') : SMulCommClass α S β :=
-  ⟨fun a s => smul_comm a (s : M')⟩
-
-/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
-instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β]
-      (S : Submonoid M') :
-    IsScalarTower S α β :=
-  ⟨fun a => smul_assoc (a : M')⟩
-
-section SMul
-variable [SMul M' α] {S : Submonoid M'}
-
-@[to_additive] lemma smul_def (g : S) (a : α) : g • a = (g : M') • a := rfl
-
-@[to_additive (attr := simp)]
-lemma mk_smul (g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl
-
-instance faithfulSMul [FaithfulSMul M' α] : FaithfulSMul S α :=
+instance Submonoid.faithfulSMul {M' α : Type*} [MulOneClass M'] [SMul M' α] {S : Submonoid M'}
+    [FaithfulSMul M' α] : FaithfulSMul S α :=
   ⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩
 
-end SMul
-end MulOneClass
-
-variable [Monoid M']
-
-/-- The action by a submonoid is the action by the underlying monoid. -/
-@[to_additive
-      "The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. "]
-instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
-  MulAction.compHom _ S.subtype
-
-example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
-
-
-end Submonoid
-
-end Actions
-
 section Units
 
 namespace Submonoid

Mathlib/Algebra/Module/Submodule/Defs.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.GroupTheory.GroupAction.SubMulAction
+import Mathlib.Algebra.Group.Submonoid.Basic
 
 /-!
 

Mathlib/Algebra/Polynomial/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.MonoidAlgebra.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Data.Finset.Sort
 import Mathlib.Tactic.FastInstance
+import Mathlib.Algebra.Group.Submonoid.Operations
 
 /-!
 # Theory of univariate polynomials

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -5,8 +5,8 @@ Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.Group.Submonoid.MulAction
 
 /-!
 # Definition of `orbit`, `fixedPoints` and `stabilizer`

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -6,6 +6,7 @@ Authors: Amelia Livingston
 import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.GroupTheory.Congruence.Hom
 import Mathlib.GroupTheory.OreLocalization.Basic
+import Mathlib.Algebra.Group.Submonoid.Operations
 
 /-!
 # Localizations of commutative monoids

Mathlib/GroupTheory/OreLocalization/Basic.lean

@@ -3,9 +3,10 @@ Copyright (c) 2022 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
 -/
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.GroupTheory.OreLocalization.OreSet
 import Mathlib.Tactic.Common
+import Mathlib.Algebra.Group.Submonoid.MulAction
+import Mathlib.Algebra.Group.Units.Defs
 
 /-!
 

Mathlib/Topology/Algebra/Monoid.lean

@@ -9,6 +9,7 @@ import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.Group.ULift
 import Mathlib.Topology.ContinuousMap.Defs
+import Mathlib.Algebra.Group.Submonoid.Basic
 
 /-!
 # Theory of topological monoids