theorem
affine_intersection_component_codim_bound
{R : Type u_1}
[CommRing R]
[IsNoetherianRing R]
{s t : Finset R}
{𝔴 : Ideal R}
(hmin : 𝔴 ∈ (Ideal.span ↑(s ∪ t)).minimalPrimes)
:
Affine codimension bound for intersection components: a minimal prime over the span
of s ∪ t in a Noetherian ring has height at most |s| + |t|.
theorem
projective_cone_intersection
{k : Type u_1}
[Field k]
{n : ℕ}
{𝔭 𝔮 : Ideal (MvPolynomial (Fin (n + 1)) k)}
(hp : 𝔭 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1)))
(hq : 𝔮 ≤ MvPolynomial.variablesIdeal k (Fin (n + 1)))
:
Two projective cones in 𝔸^{n+1} (ideals contained in the irrelevant ideal) have
nontrivial intersection: their sum is not the unit ideal.