Documentation

LeanPool.CCDN.Hilbert.RecurrenceParameterTranscendence

Positive Hilbert growth forces any parameter generating the eventual filtration recurrence to be transcendental.

theorem CCDN.recurrence_parameter_transcendental {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) (d : ℕ) (hd : 0 < d) (hdegree : HasFilteredCurveDegree I d) (l : MvPolynomial σ K) (N : ℕ) (hrec : ∀ m ≥ N, filteredCoordinateSpace I (m + 1) = filteredCoordinateSpace I m ⊔ Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk I) l)) (filteredCoordinateSpace I m)) :

A parameter giving eventual filtered generation on a positive-degree curve cannot satisfy a polynomial over the ground field.