refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355)

This PR generalizes much of `RingTheory/Ideal/Pointwise` to semirings. I also moved a couple lemmas from the `Group` section to the `Monoid` section, and added a lemma to `RingTheory/Ideal/Over`.

Mathlib/RingTheory/Ideal/Over.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
+import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.RingTheory.Localization.Integral
 
@@ -28,11 +29,9 @@ variable {R : Type*} [CommRing R]
 
 namespace Ideal
 
-open Polynomial
+open Polynomial Submodule
 
-open Polynomial
-
-open Submodule
+open scoped Pointwise
 
 section CommRing
 
@@ -443,6 +442,12 @@ theorem under_def : P.under A = Ideal.comap (algebraMap A B) P := rfl
 instance IsPrime.under [hP : P.IsPrime] : (P.under A).IsPrime :=
   hP.comap (algebraMap A B)
 
+@[simp]
+lemma under_smul {G : Type*} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (g : G) :
+    (g • P : Ideal B).under A = P.under A := by
+  ext a
+  rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
+
 variable {A}
 
 /-- `P` lies over `p` if `p` is the preimage of `P` of the `algebraMap`. -/

Mathlib/RingTheory/Ideal/Pointwise.lean

@@ -28,26 +28,34 @@ namespace Ideal
 
 section Monoid
 
-variable [Monoid M] [CommRing R] [MulSemiringAction M R]
+variable [Monoid M] [Semiring R] [MulSemiringAction M R]
 
 /-- The action on an ideal corresponding to applying the action to every element.
 
 This is available as an instance in the `Pointwise` locale. -/
-protected def pointwiseMulSemiringAction : MulSemiringAction M (Ideal R) where
+protected def pointwiseDistribMulAction : DistribMulAction M (Ideal R) where
   smul a := Ideal.map (MulSemiringAction.toRingHom _ _ a)
   one_smul I :=
     congr_arg (I.map ·) (RingHom.ext <| one_smul M) |>.trans I.map_id
   mul_smul _ _ I :=
     congr_arg (I.map ·) (RingHom.ext <| mul_smul _ _) |>.trans (I.map_map _ _).symm
-  smul_one a := by simp only [Ideal.one_eq_top]; exact Ideal.map_top _
-  smul_mul a I J := Ideal.map_mul (MulSemiringAction.toRingHom _ _ a) I J
-  smul_add _ I J := Ideal.map_sup _ I J
   smul_zero _ := Ideal.map_bot
+  smul_add _ I J := Ideal.map_sup _ I J
 
-scoped[Pointwise] attribute [instance] Ideal.pointwiseMulSemiringAction
+scoped[Pointwise] attribute [instance] Ideal.pointwiseDistribMulAction
 
 open Pointwise
 
+/-- The action on an ideal corresponding to applying the action to every element.
+
+This is available as an instance in the `Pointwise` locale. -/
+protected def pointwiseMulSemiringAction {R : Type*} [CommRing R] [MulSemiringAction M R] :
+    MulSemiringAction M (Ideal R) where
+  smul_one a := by simp only [Ideal.one_eq_top]; exact Ideal.map_top _
+  smul_mul a I J := Ideal.map_mul (MulSemiringAction.toRingHom _ _ a) I J
+
+scoped[Pointwise] attribute [instance] Ideal.pointwiseMulSemiringAction
+
 theorem pointwise_smul_def {a : M} (S : Ideal R) :
     a • S = S.map (MulSemiringAction.toRingHom _ _ a) :=
   rfl
@@ -76,12 +84,25 @@ instance pointwise_central_scalar [MulSemiringAction Mᵐᵒᵖ R] [IsCentralSca
     IsCentralScalar M (Ideal R) :=
   ⟨fun _ S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩
 
+@[simp]
+theorem pointwise_smul_toAddSubmonoid (a : M) (S : Ideal R)
+    (ha : Function.Surjective fun r : R => a • r) :
+    (a • S).toAddSubmonoid = a • S.toAddSubmonoid := by
+  ext
+  exact Ideal.mem_map_iff_of_surjective _ <| by exact ha
+
+@[simp]
+theorem pointwise_smul_toAddSubGroup {R : Type*} [Ring R] [MulSemiringAction M R]
+    (a : M) (S : Ideal R) (ha : Function.Surjective fun r : R => a • r)  :
+    (a • S).toAddSubgroup = a • S.toAddSubgroup := by
+  ext
+  exact Ideal.mem_map_iff_of_surjective _ <| by exact ha
+
 end Monoid
 
 section Group
 
-variable [Group M] [CommRing R] [MulSemiringAction M R]
-
+variable [Group M] [Semiring R] [MulSemiringAction M R]
 
 open Pointwise
 
@@ -100,20 +121,6 @@ theorem mem_pointwise_smul_iff_inv_smul_mem {a : M} {S : Ideal R} {x : R} :
   ⟨fun h => by simpa using smul_mem_pointwise_smul a⁻¹ _ _ h,
     fun h => by simpa using smul_mem_pointwise_smul a _ _ h⟩
 
-@[simp]
-theorem pointwise_smul_toAddSubmonoid (a : M) (S : Ideal R)
-    (ha : Function.Surjective fun r : R => a • r) :
-    (a • S).toAddSubmonoid = a • S.toAddSubmonoid := by
-  ext
-  exact Ideal.mem_map_iff_of_surjective _ <| by exact ha
-
-@[simp]
-theorem pointwise_smul_toAddSubGroup (a : M) (S : Ideal R)
-    (ha : Function.Surjective fun r : R => a • r)  :
-    (a • S).toAddSubgroup = a • S.toAddSubgroup := by
-  ext
-  exact Ideal.mem_map_iff_of_surjective _ <| by exact ha
-
 theorem mem_inv_pointwise_smul_iff {a : M} {S : Ideal R} {x : R} : x ∈ a⁻¹ • S ↔ a • x ∈ S := by
   rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]