Filtered multiples in a two-equation ideal

The intersection of the bounded-degree multiples of two coprime equations consists exactly of bounded-degree multiples of their product.

noncomputable def CCDN.filteredMultiples {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (N : ℕ) : Submodule K (MvPolynomial σ K)

Multiples of f whose multiplier has the degree allowed by cutoff N.

Equations

• CCDN.filteredMultiples f N = Submodule.map (LinearMap.mulLeft K f) (MvPolynomial.restrictTotalDegree σ K (N - f.totalDegree))

theorem CCDN.mem_filteredMultiples {K : Type u_1} {σ : Type u_2} [Field K] (f x : MvPolynomial σ K) (N : ℕ) : x ∈ filteredMultiples f N ↔ ∃ (u : MvPolynomial σ K), u.totalDegree ≤ N - f.totalDegree ∧ f * u = x

x is a filtered multiple of f at level N if and only if x = f * u with u of total degree at most N - deg f.

theorem CCDN.filteredMultiples_le_degree {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) {N : ℕ} (hN : f.totalDegree ≤ N) : filteredMultiples f N ≤ MvPolynomial.restrictTotalDegree σ K N

If deg f ≤ N, the filtered multiples of f at level N have total degree at most N.

instance CCDN.filteredMultiples_finite {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial σ K) (N : ℕ) : Module.Finite K ↥(filteredMultiples f N)

theorem CCDN.filteredMultiples_finrank {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (hf : f ≠ 0) (N : ℕ) : Module.finrank K ↥(filteredMultiples f N) = Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K (N - f.totalDegree))

For f ≠ 0, the space of filtered multiples of f at level N has the dimension of the space of polynomials of total degree at most N - deg f.

theorem CCDN.finrank_map_add_kernel_subspace_le {K : Type u_1} {M : Type u_2} {W : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup W] [Module K W] (φ : M →ₗ[K] W) (V U : Submodule K M) [Module.Finite K ↥V] (hUV : U ≤ V) (hUker : U ≤ φ.ker) : Module.finrank K ↥(Submodule.map φ V) + Module.finrank K ↥U ≤ Module.finrank K ↥V

A subspace known to lie in a linear map's kernel subtracts from the image dimension.

noncomputable def CCDN.filteredCoordinateSpace {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (N : ℕ) : Submodule K (MvPolynomial σ K ⧸ I)

Bounded-degree polynomials in the quotient coordinate ring: the image in K[X] ⧸ I of the polynomials of total degree at most N. For K = ℚ its dimension is CCDN.affineHilbertFunction I N.

Equations

• CCDN.filteredCoordinateSpace I N = Submodule.map (Ideal.Quotient.mkₐ K I).toLinearMap (MvPolynomial.restrictTotalDegree σ K N)

instance CCDN.filteredCoordinateSpace_finite {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) (N : ℕ) : Module.Finite K ↥(filteredCoordinateSpace I N)

def CCDN.HasFilteredCurveDegree {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (d : ℕ) : Prop

Curve degree via the filtered Hilbert function: the dimension of the bounded-degree part of the coordinate ring is eventually d * M + c. Over ℚ with σ = Fin n this is CCDN.HasAffineCurveDegree.

Equations

• CCDN.HasFilteredCurveDegree I d = ∃ (N : ℕ) (c : ℤ), ∀ M ≥ N, ↑(Module.finrank K ↥(CCDN.filteredCoordinateSpace I M)) = ↑d * ↑M + c

theorem CCDN.HasFilteredCurveDegree.le_mul_of_growth {K : Type u_1} {σ : Type u_2} [Field K] {I : Ideal (MvPolynomial σ K)} {d r m D : ℕ} (hdegree : HasFilteredCurveDegree I d) (hm : 0 < m) (hlower : ∀ (N : ℕ), r * (N + 1) ≤ Module.finrank K ↥(filteredCoordinateSpace I (D + m * N))) : r ≤ d * m

A lower bound along positive-step filtered pieces cannot grow faster than the curve's eventual linear Hilbert function.

theorem CCDN.filteredCoordinateSpace_finrank_bound {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] {f g : MvPolynomial σ K} (hf : Prime f) (hfg : ¬f ∣ g) (I : Ideal (MvPolynomial σ K)) (hIf : f ∈ I) (hIg : g ∈ I) {N : ℕ} (hN : f.totalDegree + g.totalDegree ≤ N) : Module.finrank K ↥(filteredCoordinateSpace I N) + Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K (N - f.totalDegree)) + Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K (N - g.totalDegree)) ≤ Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K N) + Module.finrank K ↥(MvPolynomial.restrictTotalDegree σ K (N - (f.totalDegree + g.totalDegree)))

The filtered Koszul rank bound, before evaluating the monomial-space dimensions. It applies to every ideal containing the two equations.

theorem CCDN.exists_filtered_polynomial_basis {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) (D : ℕ) : ∃ (h : Fin (Module.finrank K ↥(filteredCoordinateSpace I D)) → MvPolynomial σ K), (∀ (i : Fin (Module.finrank K ↥(filteredCoordinateSpace I D))), (h i).totalDegree ≤ D) ∧ LinearIndependent K fun (i : Fin (Module.finrank K ↥(filteredCoordinateSpace I D))) => (Ideal.Quotient.mkₐ K I) (h i)

Lift a basis of the filtered coordinate ring to bounded-degree polynomials.

theorem CCDN.filteredCoordinateSpace_finrank_antitone_ideal {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I J : Ideal (MvPolynomial σ K)) (hIJ : I ≤ J) (N : ℕ) : Module.finrank K ↥(filteredCoordinateSpace J N) ≤ Module.finrank K ↥(filteredCoordinateSpace I N)

Enlarging the ideal can only shrink the filtered pieces of the coordinate ring.