Matrix minors and characteristic coefficients

The minor ideals of the range of a matrix are generated by all square submatrix determinants, allowing independent row and column choices. Each coefficient of det (1 - X A) belongs to the corresponding minor ideal. Consequently, computing the latter in Smith bases bounds the characteristic coefficients without confusing principal minors with all minors. This is the algebraic input to the lattice Hodge–Newton inequality.

References

• K. S. Kedlaya, A little p-adic numerical analysis, §3, Theorem 16.

theorem Matrix.det_submatrix_mem_minorsIdeal_range {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommRing R] [Fintype n] (A : Matrix m n R) {p : ℕ} (r : Fin p → m) (c : Fin p → n) : (A.submatrix r c).det ∈ A.mulVecLin.range.minorsIdeal p

Every square submatrix determinant belongs to the corresponding minor ideal of the range. Row and column selections are independent and may repeat indices.

theorem Matrix.minorsIdeal_range_eq_span_det_submatrix {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommRing R] [Fintype n] [Finite m] (A : Matrix m n R) (p : ℕ) : A.mulVecLin.range.minorsIdeal p = Ideal.span (Set.range fun (rc : (Fin p → m) × (Fin p → n)) => (A.submatrix rc.1 rc.2).det)

The size-p minor ideal of a matrix range is generated by all size-p submatrix determinants, not merely by principal minors. Repeated indices contribute zero.

theorem Matrix.coeff_charpolyRev_mem_minorsIdeal_range {R : Type u_1} {n : Type u_3} [CommRing R] [Fintype n] [DecidableEq n] (A : Matrix n n R) (p : ℕ) : A.charpolyRev.coeff p ∈ A.mulVecLin.range.minorsIdeal p

The coefficient of X^p in det (1 - X A) belongs to the ideal of size-p minors of the range. This includes the constant term and coefficients beyond the dimension.