Going down #
In this file we define a predicate Algebra.HasGoingDown
: An R
-algebra S
satisfies
Algebra.HasGoingDown R S
if for every pair of prime ideals p ≤ q
of R
with Q
a prime
of S
lying above q
, there exists a prime P ≤ Q
of S
lying above p
.
Main results #
Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap
: going down is equivalent to generalizations lifting alongSpec S → Spec R
.Algebra.HasGoingDown.of_flat
: flat algebras satisfy going down.
TODOs #
- An integral extension of domains with normal base satisfies going down.
An R
-algebra S
satisfies Algebra.HasGoingDown R S
if for every pair of
prime ideals p ≤ q
of R
with Q
a prime of S
lying above q
, there exists a
prime P ≤ Q
of S
lying above p
.
The condition only asks for <
which is easier to prove, use
Ideal.exists_ideal_le_liesOver_of_le
for applying it.
Instances
theorem
Ideal.exists_ltSeries_of_hasGoingDown
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[Algebra.HasGoingDown R S]
(l : LTSeries (PrimeSpectrum R))
(P : Ideal S)
[P.IsPrime]
[lo : P.LiesOver (RelSeries.last l).asIdeal]
:
∃ (L : LTSeries (PrimeSpectrum S)),
L.length = l.length ∧ RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧ List.map (algebraMap R S).specComap (RelSeries.toList L) = RelSeries.toList l
theorem
Algebra.HasGoingDown.trans
(R : Type u_3)
(S : Type u_4)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Type u_5)
[CommRing T]
[Algebra R T]
[Algebra S T]
[IsScalarTower R S T]
[HasGoingDown R S]
[HasGoingDown S T]
:
HasGoingDown R T
theorem
Algebra.HasGoingDown.of_specComap_localRingHom_surjective
{R : Type u_3}
{S : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
(H :
∀ (P : Ideal S) [inst : P.IsPrime],
Function.Surjective (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯).specComap)
:
HasGoingDown R S
If for every prime of S
, the map Spec Sₚ → Spec Rₚ
is surjective,
the algebra satisfies going down.
instance
Algebra.HasGoingDown.of_flat
{R : Type u_3}
{S : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
[Module.Flat R S]
:
HasGoingDown R S
Flat algebras satisfy the going down property.