From 2c5ee0d7efdb723afdf718540ddfabaa477015fc Mon Sep 17 00:00:00 2001 From: Yongle Hu Date: Sat, 19 Oct 2024 18:37:47 +0000 Subject: [PATCH] feat(RingTheory/Ideal/Over): define a class for an ideal lying over an ideal (#17415) Define `class` of an ideal lies over an ideal. Co-authored-by: Yongle Hu @mbkybky Co-authored-by: Jiedong Jiang @jjdishere Co-authored-by: Hu Yongle <2065545849@qq.com> Co-authored-by: Yongle Hu <2065545849@qq.com> --- Mathlib/RingTheory/FiniteType.lean | 5 + Mathlib/RingTheory/Ideal/Maps.lean | 16 +++ Mathlib/RingTheory/Ideal/Over.lean | 126 +++++++++++++++++- .../IsIntegralClosure/Basic.lean | 25 ++++ Mathlib/RingTheory/Noetherian.lean | 8 +- 5 files changed, 176 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean index 8eb4df96ddf80..97c79c644e56a 100644 --- a/Mathlib/RingTheory/FiniteType.lean +++ b/Mathlib/RingTheory/FiniteType.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin -/ import Mathlib.RingTheory.Adjoin.Tower +import Mathlib.RingTheory.Ideal.QuotientOperations /-! # Finiteness conditions in commutative algebra @@ -111,6 +112,10 @@ theorem trans [Algebra S A] [IsScalarTower R S A] (hRS : FiniteType R S) (hSA : FiniteType R A := ⟨fg_trans' hRS.1 hSA.1⟩ +instance quotient (R : Type*) {S : Type*} [CommSemiring R] [CommRing S] [Algebra R S] (I : Ideal S) + [h : Algebra.FiniteType R S] : Algebra.FiniteType R (S ⧸ I) := + Algebra.FiniteType.trans h inferInstance + /-- An algebra is finitely generated if and only if it is a quotient of a free algebra whose variables are indexed by a finset. -/ theorem iff_quotient_freeAlgebra : diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index faa5fc206c934..80ddaa2813840 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -846,3 +846,19 @@ def idealMap (I : Ideal R) : I →ₗ[R] I.map (algebraMap R S) := (fun _ ↦ Ideal.mem_map_of_mem _) end Algebra + +namespace NoZeroSMulDivisors + +theorem of_ker_algebraMap_eq_bot (R A : Type*) [CommRing R] [Semiring A] [Algebra R A] + [NoZeroDivisors A] (h : RingHom.ker (algebraMap R A) = ⊥) : NoZeroSMulDivisors R A := + of_algebraMap_injective ((RingHom.injective_iff_ker_eq_bot _).mpr h) + +theorem ker_algebraMap_eq_bot (R A : Type*) [CommRing R] [Ring A] [Nontrivial A] [Algebra R A] + [NoZeroSMulDivisors R A] : RingHom.ker (algebraMap R A) = ⊥ := + (RingHom.injective_iff_ker_eq_bot _).mp (algebraMap_injective R A) + +theorem iff_ker_algebraMap_eq_bot {R A : Type*} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] : + NoZeroSMulDivisors R A ↔ RingHom.ker (algebraMap R A) = ⊥ := + iff_algebraMap_injective.trans (RingHom.injective_iff_ker_eq_bot (algebraMap R A)) + +end NoZeroSMulDivisors diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index f8586e0f2559a..bbc4a002eeb87 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/Mathlib/RingTheory/Ideal/Over.lean @@ -3,7 +3,6 @@ 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.Algebraic import Mathlib.RingTheory.Localization.AtPrime import Mathlib.RingTheory.Localization.Integral @@ -429,4 +428,129 @@ lemma map_eq_top_iff {R S} [CommRing R] [CommRing S] end IsDomain +section ideal_liesOver + +section Semiring + +variable (A : Type*) [CommSemiring A] {B : Type*} [Semiring B] [Algebra A B] + (P : Ideal B) (p : Ideal A) + +/-- The ideal obtained by pulling back the ideal `P` from `B` to `A`. -/ +abbrev under : Ideal A := Ideal.comap (algebraMap A B) P + +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) + +variable {A} + +/-- `P` lies over `p` if `p` is the preimage of `P` of the `algebraMap`. -/ +class LiesOver : Prop where + over : p = P.under A + +instance over_under : P.LiesOver (P.under A) where over := rfl + +theorem over_def [P.LiesOver p] : p = P.under A := LiesOver.over + +theorem mem_of_liesOver [P.LiesOver p] (x : A) : x ∈ p ↔ algebraMap A B x ∈ P := by + rw [P.over_def p] + rfl + +end Semiring + +section CommSemiring + +variable {A : Type*} [CommSemiring A] {B : Type*} [CommSemiring B] {C : Type*} [Semiring C] + [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] + (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) + +@[simp] +theorem under_under : (𝔓.under B).under A = 𝔓.under A := by + simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq] + +theorem LiesOver.trans [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p where + over := by rw [P.over_def p, 𝔓.over_def P, under_under] + +theorem LiesOver.tower_bot [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p where + over := by rw [𝔓.over_def p, 𝔓.over_def P, under_under] + +variable (B) + +instance under_liesOver_of_liesOver [𝔓.LiesOver p] : (𝔓.under B).LiesOver p := + LiesOver.tower_bot 𝔓 (𝔓.under B) p + +end CommSemiring + +section CommRing + +namespace Quotient + +variable (R : Type*) [CommSemiring R] {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] + [Algebra R A] [Algebra R B] [IsScalarTower R A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] + +/-- If `P` lies over `p`, then canonically `B ⧸ P` is a `A ⧸ p`-algebra. -/ +instance algebraOfLiesOver : Algebra (A ⧸ p) (B ⧸ P) := + algebraQuotientOfLEComap (le_of_eq (P.over_def p)) + +instance isScalarTower_of_liesOver : IsScalarTower R (A ⧸ p) (B ⧸ P) := + IsScalarTower.of_algebraMap_eq' <| + congrArg (algebraMap B (B ⧸ P)).comp (IsScalarTower.algebraMap_eq R A B) + +/-- `B ⧸ P` is a finite `A ⧸ p`-module if `B` is a finite `A`-module. -/ +instance module_finite_of_liesOver [Module.Finite A B] : Module.Finite (A ⧸ p) (B ⧸ P) := + Module.Finite.of_restrictScalars_finite A (A ⧸ p) (B ⧸ P) + +example [Module.Finite A B] : Module.Finite (A ⧸ P.under A) (B ⧸ P) := inferInstance + +/-- `B ⧸ P` is a finitely generated `A ⧸ p`-algebra if `B` is a finitely generated `A`-algebra. -/ +instance algebra_finiteType_of_liesOver [Algebra.FiniteType A B] : + Algebra.FiniteType (A ⧸ p) (B ⧸ P) := + Algebra.FiniteType.of_restrictScalars_finiteType A (A ⧸ p) (B ⧸ P) + +/-- `B ⧸ P` is a Noetherian `A ⧸ p`-module if `B` is a Noetherian `A`-module. -/ +instance isNoetherian_of_liesOver [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ P) := + isNoetherian_of_tower A inferInstance + +theorem algebraMap_injective_of_liesOver : + Function.Injective (algebraMap (A ⧸ p) (B ⧸ P)) := by + rintro ⟨a⟩ ⟨b⟩ hab + apply Quotient.eq.mpr ((mem_of_liesOver P p (a - b)).mpr _) + rw [RingHom.map_sub] + exact Quotient.eq.mp hab + +instance [P.IsPrime] : NoZeroSMulDivisors (A ⧸ p) (B ⧸ P) := + NoZeroSMulDivisors.of_algebraMap_injective (Quotient.algebraMap_injective_of_liesOver P p) + +end Quotient + +end CommRing + +section IsIntegral + +variable {A : Type*} [CommRing A] {B : Type*} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] + (P : Ideal B) (p : Ideal A) [P.LiesOver p] + +variable (A) in +/-- If `B` is an integral `A`-algebra, `P` is a maximal ideal of `B`, then the pull back of + `P` is also a maximal ideal of `A`. -/ +instance IsMaximal.under [P.IsMaximal] : (P.under A).IsMaximal := + isMaximal_comap_of_isIntegral_of_isMaximal P + +theorem IsMaximal.of_liesOver_isMaximal [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal := by + rw [P.over_def p] at hpm + exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm + +theorem IsMaximal.of_isMaximal_liesOver [P.IsMaximal] : p.IsMaximal := by + rw [P.over_def p] + exact isMaximal_comap_of_isIntegral_of_isMaximal P + +/-- `B ⧸ P` is an integral `A ⧸ p`-algebra if `B` is a integral `A`-algebra. -/ +instance Quotient.algebra_isIntegral_of_liesOver : Algebra.IsIntegral (A ⧸ p) (B ⧸ P) := + Algebra.IsIntegral.tower_top A + +end IsIntegral + +end ideal_liesOver + end Ideal diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean index 59406a95b8ec6..eabc18718c598 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean @@ -558,6 +558,18 @@ nonrec theorem RingHom.IsIntegral.tower_bot (hg : Function.Injective g) haveI : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl fun x ↦ IsIntegral.tower_bot hg (hfg (g x)) +variable (T) in +/-- Let `T / S / R` be a tower of algebras, `T` is non-trivial and is a torsion free `S`-module, + then if `T` is an integral `R`-algebra, then `S` is an integral `R`-algebra. -/ +theorem Algebra.IsIntegral.tower_bot [Algebra R S] [Algebra R T] [Algebra S T] + [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T] + [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S where + isIntegral := by + apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T) + (NoZeroSMulDivisors.algebraMap_injective S T) + rw [← IsScalarTower.algebraMap_eq R S T] + exact h.isIntegral + theorem IsIntegral.tower_bot_of_field {R A B : Type*} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x := @@ -571,6 +583,16 @@ theorem RingHom.isIntegralElem.of_comp {x : T} (h : (g.comp f).IsIntegralElem x) theorem RingHom.IsIntegral.tower_top (h : (g.comp f).IsIntegral) : g.IsIntegral := fun x ↦ RingHom.isIntegralElem.of_comp f g (h x) +variable (R) in +/-- Let `T / S / R` be a tower of algebras, `T` is an integral `R`-algebra, then it is integral + as an `S`-algebra. -/ +theorem Algebra.IsIntegral.tower_top [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] + [h : Algebra.IsIntegral R T] : Algebra.IsIntegral S T where + isIntegral := by + apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T) + rw [← IsScalarTower.algebraMap_eq R S T] + exact h.isIntegral + theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) : (Ideal.quotientMap I f le_rfl).IsIntegral := by rintro ⟨x⟩ @@ -578,6 +600,9 @@ theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) : refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩ simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx +instance {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral R (A ⧸ I) := + Algebra.IsIntegral.trans A + instance Algebra.IsIntegral.quotient {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) := ⟨RingHom.IsIntegral.quotient (algebraMap R A) Algebra.IsIntegral.isIntegral⟩ diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean index 903c8862e2b78..411b9fdf6c5a4 100644 --- a/Mathlib/RingTheory/Noetherian.lean +++ b/Mathlib/RingTheory/Noetherian.lean @@ -112,9 +112,11 @@ theorem isNoetherian_of_surjective (f : M →ₗ[R] P) (hf : LinearMap.range f = variable {M} -instance isNoetherian_quotient {R} [Ring R] {M} [AddCommGroup M] [Module R M] - (N : Submodule R M) [IsNoetherian R M] : IsNoetherian R (M ⧸ N) := - isNoetherian_of_surjective _ _ (LinearMap.range_eq_top.mpr N.mkQ_surjective) +instance isNoetherian_quotient {A M : Type*} [Ring A] [AddCommGroup M] [SMul R A] [Module R M] + [Module A M] [IsScalarTower R A M] (N : Submodule A M) [IsNoetherian R M] : + IsNoetherian R (M ⧸ N) := + isNoetherian_of_surjective M ((Submodule.mkQ N).restrictScalars R) <| + LinearMap.range_eq_top.mpr N.mkQ_surjective @[deprecated (since := "2024-04-27"), nolint defLemma] alias Submodule.Quotient.isNoetherian := isNoetherian_quotient