Linear Noether normalization of a standard graded algebra

This file implements blueprint node A02 of the algebra backend. Throughout, Q := MvPolynomial (Fin n) K is the polynomial ring in n variables over a field K, 𝔪ₙ := idealOfVars (Fin n) K is the ideal generated by the variables, and J is a homogeneous ideal of Q with respect to the standard grading homogeneousSubmodule (Fin n) K.

Main declarations

• exists_linear_normalization: for K infinite and J ≠ ⊤ homogeneous, there are quotDim J linear forms y i such that MvPolynomial.aeval (mk J ∘ y) is injective and 𝔪ₙ ^ N ≤ J ⊔ span (range y) for some N.
• exists_eq_add_sum_mul_of_pow_idealOfVars_le (graded refinement of 𝔪ₙ ^ N ≤ J ⊔ (y)): every form F of degree t ≥ N is G + ∑ i, y i * H i with G ∈ J and H i forms of degree t - 1.
• span_image_mk_eq_top_of_pow_idealOfVars_le, finite_of_pow_idealOfVars_le', finite_of_pow_idealOfVars_le: graded Nakayama / module-finiteness of Q ⧸ J over MvPolynomial (Fin s) K acting through y, with the explicit generating set of classes of forms of degree < N.

Sub-lemmas (blueprint A02.a–A02.h)

• A02.a exists_linear_form_notMem: a linear form outside finitely many ideals not containing 𝔪ₙ.
• A02.b le_idealOfVars_of_isHomogeneous_of_ne_top, quotDim_idealOfVars, eq_idealOfVars_of_quotDim_eq_zero.
• A02.c IsHomogeneous.minimalPrimes_isHomogeneous: minimal primes of a homogeneous ideal are homogeneous (in any graded ring).
• A02.d quotDim_sup_span_singleton_lt: adding a linear form avoiding the minimal primes other than 𝔪ₙ drops quotDim.
• A02.e exists_linear_forms_quotDim_sup_eq_zero: iterating A02.d.
• A02.f pow_idealOfVars_le_of_quotDim_eq_zero: quotDim J = 0 gives 𝔪ₙ ^ N ≤ J.
• A02.g aeval_injective_of_pow_idealOfVars_le: injectivity from dimension counting.
• A02.h the finiteness statements above.

Conventions

Mathlib's graded-ring structure on MvPolynomial is a local instance (attribute [local instance] MvPolynomial.gradedAlgebra); statements mention the grading explicitly as homogeneousSubmodule (Fin n) K. The algebra structure of Q ⧸ J over MvPolynomial (Fin s) K is never a global instance: the finiteness theorems take it either as an instance argument together with the hypothesis algebraMap _ _ = (MvPolynomial.aeval fun i ↦ Ideal.Quotient.mk J (y i)).toRingHom (finite_of_pow_idealOfVars_le'), or install it with letI in the statement (finite_of_pow_idealOfVars_le).

A02.c: minimal primes of a homogeneous ideal are homogeneous (general graded rings)

theorem Nikodym.LowerBound.IsHomogeneous.minimalPrimes_isHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [AddCommMonoid ι] [LinearOrder ι] [IsOrderedCancelAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] {J : Ideal A} (hJ : Ideal.IsHomogeneous 𝒜 J) {q : Ideal A} (hq : q ∈ J.minimalPrimes) : Ideal.IsHomogeneous 𝒜 q

Blueprint A02.c: the minimal primes of a homogeneous ideal are homogeneous. For q ∈ J.minimalPrimes, the homogeneous core of q is a prime containing J and contained in q, hence equal to q by minimality.

Homogeneous components of products with a form

theorem Nikodym.LowerBound.IsHomogeneous.mem_pow_idealOfVars {σ : Type u_1} {R : Type u_2} [CommSemiring R] {F : MvPolynomial σ R} {t : ℕ} (hF : F.IsHomogeneous t) : F ∈ MvPolynomial.idealOfVars σ R ^ t

Blueprint A02.h, auxiliary: a form of degree t lies in 𝔪 ^ t.

