Closure-preserving integral affine projections compose.

theorem CCDN.closure_projection_integral_comp {K : Type u_1} [Field K] {l m n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (b : Fin m → MvPolynomial (Fin n) K) (hb : ∀ (i : Fin m), (b i).IsHomogeneous 1) (a : Fin l → MvPolynomial (Fin m) K) (hbintegral : (projectionCoordinateMap (projectiveClosureIdeal I) (closureProjectionCoordinates b)).IsIntegral) (haintegral : (projectionCoordinateMap (projectiveClosureIdeal (RingHom.ker (projectionCoordinateMap I b))) (closureProjectionCoordinates a)).IsIntegral) : (projectionCoordinateMap (projectiveClosureIdeal I) (closureProjectionCoordinates fun (j : Fin l) => (MvPolynomial.aeval b) (a j))).IsIntegral

Integrality of projective closure projections is stable under composition: if the closure projection of I by homogeneous linear forms b is integral, and the closure projection of the kernel of b by a is integral, then the closure projection of I by the composite forms aeval b (a j) is integral.