theorem withbot_enat_le_of_nat_bound {a d : ℕ} {c : WithBot ℕ∞} (h : ↑a ≤ ↑d + c) (hgt : d + 1 < a) : 2 ≤ c

Arithmetic helper in WithBot ℕ∞: if a ≤ d + c and d + 1 < a, then 2 ≤ c.

theorem withbot_enat_codim_bound {dimX dimY n : ℕ} {c : WithBot ℕ∞} (h : ↑(dimX + 1 + (dimY + 1)) ≤ ↑(n + 1) + c) (hdim_le : n ≤ dimX + dimY) : ↑(dimX + dimY - n + 1) ≤ c

Codimension bound helper: from dim X + 1 + (dim Y + 1) ≤ (n+1) + c and n ≤ dim X + dim Y, deduce dim X + dim Y − n + 1 ≤ c.

theorem ringKrullDim_mvPolynomial_fin_succ (k : Type u_1) [Field k] (n : ℕ) : ringKrullDim (MvPolynomial (Fin (n + 1)) k) = ↑(n + 1)

The Krull dimension of the polynomial ring in n+1 variables over a field equals n+1.

theorem ne_top_of_ringKrullDim_quotient_ge_two {R : Type u_1} [CommRing R] {I : Ideal R} (h : 2 ≤ ringKrullDim (R ⧸ I)) : I ≠ ⊤

If the quotient R / I has Krull dimension at least 2, then I is not the whole ring.

theorem projective_codim_bound {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 dimension inequality used to derive projective codimension bounds.

theorem projective_intersection_nonempty_of_dim_condition {k : Type u_1} [Field k] (n dimX dimY : ℕ) {𝔭 𝔮 : Ideal (MvPolynomial (Fin (n + 1)) k)} [𝔭.IsPrime] [𝔮.IsPrime] (_hp_le : 𝔭 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (_hq_le : 𝔮 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hconeX : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) = ↑(dimX + 1)) (hconeY : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) = ↑(dimY + 1)) (hserre : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)) (hdim : n < dimX + dimY) : 2 ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)

Theorem 8.2 (intersection dimension): if dim X + dim Y > n in P^n, then the intersection of their cones has dimension at least 2 (so the projective varieties meet).

theorem projective_intersection_sup_ne_top_of_dim {k : Type u_1} [Field k] (n dimX dimY : ℕ) {𝔭 𝔮 : Ideal (MvPolynomial (Fin (n + 1)) k)} [𝔭.IsPrime] [𝔮.IsPrime] (hp_le : 𝔭 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hq_le : 𝔮 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hconeX : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) = ↑(dimX + 1)) (hconeY : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) = ↑(dimY + 1)) (hserre : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)) (hdim : n < dimX + dimY) : 𝔭 ⊔ 𝔮 ≠ ⊤

Consequence: under the dimension hypothesis n < dim X + dim Y, the sum of the two projective ideals is proper.

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

Trivial nonemptiness: two cones in affine space always contain the origin, so their ideal sum is proper whenever both lie in the irrelevant ideal.

theorem goal76_projective_codim_bound {k : Type u_1} [Field k] (n dimX dimY : ℕ) {𝔭 𝔮 : Ideal (MvPolynomial (Fin (n + 1)) k)} [𝔭.IsPrime] [𝔮.IsPrime] (_hp_le : 𝔭 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (_hq_le : 𝔮 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hconeX : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) = ↑(dimX + 1)) (hconeY : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) = ↑(dimY + 1)) (hserre : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)) (hdim : n ≤ dimX + dimY) : ↑(dimX + dimY - n + 1) ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)

Codimension bound (Goal 76): under the Serre inequality, the intersection of two projective varieties in P^n of dimensions dim X, dim Y has dimension at least dim X + dim Y − n.

theorem goal76_projective_intersection_nonempty {k : Type u_1} [Field k] (n dimX dimY : ℕ) {𝔭 𝔮 : Ideal (MvPolynomial (Fin (n + 1)) k)} [𝔭.IsPrime] [𝔮.IsPrime] (hp_le : 𝔭 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hq_le : 𝔮 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1))) (hconeX : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) = ↑(dimX + 1)) (hconeY : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) = ↑(dimY + 1)) (hserre : ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔮) ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) k) + ringKrullDim (MvPolynomial (Fin (n + 1)) k ⧸ 𝔭 ⊔ 𝔮)) (hdim : n < dimX + dimY) : 𝔭 ⊔ 𝔮 ≠ ⊤

Nonemptiness (Goal 76, Thm 8.2): two projective varieties of dimensions dim X, dim Y in P^n with dim X + dim Y > n necessarily intersect.