theorem serre_dimension_inequality (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] : ringKrullDim (R ⧸ 𝔭) + ringKrullDim (R ⧸ 𝔮) ≤ ringKrullDim R + ringKrullDim (R ⧸ 𝔭 ⊔ 𝔮)

Serre's dimension inequality: for a Noetherian local ring R and primes 𝔭, 𝔮, dim(R/𝔭) + dim(R/𝔮) ≤ dim R + dim(R/(𝔭 ⊔ 𝔮)).

class HasSerreDimensionInequality (R : Type u_1) [CommRing R] [IsLocalRing R] : Prop

Typeclass abstracting Serre's dimension inequality for a local ring, allowing downstream lemmas to be stated under a single hypothesis.

• dim_ineq {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] : ringKrullDim (R ⧸ 𝔭) + ringKrullDim (R ⧸ 𝔮) ≤ ringKrullDim R + ringKrullDim (R ⧸ 𝔭 ⊔ 𝔮)

instance instHasSerreDimensionInequalityNoetherian (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : HasSerreDimensionInequality R

Every Noetherian local ring satisfies Serre's dimension inequality.

theorem ringKrullDim_quotient_top (R : Type u_1) [CommRing R] : ringKrullDim (R ⧸ ⊤) = ⊥

The Krull dimension of the trivial quotient R / ⊤ is ⊥.

theorem sup_ne_top_of_dim_inequality {R : Type u_1} [CommRing R] {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] (hdim : ringKrullDim (R ⧸ 𝔭) + ringKrullDim (R ⧸ 𝔮) ≤ ringKrullDim R + ringKrullDim (R ⧸ 𝔭 ⊔ 𝔮)) : 𝔭 ⊔ 𝔮 ≠ ⊤

If Serre's dimension inequality holds for two primes, then their sum is not the unit ideal — otherwise the right-hand side becomes ⊥ while the left-hand side is ≥ 0.

theorem sup_ne_top_of_serre {R : Type u_1} [CommRing R] [IsLocalRing R] [HasSerreDimensionInequality R] {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] : 𝔭 ⊔ 𝔮 ≠ ⊤

Corollary of Serre's inequality: in a local ring satisfying the inequality, the sum of two primes is never the whole ring.

theorem sum_of_primes_proper_of_height_bound {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsLocalRing R] [HasSerreDimensionInequality R] {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] (_h : ↑𝔭.height + ↑𝔮.height ≤ ringKrullDim R) : 𝔭 ⊔ 𝔮 ≠ ⊤

Variant with a height bound: under Serre's inequality, the sum of two primes whose heights bound the dimension of R is still proper.

theorem map_quotient_eq_top_of_sup_eq_top {R : Type u_1} [CommRing R] {𝔭 𝔮 : Ideal R} (h : 𝔭 ⊔ 𝔮 = ⊤) : Ideal.map (Ideal.Quotient.mk 𝔭) 𝔮 = ⊤

If 𝔭 ⊔ 𝔮 = ⊤, then 𝔮 maps to the unit ideal in R / 𝔭.

theorem ringKrullDim_quotient_eq_bot_of_sup_eq_top {R : Type u_1} [CommRing R] {I J : Ideal R} (h : I ⊔ J = ⊤) : ringKrullDim (R ⧸ I ⊔ J) = ⊥

If I ⊔ J = ⊤, then the Krull dimension of R / (I ⊔ J) is ⊥.

theorem ringKrullDim_quotient_sup_add_le {R : Type u_1} [CommRing R] [IsLocalRing R] [HasSerreDimensionInequality R] {𝔭 𝔮 : Ideal R} [𝔭.IsPrime] [𝔮.IsPrime] : ringKrullDim (R ⧸ 𝔭) + ringKrullDim (R ⧸ 𝔮) ≤ ringKrullDim R + ringKrullDim (R ⧸ 𝔭 ⊔ 𝔮)

Restatement of Serre's inequality via the typeclass HasSerreDimensionInequality.

noncomputable def MvPolynomial.variablesIdeal (k : Type u_1) [CommSemiring k] (σ : Type u_2) : Ideal (MvPolynomial σ k)

The irrelevant ideal of a polynomial ring: the ideal generated by all variables X_i.

theorem MvPolynomial.X_mem_variablesIdeal {k : Type u_1} [CommSemiring k] {σ : Type u_2} (i : σ) : X i ∈ variablesIdeal k σ

Each variable X_i lies in the irrelevant ideal.

theorem MvPolynomial.variablesIdeal_le_ker_eval_zero {k : Type u_1} [CommSemiring k] {σ : Type u_2} : variablesIdeal k σ ≤ RingHom.ker (eval 0)

The irrelevant ideal is contained in the kernel of evaluation at the origin.

theorem MvPolynomial.variablesIdeal_ne_top (k : Type u_1) [CommSemiring k] [Nontrivial k] (σ : Type u_2) : variablesIdeal k σ ≠ ⊤

The irrelevant ideal is proper (does not contain 1).

theorem MvPolynomial.span_singleton_X_le_variablesIdeal {k : Type u_1} [CommSemiring k] {σ : Type u_2} (i : σ) : Ideal.span {X i} ≤ variablesIdeal k σ

The singleton ideal (X_i) is contained in the irrelevant ideal.

theorem MvPolynomial.sup_ne_top_of_le_variablesIdeal {k : Type u_1} [Field k] {σ : Type u_2} {𝔭 𝔮 : Ideal (MvPolynomial σ k)} (hp : 𝔭 ≤ variablesIdeal k σ) (hq : 𝔮 ≤ variablesIdeal k σ) : 𝔭 ⊔ 𝔮 ≠ ⊤

The sum of two ideals contained in the irrelevant ideal remains proper.

theorem MvPolynomial.iSup_ne_top_of_le_variablesIdeal {k : Type u_1} [Field k] {σ : Type u_2} {ι : Type u_3} {𝔭 : ι → Ideal (MvPolynomial σ k)} (h : ∀ (i : ι), 𝔭 i ≤ variablesIdeal k σ) : iSup 𝔭 ≠ ⊤

An indexed supremum of ideals contained in the irrelevant ideal remains proper.

theorem lines_meet_in_P2 (k : Type u_1) [Field k] : Ideal.span {MvPolynomial.X 0} ⊔ Ideal.span {MvPolynomial.X 1} ≠ ⊤

Example: two distinct lines in P^2 (cut out by X_0 and X_1) intersect.

theorem line_and_conic_meet_in_P2 (k : Type u_1) [Field k] : Ideal.span {MvPolynomial.X 0} ⊔ Ideal.span {MvPolynomial.X 1 * MvPolynomial.X 1 - MvPolynomial.X 0 * MvPolynomial.X 2} ≠ ⊤

Example: a line and a conic in P^2 meet, since both ideals lie in the irrelevant ideal.

theorem planes_meet_in_P4 (k : Type u_1) [Field k] : Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1} ⊔ Ideal.span {MvPolynomial.X 2, MvPolynomial.X 3} ≠ ⊤

Example: two planes in P^4 meet, since both ideals lie in the irrelevant ideal.

theorem Ideal.sup_ne_top_of_le_proper {R : Type u_1} [CommRing R] {𝔭 𝔮 𝔪 : Ideal R} (hp : 𝔭 ≤ 𝔪) (hq : 𝔮 ≤ 𝔪) (hm : 𝔪 ≠ ⊤) : 𝔭 ⊔ 𝔮 ≠ ⊤

General principle: the sum of two ideals contained in a proper ideal is proper.

theorem Ideal.iSup_ne_top_of_le_proper {R : Type u_1} [CommRing R] {ι : Type u_2} {𝔭 : ι → Ideal R} {𝔪 : Ideal R} (h : ∀ (i : ι), 𝔭 i ≤ 𝔪) (hm : 𝔪 ≠ ⊤) : iSup 𝔭 ≠ ⊤

General principle: an indexed supremum of ideals contained in a proper ideal is proper.