A nonzero integer minor of the closed-form coefficient matrix. Rank drop after reduction forces divisibility of this same integer. The geometric rank-drop criterion and the height bound are separate obligations.
theorem
CCDN.closedForm_minor_map
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(φ : R →+* S)
(d r : ℕ)
(f : Polynomial (Polynomial R))
(a : Fin r → ℕ × ℕ)
(c : Fin r → ClosedFormColumns d)
:
φ ((closedFormCoefficientMatrix d f).submatrix a c).det = ((closedFormCoefficientMatrix d ((bivariateMap φ) f)).submatrix a c).det
Determinants of selected coefficient minors commute with any coefficient ring map.
theorem
CCDN.characteristic_dvd_closedForm_minor_of_rank_lt
{K : Type u_1}
[Field K]
(p : ℕ)
[CharP K p]
(d r : ℕ)
(f : Polynomial (Polynomial ℤ))
(a : Fin r → ℕ × ℕ)
(c : Fin r → ClosedFormColumns d)
(hr : (closedFormCoefficientMatrix d ((bivariateMap (Int.castRingHom K)) f)).rank < r)
:
Any characteristic-p rank drop below the chosen minor order makes p divide its integer determinant. The field may be an algebraic closure.