[Merged by Bors] - feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M]

Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean

@@ -3,24 +3,35 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Group.Submonoid.Defs
-import Mathlib.Algebra.GroupWithZero.Action.End
+import Mathlib.Algebra.Group.Submonoid.MulAction
+import Mathlib.Algebra.GroupWithZero.Action.Defs
 
 /-!
 # Distributive actions by submonoids
 -/
 
 namespace Submonoid
+
 variable {M α : Type*} [Monoid M]
 
+variable {S : Type*} [SetLike S M] (s : S) [SubmonoidClass S M]
+
+instance [AddMonoid α] [DistribMulAction M α] : DistribMulAction s α where
+  smul_zero r := smul_zero (r : M)
+  smul_add r := smul_add (r : M)
+
 /-- The action by a submonoid is the action by the underlying monoid. -/
 instance distribMulAction [AddMonoid α] [DistribMulAction M α] (S : Submonoid M) :
     DistribMulAction S α :=
-  DistribMulAction.compHom _ S.subtype
+  inferInstance
+
+instance [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction s α where
+  smul_mul r := smul_mul' (r : M)
+  smul_one r := smul_one (r : M)
 
 /-- The action by a submonoid is the action by the underlying monoid. -/
 instance mulDistribMulAction [Monoid α] [MulDistribMulAction M α] (S : Submonoid M) :
     MulDistribMulAction S α :=
-  MulDistribMulAction.compHom _ S.subtype
+  inferInstance
 
 end Submonoid

Mathlib/Algebra/Group/Submonoid/MulAction.lean

@@ -20,29 +20,64 @@ namespace Submonoid
 
 variable {M' : Type*} {α β : Type*}
 
+section SetLike
+
+variable {S' : Type*} [SetLike S' M'] (s : S')
+
+@[to_additive]
+instance [SMul M' α]  : SMul s α where
+  smul m a := (m : M') • a
+
+section MulOneClass
+
+variable [MulOneClass M']
+
+@[to_additive]
+instance [SMul M' β] [SMul α β] [SMulCommClass M' α β] : SMulCommClass s α β :=
+  ⟨fun a _ _ => smul_comm (a : M') _ _⟩
+
+@[to_additive]
+instance [SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α s β :=
+  ⟨fun a s => smul_comm a (s : M')⟩
+
+instance [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] :
+    IsScalarTower s α β :=
+  ⟨fun a => smul_assoc (a : M')⟩
+
+end MulOneClass
+
+variable [Monoid M'] [SubmonoidClass S' M']
+
+@[to_additive]
+instance [MulAction M' α] : MulAction s α where
+  one_smul := one_smul M'
+  mul_smul m₁ m₂ := mul_smul (m₁ : M') m₂
+
+end SetLike
+
 section MulOneClass
 
 variable [MulOneClass M']
 
 @[to_additive]
 instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
-  SMul.comp _ S.subtype
+  inferInstance
 
 @[to_additive]
 instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
     (S : Submonoid M') : SMulCommClass S α β :=
-  ⟨fun a _ _ => smul_comm (a : M') _ _⟩
+  inferInstance
 
 @[to_additive]
 instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
     (S : Submonoid M') : SMulCommClass α S β :=
-  ⟨fun a s => smul_comm a (s : M')⟩
+  inferInstance
 
 /-- 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')⟩
+  inferInstance
 
 section SMul
 variable [SMul M' α] {S : Submonoid M'}
@@ -60,9 +95,8 @@ 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₂
+instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
+  inferInstance
 
 example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
 

Mathlib/Algebra/Ring/Action/Subobjects.lean

@@ -22,12 +22,16 @@ for those subobjects.
 variable {M G R : Type*}
 variable [Monoid M] [Group G] [Semiring R]
 
+instance [MulSemiringAction M R] {S : Type*} [SetLike S M] (s : S) [SubmonoidClass S M] :
+    MulSemiringAction s R :=
+  { inferInstanceAs (DistribMulAction s R), inferInstanceAs (MulDistribMulAction s R) with }
+
 /-- A stronger version of `Submonoid.distribMulAction`. -/
 instance Submonoid.mulSemiringAction [MulSemiringAction M R] (H : Submonoid M) :
     MulSemiringAction H R :=
-  { inferInstanceAs (DistribMulAction H R), inferInstanceAs (MulDistribMulAction H R) with }
+  inferInstance
 
 /-- A stronger version of `Subgroup.distribMulAction`. -/
 instance Subgroup.mulSemiringAction [MulSemiringAction G R] (H : Subgroup G) :
     MulSemiringAction H R :=
-  H.toSubmonoid.mulSemiringAction
+  inferInstance

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Submonoid.BigOperators
-import Mathlib.Algebra.Module.RingHom
 import Mathlib.Algebra.Ring.Action.Subobjects
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Algebra.Ring.Prod
 import Mathlib.Algebra.Ring.Subsemiring.Defs
 import Mathlib.GroupTheory.Submonoid.Centralizer
 import Mathlib.RingTheory.NonUnitalSubsemiring.Basic
+import Mathlib.Algebra.Module.Defs
 
 /-!
 # Bundled subsemirings
@@ -841,71 +841,98 @@ namespace Subsemiring
 
 variable {R' α β : Type*}
 
+variable {S' : Type*} [SetLike S' R'] (s : S)
+
 section NonAssocSemiring
 
 variable [NonAssocSemiring R']
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance smul [SMul R' α] (S : Subsemiring R') : SMul S α :=
-  S.toSubmonoid.smul
+  inferInstance
 
 theorem smul_def [SMul R' α] {S : Subsemiring R'} (g : S) (m : α) : g • m = (g : R') • m :=
   rfl
 
 instance smulCommClass_left [SMul R' β] [SMul α β] [SMulCommClass R' α β] (S : Subsemiring R') :
     SMulCommClass S α β :=
-  S.toSubmonoid.smulCommClass_left
+  inferInstance
 
 instance smulCommClass_right [SMul α β] [SMul R' β] [SMulCommClass α R' β] (S : Subsemiring R') :
     SMulCommClass α S β :=
-  S.toSubmonoid.smulCommClass_right
+  inferInstance
 
 /-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`. -/
 instance isScalarTower [SMul α β] [SMul R' α] [SMul R' β] [IsScalarTower R' α β]
     (S : Subsemiring R') :
     IsScalarTower S α β :=
-  S.toSubmonoid.isScalarTower
+  inferInstance
+
+instance {M' α : Type*} [SMul M' α] {S' : Type*}
+    [SetLike S' M'] (s : S') [FaithfulSMul M' α] : FaithfulSMul s α :=
+  ⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩
 
 instance faithfulSMul [SMul R' α] [FaithfulSMul R' α] (S : Subsemiring R') : FaithfulSMul S α :=
-  S.toSubmonoid.faithfulSMul
+  inferInstance
+
+instance {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S')
+    [Zero α] [SMulWithZero R' α] : SMulWithZero s α where
+  smul_zero r := smul_zero (r : R')
+  zero_smul := zero_smul R'
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance [Zero α] [SMulWithZero R' α] (S : Subsemiring R') : SMulWithZero S α :=
-  SMulWithZero.compHom _ S.subtype.toMonoidWithZeroHom.toZeroHom
+  inferInstance
 
 end NonAssocSemiring
 
 variable [Semiring R']
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance mulAction [MulAction R' α] (S : Subsemiring R') : MulAction S α :=
-  S.toSubmonoid.mulAction
+  inferInstance
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance distribMulAction [AddMonoid α] [DistribMulAction R' α] (S : Subsemiring R') :
     DistribMulAction S α :=
-  S.toSubmonoid.distribMulAction
+  inferInstance
+
+instance [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R']
+    (s : S') : Module s α where
+  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
+  zero_smul := zero_smul R'
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance mulDistribMulAction [Monoid α] [MulDistribMulAction R' α] (S : Subsemiring R') :
     MulDistribMulAction S α :=
-  S.toSubmonoid.mulDistribMulAction
+  inferInstance
+
+instance {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S')
+    [Zero α] [MulActionWithZero R' α] : MulActionWithZero s α where
+  smul_zero r := smul_zero (r : R')
+  zero_smul := zero_smul R'
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance mulActionWithZero [Zero α] [MulActionWithZero R' α] (S : Subsemiring R') :
     MulActionWithZero S α :=
-  MulActionWithZero.compHom _ S.subtype.toMonoidWithZeroHom
+  inferInstance
+
+instance [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R']
+    (s : S') : Module s α where
+  toDistribMulAction := inferInstance
+  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
+  zero_smul := zero_smul R'
 
 -- Porting note: instance named explicitly for use in `RingTheory/Subring/Basic`
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance module [AddCommMonoid α] [Module R' α] (S : Subsemiring R') : Module S α :=
   -- Porting note: copying over the `smul` field causes a timeout
   -- { Module.compHom _ S.subtype with smul := (· • ·) }
-  Module.compHom _ S.subtype
+  inferInstance
 
 /-- The action by a subsemiring is the action by the underlying semiring. -/
 instance [Semiring α] [MulSemiringAction R' α] (S : Subsemiring R') : MulSemiringAction S α :=
-  S.toSubmonoid.mulSemiringAction
+  inferInstance
 
 /-- The center of a semiring acts commutatively on that semiring. -/
 instance center.smulCommClass_left : SMulCommClass (center R') R' R' :=

Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.Regular.Basic
 import Mathlib.GroupTheory.MonoidLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.Basic
+import Mathlib.Algebra.GroupWithZero.Units.Basic
 
 /-!
 # Localizations of commutative monoids with zeroes

Mathlib/RingTheory/OreLocalization/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
 -/
 import Mathlib.Algebra.Group.Submonoid.DistribMulAction
 import Mathlib.GroupTheory.OreLocalization.Basic
+import Mathlib.Algebra.GroupWithZero.Defs
 
 /-!