The family of maximal minors in increasing row order

MathlibAnnex.Matrix.maximalMinors

def

Collects the determinants of all square submatrices with all columns and an increasing selection of rows.

Statement

Let be a commutative ring, a linearly ordered set, and an -by- matrix over . The family of maximal minors is

Thus the rows are taken in the indicated increasing order, and the columns remain in their original order. Only finite subsets of size occur in the domain.

Definition

For every selected subset, the ordering convention is part of the defining formula:

The increasing enumeration fixes the row order and hence the sign. This is not the determinant of rows arranged in an unspecified order.

Assumptions

The number is any nonnegative integer. The row set is linearly ordered and may be infinite. No field, nonzero-minor or rank assumption is made.

Conclusion

Each component is a determinant with the same increasing-row convention. When , the unique selected subset is empty and its empty determinant is . If there are no -element subsets, the family has empty domain.

An increasing injection from the column positions into determines its range subset; the cited adapter lemmas identify the selected matrix and minor with that injection. An arbitrary ordered tuple of rows carries additional order information and is treated separately in the factorization theorem. Selection also commutes with right multiplication: .

def maximalMinors {n : ℕ} {ι : Type u} {R : Type v} [LinearOrder ι] [CommRing R]
    (A : _root_.Matrix ι (Fin n) R) : MaximalMinorIndex n ι → R :=
  fun s => maximalMinor A s

noncomputable section

open scoped BigOperators

namespace MathlibAnnex
namespace Matrix

universe u v

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project