Skip to content

Commit 8c79cb4

Browse files
rshlyakhrshlyakh
committed
feat(RingTheory/Ideal): add Algebra.HasGoingUp (leanprover-community#40911)
This closely mirrors `Mathlib/RingTheory/Ideal/GoingDown.lean` by defining an analogous predicate `Algebra.HasGoingUp` and proving basic properties. It includes: - `Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap`: going up is equivalent to specializations lifting along `Spec S → Spec R`. - `Algebra.HasGoingUp.of_isIntegral`: integral algebras satisfy going up. - `Ideal.exists_ltSeries_of_hasGoingUp`: a generalization of `exists_ideal_over_prime_of_isIntegral_of_isPrime` from `Mathlib/RingTheory/Ideal/GoingUp.lean` to chains of arbitrary length. This was previously an explicitly marked `TODO`.
1 parent c2ea7ca commit 8c79cb4

3 files changed

Lines changed: 135 additions & 2 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6667,6 +6667,7 @@ public import Mathlib.RingTheory.Ideal.Defs
66676667
public import Mathlib.RingTheory.Ideal.Finsupp
66686668
public import Mathlib.RingTheory.Ideal.GoingDown
66696669
public import Mathlib.RingTheory.Ideal.GoingUp
6670+
public import Mathlib.RingTheory.Ideal.HasGoingUp
66706671
public import Mathlib.RingTheory.Ideal.Height
66716672
public import Mathlib.RingTheory.Ideal.IdempotentFG
66726673
public import Mathlib.RingTheory.Ideal.Int

‎Mathlib/RingTheory/Ideal/GoingUp.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,7 @@ theorem exists_ideal_over_prime_of_isIntegral_of_isDomain [Algebra.IsIntegral R
303303
end
304304

305305
/-- More general going-up theorem than `exists_ideal_over_prime_of_isIntegral_of_isDomain`.
306-
TODO: Version of going-up theorem with arbitrary length chains (by induction on this)?
307-
Not sure how best to write an ascending chain in Lean -/
306+
Generalized to arbitrary length chains in `Ideal.exists_ltSeries_of_hasGoingUp`. -/
308307
theorem exists_ideal_over_prime_of_isIntegral_of_isPrime
309308
[Algebra.IsIntegral R S] (P : Ideal R) [IsPrime P]
310309
(I : Ideal S) [IsPrime I] (hIP : I.comap (algebraMap R S) ≤ P) :

‎Mathlib/RingTheory/Ideal/HasGoingUp.lean‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
/-
2+
Copyright (c) 2026 Robert Shlyakhtenko. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Robert Shlyakhtenko
5+
-/
6+
7+
module
8+
9+
public import Mathlib.RingTheory.Spectrum.Prime.Topology
10+
11+
/-!
12+
# Going up
13+
14+
In this file we define a predicate `Algebra.HasGoingUp`: An `R`-algebra `S` satisfies
15+
`Algebra.HasGoingUp R S` if for every pair of prime ideals `p ≤ q` of `R` with
16+
`P` a prime of `S` lying above `p`, there exists a prime `P ≤ Q` of `S` lying above `q`.
17+
18+
This file closely mirrors `Mathlib.RingTheory.Ideal.GoingDown`.
19+
20+
## Main results
21+
22+
- `Algebra.HasGoingUp.iff_specializingMap_primeSpectrumComap`: going up is equivalent
23+
to specializations lifting along `Spec S → Spec R`.
24+
- `Algebra.HasGoingUp.of_isIntegral`: integral algebras satisfy going up.
25+
-/
26+
27+
@[expose] public section
28+
29+
/--
30+
An `R`-algebra `S` satisfies `Algebra.HasGoingUp R S` if for every pair of
31+
prime ideals `p ≤ q` of `R` with `P` a prime of `S` lying above `p`, there exists a
32+
prime `P ≤ Q` of `S` lying above `q`.
33+
34+
The condition only asks for `<` which is easier to prove, use
35+
`Ideal.exists_ideal_ge_liesOver_of_le` for applying it. -/
36+
@[stacks 00HV "(1)"]
37+
class Algebra.HasGoingUp
38+
(R S : Type*) [CommRing R] [CommRing S] [Algebra R S] : Prop where
39+
exists_ideal_ge_liesOver_of_lt {q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] :
40+
P.under R < q → ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
41+
42+
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
43+
44+
namespace Ideal
45+
46+
lemma exists_ideal_ge_liesOver_of_le [Algebra.HasGoingUp R S]
47+
{p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p]
48+
(hle : p ≤ q) :
49+
∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q := by
50+
rcases eq_or_ne p q with rfl | h
51+
· use P
52+
· rw [P.over_def p] at hle h
53+
exact Algebra.HasGoingUp.exists_ideal_ge_liesOver_of_lt P (lt_of_le_of_ne hle h)
54+
55+
lemma exists_ideal_gt_liesOver_of_lt [Algebra.HasGoingUp R S]
56+
{p q : Ideal R} [q.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p]
57+
(hpq : p < q) :
58+
∃ Q, P < Q ∧ Q.IsPrime ∧ Q.LiesOver q := by
59+
obtain ⟨Q, hPQ, hQ, hQq⟩ := P.exists_ideal_ge_liesOver_of_le (p := p) (q := q) hpq.le
60+
refine ⟨Q, lt_of_le_of_ne hPQ fun h ↦ ?_, hQ, hQq⟩
61+
subst Q
62+
simp [P.over_def p, P.over_def q] at hpq
63+
64+
/-- This generalizes `exists_ideal_over_prime_of_isIntegral_of_isPrime`
65+
to arbitrary length chains. -/
66+
lemma exists_ltSeries_of_hasGoingUp [Algebra.HasGoingUp R S]
67+
(l : LTSeries (PrimeSpectrum R))
68+
(P : Ideal S) [P.IsPrime]
69+
[lo : P.LiesOver (RelSeries.head l).asIdeal] :
70+
∃ L : LTSeries (PrimeSpectrum S),
71+
L.length = l.length ∧
72+
L.head = (⟨P, inferInstance⟩ : PrimeSpectrum S) ∧
73+
List.map (PrimeSpectrum.comap (algebraMap R S)) (L.toList) = l.toList := by
74+
induction l using RelSeries.inductionOn generalizing P with
75+
| singleton q =>
76+
refine ⟨RelSeries.singleton _ ⟨P, inferInstance⟩, rfl, rfl, ?_⟩
77+
simpa [PrimeSpectrum.ext_iff] using lo.over.symm
78+
| cons l q lt ih =>
79+
simp only [RelSeries.head_cons] at lo
80+
obtain ⟨Q, PQlt, hQ, Qlo⟩ :=
81+
Ideal.exists_ideal_gt_liesOver_of_lt P lt
82+
obtain ⟨L, len, head, spec⟩ := ih Q
83+
refine ⟨L.cons ⟨P, inferInstance⟩ (by
84+
simp_all only [Set.mem_ofPred_eq]
85+
exact PQlt), by simpa using len, rfl, ?_⟩
86+
simpa [spec, PrimeSpectrum.ext_iff] using lo.over.symm
87+
88+
end Ideal
89+
90+
namespace Algebra.HasGoingUp
91+
92+
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
93+
94+
/-- An `R`-algebra `S` has the going up property if and only if specializations lift
95+
along `Spec S → Spec R`. -/
96+
@[stacks 00HW "(2)"]
97+
lemma iff_specializingMap_primeSpectrumComap :
98+
Algebra.HasGoingUp R S ↔
99+
SpecializingMap (PrimeSpectrum.comap (algebraMap R S)) := by
100+
refine ⟨?_, fun h ↦ ⟨fun {q} hq P hP hlt ↦ ?_⟩⟩
101+
· intro h P q hq
102+
simp only [flip] at hq
103+
rw [← PrimeSpectrum.le_iff_specializes] at hq
104+
obtain ⟨Q, hle, hQ, h⟩ := P.asIdeal.exists_ideal_ge_liesOver_of_le (q := q.asIdeal)
105+
(p := P.asIdeal.under R) hq
106+
refine ⟨⟨Q, hQ⟩, (PrimeSpectrum.le_iff_specializes P _).mp hle, ?_⟩
107+
ext : 1
108+
exact h.over.symm
109+
· have : PrimeSpectrum.comap (algebraMap R S) ⟨P, hP⟩ ⤳ (⟨q, hq⟩ : PrimeSpectrum R) :=
110+
(PrimeSpectrum.le_iff_specializes _ _).mp hlt.le
111+
obtain ⟨Q, hs, heq⟩ := h this
112+
refine ⟨Q.asIdeal, (PrimeSpectrum.le_iff_specializes _ _).mpr hs, Q.2, ⟨?_⟩⟩
113+
simpa [PrimeSpectrum.ext_iff] using heq.symm
114+
115+
variable (R S) in
116+
@[stacks 00HX]
117+
lemma trans (T : Type*) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
118+
[Algebra.HasGoingUp R S] [Algebra.HasGoingUp S T] :
119+
Algebra.HasGoingUp R T := by
120+
rw [iff_specializingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
121+
simp only [PrimeSpectrum.comap_comp]
122+
apply SpecializingMap.comp
123+
· rwa [← iff_specializingMap_primeSpectrumComap]
124+
· rwa [← iff_specializingMap_primeSpectrumComap]
125+
126+
/-- Integral algebras satisfy the going up property. -/
127+
@[stacks 00GU]
128+
instance of_isIntegral [Algebra.IsIntegral R S] : Algebra.HasGoingUp R S where
129+
exists_ideal_ge_liesOver_of_lt {q} _ P _ hPq :=
130+
let ⟨Q, hPQ, hQ, hQq⟩ := Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime q P hPq.le
131+
⟨Q, hPQ, hQ, ⟨hQq.symm⟩⟩
132+
133+
end Algebra.HasGoingUp

0 commit comments

Comments
 (0)