theorem Nikodym.LowerBound.homogeneousComponent_mul_of_isHomogeneous_right {σ : Type u_1} {R : Type u_2} [CommSemiring R] {y : MvPolynomial σ R} {e : ℕ} (hy : y.IsHomogeneous e) (c : MvPolynomial σ R) (m : ℕ) : (MvPolynomial.homogeneousComponent (m + e)) (c * y) = (MvPolynomial.homogeneousComponent m) c * y

Blueprint A02.h, auxiliary: the degree-(m + e) component of c * y, for a form y of degree e, is (c)_m * y.

The polynomial ring in n variables

@[instance_reducible]

noncomputable def Nikodym.LowerBound.normalizationPolynomialQuotientSMul {K : Type u_1} [Field K] {k : ℕ} (J : Ideal (MvPolynomial (Fin k) K)) (S : Type u_2) [CommSemiring S] [Algebra S (MvPolynomial (Fin k) K ⧸ J)] : SMul S (MvPolynomial (Fin k) K ⧸ J)

Use the specified algebra scalar action without searching quotient module structures.

Equations

• Nikodym.LowerBound.normalizationPolynomialQuotientSMul J S = inst✝.toSMul

@[instance_reducible]

noncomputable def Nikodym.LowerBound.normalizationPolynomialQuotientModule {K : Type u_1} [Field K] {k : ℕ} (J : Ideal (MvPolynomial (Fin k) K)) (S : Type u_2) [CommSemiring S] [Algebra S (MvPolynomial (Fin k) K ⧸ J)] : Module S (MvPolynomial (Fin k) K ⧸ J)

Use the given algebra action directly on a polynomial quotient.

Equations

• Nikodym.LowerBound.normalizationPolynomialQuotientModule J S = Algebra.toModule

A02.b: proper homogeneous ideals lie in 𝔪ₙ

theorem Nikodym.LowerBound.idealOfVars_isPrime {K : Type u_1} [Field K] {n : ℕ} : (MvPolynomial.idealOfVars (Fin n) K).IsPrime

Blueprint A02.b: 𝔪ₙ is a prime ideal.

theorem Nikodym.LowerBound.quotDim_idealOfVars {K : Type u_1} [Field K] {n : ℕ} : quotDim (MvPolynomial.idealOfVars (Fin n) K) = 0

Blueprint A02.b: quotDim 𝔪ₙ = 0.

theorem Nikodym.LowerBound.le_idealOfVars_of_isHomogeneous_of_ne_top {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) : J ≤ MvPolynomial.idealOfVars (Fin n) K

Blueprint A02.b: a proper homogeneous ideal is contained in 𝔪ₙ: the degree-0 component of any element is a constant lying in the ideal, hence zero.

theorem Nikodym.LowerBound.eq_idealOfVars_of_quotDim_eq_zero {K : Type u_1} [Field K] {n : ℕ} {p : Ideal (MvPolynomial (Fin n) K)} [p.IsPrime] (hp : p ≤ MvPolynomial.idealOfVars (Fin n) K) (h0 : quotDim p = 0) : p = MvPolynomial.idealOfVars (Fin n) K

Blueprint A02.b: a prime p ≤ 𝔪ₙ with quotDim p = 0 equals 𝔪ₙ.

theorem Nikodym.LowerBound.isHomogeneous_span_range {K : Type u_1} [Field K] {n s : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) (Ideal.span (Set.range y))

Blueprint A02: the ideal generated by linear forms is homogeneous.

theorem Nikodym.LowerBound.sup_span_range_le_idealOfVars {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) : J ⊔ Ideal.span (Set.range y) ≤ MvPolynomial.idealOfVars (Fin n) K

Blueprint A02: for a proper homogeneous J and linear forms y, J ⊔ (y) ≤ 𝔪ₙ.

theorem Nikodym.LowerBound.sup_span_range_ne_top {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) : J ⊔ Ideal.span (Set.range y) ≠ ⊤

Blueprint A02: for a proper homogeneous J and linear forms y, J ⊔ (y) ≠ ⊤.

theorem Nikodym.LowerBound.eq_top_of_sup_span_range_eq_top {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) (h : J ⊔ Ideal.span (Set.range y) = ⊤) : J = ⊤

Blueprint A02: if J ⊔ (y) = ⊤ for a homogeneous J and linear forms y, then J = ⊤.

A02.a: prime avoidance for linear forms

