Vanishing of products of matrix minors

@[reducible, inline]

noncomputable abbrev LatinQuarter.squareHom {R : Type u_1} [CommRing R] [CharP R 2] : R →+* R

The square map is a ring homomorphism in characteristic two.

Equations

• LatinQuarter.squareHom = frobenius R 2

theorem LatinQuarter.isUnit_det_of_square_map_eq_one {R : Type u_1} [CommRing R] [CharP R 2] {k : ℕ} (A : Matrix (Fin k) (Fin k) R) (hA : squareHom.mapMatrix A = 1) : IsUnit A.det

Marked top-left block entries square to the identity, so that block is invertible even though the coefficient ring is not a field.

theorem LatinQuarter.marked_blocks_minor_ideal {R : Type u_1} [CommRing R] [CharP R 2] {k h : ℕ} (A : Matrix (Fin k) (Fin k) R) (B : Matrix (Fin k) (Fin h) R) (C : Matrix (Fin h) (Fin k) R) (D : Matrix (Fin h) (Fin h) R) (hA : squareHom.mapMatrix A = 1) (hC : C.map ⇑squareHom = 0) (hD : D.map ⇑squareHom = 0) : ∃ (z : Fin h × Fin h → R), (∀ (j : Fin h × Fin h), z j * z j = 0) ∧ ∀ (t : ℕ), AllMinorsIn (Matrix.fromBlocks A B C D) t (Ideal.span (Set.range z) ^ (t - k))

One block elimination gives a common ideal for all the minors.

theorem LatinQuarter.marked_blocks_product_vanishes {R : Type u_1} [CommRing R] [CharP R 2] {k h : ℕ} {ι : Type u_2} [Fintype ι] (A : Matrix (Fin k) (Fin k) R) (B : Matrix (Fin k) (Fin h) R) (C : Matrix (Fin h) (Fin k) R) (D : Matrix (Fin h) (Fin h) R) (hA : squareHom.mapMatrix A = 1) (hC : C.map ⇑squareHom = 0) (hD : D.map ⇑squareHom = 0) (t : ι → ℕ) (r c : (i : ι) → Fin (t i) → Fin k ⊕ Fin h) (hbudget : h * h < ∑ i : ι, (t i - k)) : ∏ i : ι, ((Matrix.fromBlocks A B C D).submatrix (r i) (c i)).det = 0

The abstract vanishing lemma: more residual factors than residual positions force a repeated square-zero entry.