From d57b21ae7ff501413f6ee2443a90d83173930e50 Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Mon, 28 Oct 2024 23:09:04 +0000 Subject: [PATCH] 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 | 13 +++++-- Mathlib/RingTheory/Ideal/Pointwise.lean | 51 ++++++++++++++----------- 2 files changed, 38 insertions(+), 26 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index bbc4a002eeb87..b5adc93c0c078 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/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`. -/ diff --git a/Mathlib/RingTheory/Ideal/Pointwise.lean b/Mathlib/RingTheory/Ideal/Pointwise.lean index cde9b62eabc90..5116083a5f52f 100644 --- a/Mathlib/RingTheory/Ideal/Pointwise.lean +++ b/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]