Determinantal rank and sandwich compression

The mortality proof uses vanishing minors as a natural-number rank bound. This avoids choosing bases for exterior powers. All matrix products in this file are ordinary products over a commutative scalar ring.

def KoetheCounterexample.Mortality.MinorsVanish {R : Type u_1} [CommRing R] {n : Type u_2} (A : Matrix n n R) (r : ℕ) : Prop

All minors of a specified size vanish. Repeated rows or columns are allowed in the indexing functions; their determinants are automatically zero.

Equations

• KoetheCounterexample.Mortality.MinorsVanish A r = ∀ (I J : Fin r → n), (A.submatrix I J).det = 0

theorem KoetheCounterexample.Mortality.det_submatrix_zero_of_not_injective {R : Type u_1} [CommRing R] {n : Type u_2} {m : Type u_3} {r : ℕ} (A : Matrix n m R) (I : Fin r → n) (J : Fin r → m) (hI : ¬Function.Injective I) : (A.submatrix I J).det = 0

theorem KoetheCounterexample.Mortality.injective_of_det_submatrix_ne_zero {R : Type u_1} [CommRing R] {n : Type u_2} {m : Type u_3} {r : ℕ} (A : Matrix n m R) (I : Fin r → n) (J : Fin r → m) (h : (A.submatrix I J).det ≠ 0) : Function.Injective I

theorem KoetheCounterexample.Mortality.minorsVanish_above {R : Type u_1} [CommRing R] {n : Type u_2} {r : ℕ} [Fintype n] (A : Matrix n n R) (h : Fintype.card n < r) : MinorsVanish A r

theorem KoetheCounterexample.Mortality.eq_zero_of_minorsVanish_one {R : Type u_1} [CommRing R] {n : Type u_2} (A : Matrix n n R) (h : MinorsVanish A 1) : A = 0

theorem KoetheCounterexample.Mortality.det_mul_expand_rows {R : Type u_1} [CommRing R] {n : Type u_2} {r : ℕ} [Fintype n] (A : Matrix (Fin r) n R) (B : Matrix n (Fin r) R) : (A * B).det = ∑ f : Fin r → n, (∏ i : Fin r, A i (f i)) * (B.submatrix f id).det

Expansion by multilinearity in the rows. Unlike a compound-matrix formula, this involves no ordering of subsets and no division by a factorial.

theorem KoetheCounterexample.Mortality.submatrix_mul_outer {R : Type u_1} [CommRing R] {n : Type u_2} [Fintype n] {l : Type u_4} {o : Type u_5} {p : Type u_6} {q : Type u_7} (A : Matrix l n R) (B : Matrix n o R) (I : p → l) (J : q → o) : (A * B).submatrix I J = A.submatrix I id * B.submatrix id J

Restricting only the outside indices of a rectangular product.

theorem KoetheCounterexample.Mortality.det_map {R : Type u_1} [CommRing R] {r : ℕ} {S : Type u_4} [CommRing S] (φ : R →+* S) (A : Matrix (Fin r) (Fin r) R) : (A.map ⇑φ).det = φ A.det

theorem KoetheCounterexample.Mortality.pivot_factorization {K : Type u_1} [Field K] {n : Type u_2} {r : ℕ} (P : Matrix n n K) (I J : Fin r → n) (hp : (P.submatrix I J).det ≠ 0) (hnext : MinorsVanish P (r + 1)) : P = P.submatrix id J * (P.submatrix I J)⁻¹ * P.submatrix I id

A nonzero r-minor, together with vanishing (r+1)-minors, gives the usual pivot factorization. The inverse is taken only over a field.

theorem KoetheCounterexample.Mortality.sandwich_minors_vanish_field {K : Type u_1} [Field K] {n : Type u_2} {r : ℕ} [Fintype n] (P C : Matrix n n K) (I J : Fin r → n) (hp : (P.submatrix I J).det ≠ 0) (hnext : MinorsVanish P (r + 1)) (hz : ((P * C * P).submatrix I J).det = 0) : MinorsVanish (P * C * P) r

The pivot detects every r-minor of a sandwiched product.

theorem KoetheCounterexample.Mortality.sandwich_minors_vanish {R : Type u_1} [CommRing R] [IsDomain R] {n : Type u_2} [Fintype n] {r : ℕ} (P C : Matrix n n R) (I J : Fin r → n) (hp : (P.submatrix I J).det ≠ 0) (hnext : MinorsVanish P (r + 1)) (hz : ((P * C * P).submatrix I J).det = 0) : MinorsVanish (P * C * P) r

Polynomial/domain version of sandwich compression. Localization is used only to invert the fixed nonzero pivot; injectivity returns the identity to its original commutative domain.