Matrix minors in ideals

def LatinQuarter.AllMinorsIn {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} (M : Matrix m n R) (t : ℕ) (J : Ideal R) : Prop

All minors of size t lie in J. Repeated indices are allowed; their determinants are zero.

Equations

• LatinQuarter.AllMinorsIn M t J = ∀ (r : Fin t → m) (c : Fin t → n), (M.submatrix r c).det ∈ J

theorem LatinQuarter.allMinorsIn_mul_left {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} {p : Type u_4} [Fintype n] (A : Matrix m n R) (B : Matrix n p R) {t : ℕ} {J : Ideal R} (hB : AllMinorsIn B t J) : AllMinorsIn (A * B) t J

theorem LatinQuarter.allMinorsIn_transpose {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} (M : Matrix m n R) {t : ℕ} {J : Ideal R} (hM : AllMinorsIn M t J) : AllMinorsIn M.transpose t J

theorem LatinQuarter.allMinorsIn_mul_right {R : Type u_1} [CommRing R] {m : Type u_2} {n : Type u_3} {p : Type u_4} [Fintype n] (A : Matrix m n R) (B : Matrix n p R) {t : ℕ} {J : Ideal R} (hA : AllMinorsIn A t J) : AllMinorsIn (A * B) t J

theorem LatinQuarter.det_mem_pow_of_rows {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) (J : Ideal R) (s : Finset ι) (h : ∀ i ∈ s, ∀ (j : ι), M i j ∈ J) : M.det ∈ J ^ s.card

A determinant with s.card rows in an ideal lies in that ideal power.

theorem LatinQuarter.allMinorsIn_fromBlocks_diagonal {R : Type u_1} [CommRing R] {k h t : ℕ} (A : Matrix (Fin k) (Fin k) R) (Z : Matrix (Fin h) (Fin h) R) (J : Ideal R) (hZ : ∀ (i j : Fin h), Z i j ∈ J) : AllMinorsIn (Matrix.fromBlocks A 0 0 Z) t (J ^ (t - k))

The lower block rows supply enough factors from the residual ideal.