theorem Nikodym.LowerBound.exists_linear_form_notMem {K : Type u_1} [Field K] {n : ℕ} [Infinite K] {ι : Type u_2} [Finite ι] (p : ι → Ideal (MvPolynomial (Fin n) K)) (hp : ∀ (i : ι), ¬MvPolynomial.idealOfVars (Fin n) K ≤ p i) : ∃ (y : MvPolynomial (Fin n) K), y.IsHomogeneous 1 ∧ ∀ (i : ι), y ∉ p i

Blueprint A02.a: a linear form outside finitely many ideals. If none of the ideals p i (finitely many) contains 𝔪ₙ, there is a linear form outside all of them. The subspaces p i ∩ P_1 of the space P_1 of linear forms are proper, and a finite union of proper subspaces over an infinite field is not everything.

A02.f: dimension zero forces a power of 𝔪ₙ

theorem Nikodym.LowerBound.pow_idealOfVars_le_of_quotDim_eq_zero {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) (h0 : quotDim J = 0) : ∃ (N : ℕ), MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J

Blueprint A02.f: a proper homogeneous ideal of quotient dimension 0 contains a power of 𝔪ₙ. Its minimal primes are homogeneous (A02.c), proper, hence ≤ 𝔪ₙ, and of quotient dimension 0, hence = 𝔪ₙ; so its radical is 𝔪ₙ, and 𝔪ₙ is finitely generated.

A02.d, A02.e: cutting down the dimension by linear forms

theorem Nikodym.LowerBound.quotDim_sup_span_singleton_lt {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) (hpos : 1 ≤ quotDim J) {y : MvPolynomial (Fin n) K} (hy1 : y.IsHomogeneous 1) (hy : ∀ p ∈ J.minimalPrimes, p ≠ MvPolynomial.idealOfVars (Fin n) K → y ∉ p) : quotDim (J ⊔ Ideal.span {y}) < quotDim J

Blueprint A02.d: a linear form avoiding the minimal primes other than 𝔪ₙ drops the dimension. Every prime q ⊇ J + (y) contains a minimal prime p of J; either p = 𝔪ₙ = q (dimension 0), or y ∉ p, so p < q and quotDim q < quotDim p ≤ quotDim J.

theorem Nikodym.LowerBound.exists_linear_forms_quotDim_sup_eq_zero {K : Type u_1} [Field K] {n : ℕ} [Infinite K] (k : ℕ) (J : Ideal (MvPolynomial (Fin n) K)) : J ≠ ⊤ → Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J → quotDim J ≤ k → ∃ (y : Fin k → MvPolynomial (Fin n) K), (∀ (i : Fin k), (y i).IsHomogeneous 1) ∧ quotDim (J ⊔ Ideal.span (Set.range y)) = 0

Blueprint A02.e: iterating A02.d. For K infinite and J ≠ ⊤ homogeneous with quotDim J ≤ k, there are k linear forms y with quotDim (J ⊔ (y)) = 0.

A02.h: graded Nakayama

theorem Nikodym.LowerBound.exists_eq_add_sum_mul_of_pow_idealOfVars_le {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s N : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) (hN : MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)) {t : ℕ} (ht : N ≤ t) {F : MvPolynomial (Fin n) K} (hF : F.IsHomogeneous t) : ∃ (G : MvPolynomial (Fin n) K) (H : Fin s → MvPolynomial (Fin n) K), G ∈ J ∧ (∀ (i : Fin s), (H i).IsHomogeneous (t - 1)) ∧ F = G + ∑ i : Fin s, y i * H i

Blueprint A02.h (graded refinement): if 𝔪ₙ ^ N ≤ J ⊔ (y) for linear forms y, every form F of degree t ≥ N is G + ∑ i, y i * H i with G ∈ J and H i forms of degree t - 1. Write F = G₀ + ∑ i, c i * y i and take degree-t components.

theorem Nikodym.LowerBound.span_image_mk_eq_top_of_pow_idealOfVars_le {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s N : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) (hN : MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)) [Algebra (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J)] (halg : algebraMap (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J) = (MvPolynomial.aeval fun (i : Fin s) => (Ideal.Quotient.mk J) (y i)).toRingHom) : ∃ (gens : Finset (MvPolynomial (Fin n) K)), (∀ g ∈ gens, ∃ u < N, g.IsHomogeneous u) ∧ Submodule.span (MvPolynomial (Fin s) K) (⇑(Ideal.Quotient.mk J) '' ↑gens) = ⊤

