Selecting a nonsingular residue minor

A rectangular matrix over a field with full column rank has a square row minor with nonzero determinant. The selected rows are returned as an embedding of the column index type into the row index type, matching the input expected by GeometrySplitTangentMatrix.

theorem Stafford38.GeometryResidueMinorSelection.exists_selectedMinor_det_ne_zero_of_rank_eq_card {k : Type u} [Field k] {ι : Type v} {κ : Type w} [Finite ι] [Fintype κ] [DecidableEq κ] (B : Matrix ι κ k) (hrank : B.rank = Fintype.card κ) : ∃ (rows : κ ↪ ι), (GeometrySplitTangentMatrix.selectedMinor B rows).det ≠ 0

Full column rank produces an explicitly indexed square row minor with nonzero determinant.

theorem Stafford38.GeometryResidueMinorSelection.exists_selectedMinor_det_ne_zero_of_mulVec_injective {k : Type u} [Field k] {ι : Type v} {κ : Type w} [Finite ι] [Fintype κ] [DecidableEq κ] (B : Matrix ι κ k) (hinj : Function.Injective B.mulVec) : ∃ (rows : κ ↪ ι), (GeometrySplitTangentMatrix.selectedMinor B rows).det ≠ 0

Injectivity of the residue matrix on column vectors is the usual hypothesis implying the existence of a nonsingular selected row minor.

Power-series residue matrices

def Stafford38.GeometryResidueMinorSelection.residueMatrix {k : Type u} [Field k] {ι : Type v} {κ : Type w} (B : Matrix ι κ (PowerSeries k)) : Matrix ι κ k

Entrywise constant coefficient of a power-series matrix.

Equations

• Stafford38.GeometryResidueMinorSelection.residueMatrix B i j = PowerSeries.constantCoeff (B i j)

theorem Stafford38.GeometryResidueMinorSelection.constantCoeff_selectedMinor_det {k : Type u} [Field k] {ι : Type v} {κ : Type w} [Fintype κ] [DecidableEq κ] (B : Matrix ι κ (PowerSeries k)) (rows : κ ↪ ι) : PowerSeries.constantCoeff (GeometrySplitTangentMatrix.selectedMinor B rows).det = (GeometrySplitTangentMatrix.selectedMinor (residueMatrix B) rows).det

theorem Stafford38.GeometryResidueMinorSelection.powerSeries_exists_selectedMinor_constantCoeff_ne_zero_of_residue_mulVec_injective {k : Type u} [Field k] {ι : Type v} {κ : Type w} [Finite ι] [Fintype κ] [DecidableEq κ] (B : Matrix ι κ (PowerSeries k)) (hinj : Function.Injective (residueMatrix B).mulVec) : ∃ (rows : κ ↪ ι), PowerSeries.constantCoeff (GeometrySplitTangentMatrix.selectedMinor B rows).det ≠ 0

Injectivity after reduction to constant coefficients selects a minor whose power-series determinant is a unit.

theorem Stafford38.GeometryResidueMinorSelection.powerSeries_exists_leftInverse_of_residue_mulVec_injective {k : Type u} [Field k] {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] [DecidableEq κ] (B : Matrix ι κ (PowerSeries k)) (hinj : Function.Injective (residueMatrix B).mulVec) : ∃ (C : Matrix κ ι (PowerSeries k)), C * B = 1

The residue-rank criterion composed with the selected-minor construction: the power-series matrix has an explicit left inverse.