Finite minimal-prime components and their filtered dimension budget. The component family and zero-set cover are constructed here; eventual linearity of their Hilbert functions is a separate hypothesis.

noncomputable def CCDN.minimalPrimeComponents {R : Type u_1} [CommRing R] [IsNoetherianRing R] (I : Ideal R) : Finset (Ideal R)

The finite set of minimal primes over an ideal I of a Noetherian ring.

Equations

• CCDN.minimalPrimeComponents I = ⋯.toFinset

@[simp]

theorem CCDN.mem_minimalPrimeComponents {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I P : Ideal R} : P ∈ minimalPrimeComponents I ↔ I.IsMinimalPrime P

P belongs to minimalPrimeComponents I exactly when it is a minimal prime over I.

theorem CCDN.minimalPrimeComponents_isPrime {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I P : Ideal R} (hP : P ∈ minimalPrimeComponents I) : P.IsPrime

Every member of minimalPrimeComponents I is a prime ideal.

theorem CCDN.le_minimalPrimeComponents {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I P : Ideal R} (hP : P ∈ minimalPrimeComponents I) : I ≤ P

Every member of minimalPrimeComponents I contains I.

theorem CCDN.minimalPrimeComponents_eq_of_le {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I P Q : Ideal R} (hP : P ∈ minimalPrimeComponents I) (hQ : Q ∈ minimalPrimeComponents I) (hPQ : P ≤ Q) : P = Q

Two members of minimalPrimeComponents I that are comparable are equal.

theorem CCDN.idealZeroLocus_eq_union_minimalPrimeComponents {n : ℕ} (I : Ideal (CoordinatePolynomial n)) : idealZeroLocus I = ⋃ P ∈ minimalPrimeComponents I, idealZeroLocus P

The finite family is the minimal-prime decomposition, and its rational zero sets cover exactly the original zero set.

theorem CCDN.exists_prime_component_separators {R : Type u_1} {ι : Type u_2} [CommRing R] [Finite ι] (P : ι → Ideal R) (hprime : ∀ (i : ι), (P i).IsPrime) (hanti : ∀ (i j : ι), P i ≤ P j → i = j) : ∃ (a : ι → R), (∀ (i : ι), a i ∉ P i) ∧ ∀ (i j : ι), i ≠ j → a i ∈ P j

Separators for any finite family of incomparable prime ideals.

noncomputable def CCDN.polynomialSectionIdeal {K : Type u_1} {σ : Type u_2} [Field K] (f g : MvPolynomial σ K) : Ideal (MvPolynomial σ K)

The ideal generated by the two equations of an auxiliary section.

Equations

• CCDN.polynomialSectionIdeal f g = Ideal.span {f, g}

theorem CCDN.polynomialSectionIdeal_first_mem {K : Type u_1} {σ : Type u_2} [Field K] (f g : MvPolynomial σ K) : f ∈ polynomialSectionIdeal f g

The first equation f lies in polynomialSectionIdeal f g.

theorem CCDN.polynomialSectionIdeal_second_mem {K : Type u_1} {σ : Type u_2} [Field K] (f g : MvPolynomial σ K) : g ∈ polynomialSectionIdeal f g

The second equation g lies in polynomialSectionIdeal f g.

theorem CCDN.idealZeroLocus_polynomialSectionIdeal {n : ℕ} (f g : CoordinatePolynomial n) : idealZeroLocus (polynomialSectionIdeal f g) = zeroLocus f ∩ zeroLocus g

The zero locus of the ideal (f, g) is the intersection of the zero loci of f and g.