Blueprint A02.h: graded Nakayama, spanning set. Let S := MvPolynomial (Fin s) K act on Q ⧸ J through X i ↦ mk J (y i) (an arbitrary algebra structure with this algebraMap). If 𝔪ₙ ^ N ≤ J ⊔ (y), then Q ⧸ J is spanned over S by the classes of finitely many forms of degree < N (the monomials of degree < N).

theorem Nikodym.LowerBound.finite_of_pow_idealOfVars_le' {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s N : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) (hN : MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)) [Algebra (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J)] (halg : algebraMap (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J) = (MvPolynomial.aeval fun (i : Fin s) => (Ideal.Quotient.mk J) (y i)).toRingHom) : Module.Finite (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J)

Blueprint A02.h: module-finiteness of Q ⧸ J over MvPolynomial (Fin s) K (acting through X i ↦ mk J (y i)) from 𝔪ₙ ^ N ≤ J ⊔ (y); version with the algebra structure as a hypothesis.

theorem Nikodym.LowerBound.finite_of_pow_idealOfVars_le {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s N : ℕ} {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) (hN : MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)) : Module.Finite (MvPolynomial (Fin s) K) (MvPolynomial (Fin n) K ⧸ J)

Blueprint A02.h: module-finiteness of Q ⧸ J over MvPolynomial (Fin s) K for the algebra structure (MvPolynomial.aeval fun i ↦ mk J (y i)).toRingHom.toAlgebra, from 𝔪ₙ ^ N ≤ J ⊔ (y).

A02.g: injectivity by dimension counting

theorem Nikodym.LowerBound.aeval_injective_of_pow_idealOfVars_le {K : Type u_1} [Field K] {n : ℕ} {J : Ideal (MvPolynomial (Fin n) K)} (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) {s : ℕ} (hs : s ≤ quotDim J) {y : Fin s → MvPolynomial (Fin n) K} (hy : ∀ (i : Fin s), (y i).IsHomogeneous 1) {N : ℕ} (hN : MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)) : Function.Injective ⇑(MvPolynomial.aeval fun (i : Fin s) => (Ideal.Quotient.mk J) (y i))

Blueprint A02.g: injectivity of the linear normalization. If 𝔪ₙ ^ N ≤ J ⊔ (y) for s linear forms y with s ≤ quotDim J, then MvPolynomial.aeval (mk J ∘ y) is injective: Q ⧸ J is finite, hence integral, over its image S ⧸ ker, so dim (S ⧸ ker) = quotDim J ≥ s; a nonzero kernel would force dim (S ⧸ ker) + 1 ≤ dim S = s.

The main theorem

theorem Nikodym.LowerBound.exists_linear_normalization {K : Type u_1} [Field K] {n : ℕ} [Infinite K] (J : Ideal (MvPolynomial (Fin n) K)) (hJ : J ≠ ⊤) (hJh : Ideal.IsHomogeneous (MvPolynomial.homogeneousSubmodule (Fin n) K) J) : ∃ (y : Fin (quotDim J) → MvPolynomial (Fin n) K), (∀ (i : Fin (quotDim J)), (y i).IsHomogeneous 1) ∧ Function.Injective ⇑(MvPolynomial.aeval fun (i : Fin (quotDim J)) => (Ideal.Quotient.mk J) (y i)) ∧ ∃ (N : ℕ), MvPolynomial.idealOfVars (Fin n) K ^ N ≤ J ⊔ Ideal.span (Set.range y)

Blueprint A02: linear Noether normalization of a standard graded algebra. For K infinite and J ≠ ⊤ a homogeneous ideal of Q = MvPolynomial (Fin n) K, there are quotDim J linear forms y i such that MvPolynomial.aeval (mk J ∘ y) : MvPolynomial (Fin (quotDim J)) K →ₐ[K] Q ⧸ J is injective and 𝔪ₙ ^ N ≤ J ⊔ span (range y) for some N (so Q ⧸ J is module-finite over the image: finite_of_pow_idealOfVars_le).