The principal equation of the image of a homogeneous linear projection is homogeneous.

theorem CCDN.projection_kernel_homogeneousComponent_mem {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] (I : Ideal (MvPolynomial τ K)) (hI : IsHomogeneousIdeal I) (a : σ → MvPolynomial τ K) (ha : ∀ (i : σ), (a i).IsHomogeneous 1) (p : MvPolynomial σ K) (hp : p ∈ RingHom.ker (projectionCoordinateMap I a)) (N : ℕ) : (MvPolynomial.homogeneousComponent N) p ∈ RingHom.ker (projectionCoordinateMap I a)

For a homogeneous ideal I and homogeneous linear forms a, the kernel of the projection by a is closed under taking homogeneous components.

theorem CCDN.principal_generator_isHomogeneous {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (hI : IsHomogeneousIdeal I) (f : MvPolynomial σ K) (hf : f ≠ 0) (hgen : I = Ideal.span {f}) : f.IsHomogeneous f.totalDegree

A nonzero generator of a principal ideal that is closed under homogeneous components is homogeneous of its total degree.

theorem CCDN.homogeneous_projection_equation {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] (I : Ideal (MvPolynomial τ K)) (hI : IsHomogeneousIdeal I) (a : σ → MvPolynomial τ K) (ha : ∀ (i : σ), (a i).IsHomogeneous 1) (f : MvPolynomial σ K) (hf : f ≠ 0) (hgen : RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}) : f.IsHomogeneous f.totalDegree

If the kernel of the projection of a homogeneous ideal by homogeneous linear forms is generated by a nonzero polynomial f, then f is homogeneous of its total degree.