A linear homogeneous projection of a homogeneous quotient is strict for the total-degree filtration: any image element of bounded degree has a preimage of the same bounded degree.

theorem CCDN.homogeneousComponent_aeval_linear {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] (a : σ → MvPolynomial τ K) (ha : ∀ (i : σ), (a i).IsHomogeneous 1) (N : ℕ) (p : MvPolynomial σ K) : (MvPolynomial.homogeneousComponent N) ((MvPolynomial.aeval a) p) = (MvPolynomial.aeval a) ((MvPolynomial.homogeneousComponent N) p)

Substituting homogeneous linear forms commutes with taking homogeneous components: the degree-N component of aeval a p is aeval a of the degree-N component of p.

theorem CCDN.homogeneous_projection_filtered_lift {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] [Finite σ] (I : Ideal (MvPolynomial τ K)) (hI : IsHomogeneousIdeal I) (a : σ → MvPolynomial τ K) (ha : ∀ (i : σ), (a i).IsHomogeneous 1) (p : MvPolynomial σ K) (N : ℕ) (hp : (projectionCoordinateMap I a) p ∈ filteredCoordinateSpace I N) : ∃ (q : MvPolynomial σ K), q.totalDegree ≤ N ∧ (projectionCoordinateMap I a) q = (projectionCoordinateMap I a) p

The projection of a homogeneous quotient by homogeneous linear forms a is strict for the total-degree filtration: if the image of p has degree at most N in the quotient by I, then it is the image of some q of total degree at most N.