feat(RingTheory/Ideal/Over): define a class for an ideal lying over a…

…n 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 <[email protected]>
Co-authored-by: Yongle Hu <[email protected]>

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 :

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

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

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,13 +583,26 @@ 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⟩
   obtain ⟨p, p_monic, hpx⟩ := hf x
   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⟩

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