Homogeneity survives coefficient extension and passage to minimal-prime components. The latter uses the prime homogeneous core.

theorem CCDN.polynomialCoefficientLinear_homogeneousComponent {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {n : ℕ} (φ : K →ₗ[k] k) (N : ℕ) (f : MvPolynomial (Fin n) K) : (polynomialCoefficientLinear φ) ((MvPolynomial.homogeneousComponent N) f) = (MvPolynomial.homogeneousComponent N) ((polynomialCoefficientLinear φ) f)

Applying a linear map to the coefficients commutes with taking homogeneous components.

theorem CCDN.homogeneous_ideal_scalar_extension {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (hI : IsHomogeneousIdeal I) (f : MvPolynomial (Fin n) L) : f ∈ Ideal.map (MvPolynomial.map (algebraMap K L)) I → ∀ (N : ℕ), (MvPolynomial.homogeneousComponent N) f ∈ Ideal.map (MvPolynomial.map (algebraMap K L)) I

The extension of scalars of a homogeneous ideal is homogeneous.

theorem CCDN.minimal_prime_ideal_homogeneous {K : Type u_1} {σ : Type u_2} [Field K] (I : Ideal (MvPolynomial σ K)) (hI : IsHomogeneousIdeal I) (P : Ideal (MvPolynomial σ K)) (hP : P ∈ I.minimalPrimes) : IsHomogeneousIdeal P

Every minimal prime over a homogeneous ideal is homogeneous.