Polynomial-entry matrices: independence of the rows at a parameter value

Mathlib.LinearAlgebra.Matrix.NonsingularInverse has Matrix.linearIndependent_rows_iff_isUnit for square matrices over a field. This file concerns rectangular polynomial-entry matrices over any field K: that the rows of P(t) (or of P(p), with a multivariate parameter) are linearly independent at a parameter value is witnessed by one minor. A column selection e at which the rows are independent at a base point (exists_submatrix_det_ne_zero_of_linearIndependent_rows) picks out the minor Q := det (P selected on columns e), whose evaluation is the specialized minor's determinant, and the rows are independent wherever that determinant is nonzero (linearIndependent_rows_of_specialized_submatrix_det_ne_zero). Unlike the Gram determinant det (A * Aᵀ), the minor needs no linear order on K.

• Along a line (finite_setOf_not_linearIndependent_rows_along_affine_path, _of_polynomial and their vector forms) the parameters where independence fails are finitely many (Polynomial.finite_setOfPred_isRoot), with no hypothesis on K. The combinatorial-rigidity project uses the vector form for exists_uniform_rowIndependent_placement_dim_two, the step behind linearRigidityMatroid_eq_rigidityMatroid (LinearRigidityMatroid.lean), and for the generic placements of GenericRigidityMatroid.lean.
• Over a multivariate parameter (Matrix.exists_linearIndependent_rows_specialize, exists_le_finrank_span_polynomial, exists_finrank_dualCoannihilator_polynomial) some point is good when K is infinite: the minor is a nonzero MvPolynomial, so it does not vanish somewhere (MvPolynomial.exists_eval_ne_zero). exists_polynomial_ne_zero_of_linearIndependent_at returns the minor instead, so that the minors of several families can be multiplied and one common non-root chosen. The project's genericity device (the blueprint's lem:genericity-device, after Katoh–Tanigawa 2011, §5.1) rests on these lemmas: the entries of the panel-hinge rigidity matrix are polynomials in the panel coordinates, so a rank attained at one realization is attained at a generic one, and no single line need reach the realizations the device is applied to.

Mirror path: Mathlib/LinearAlgebra/Matrix/Rank.lean. Promotion to mathlib is a copy-paste into the upstream file, alongside Matrix.rank_self_mul_transpose and LinearIndependent.rank_matrix.

theorem Matrix.linearIndependent_rows_of_specialized_submatrix_det_ne_zero {ι : Type u_4} {κ : Type u_5} {R : Type u_6} {S : Type u_7} [Fintype ι] [DecidableEq ι] [CommRing R] [IsDomain R] [CommRing S] (M : ι → κ → R) (φ : R →+* S) (e : ι → κ) (hdet : φ (of fun (i j : ι) => M i (e j)).det ≠ 0) : LinearIndependent R M

Linear independence of rows from a specialized nonzero minor. Let M : ι → κ → R be a (possibly rectangular) family of rows over an integral domain R, with ι finite. If there is a column selection e : ι → κ and a ring homomorphism φ : R →+* S into a commutative ring S such that the square submatrix (i, j) ↦ M i (e j) has a determinant whose image under φ is nonzero, then the rows M are linearly independent over R.

This is the "a polynomial minor with a nonzero specialization is itself nonzero, hence the generic rows are independent" reflection: a nonzero specialized minor det forces the R-det to be nonzero (φ 0 = 0), so the chosen square submatrix has independent rows (linearIndependent_rows_of_det_ne_zero), and the full rows are independent by composing with the column-projection linear map (κ → R) → (ι → R) (LinearIndependent.of_comp). No coefficient-wise reflection along φ is used — that would be false when φ has a nontrivial kernel; the argument routes through the minor's determinant instead.

theorem Matrix.exists_submatrix_det_ne_zero_of_linearIndependent_rows {m : Type u_4} {n : Type u_5} {K : Type u_6} [Field K] [Fintype m] [DecidableEq m] [Finite n] {M : Matrix m n K} (h : LinearIndependent K M.row) : ∃ (e : m → n), (of fun (i j : m) => M i (e j)).det ≠ 0

A matrix with linearly independent rows over a field has a nonsingular maximal minor. Let M : Matrix m n K over a field K with m and n finite. If the rows of M are linearly independent, then there is a square column selection e : m → n such that the m × m submatrix (i, j) ↦ M i (e j) has nonzero determinant.

This is the "full row rank ⟹ nonzero square minor" extraction: the columns Mᵀ.row : n → (m → K) span a subspace of K-dimension M.rank = #m (LinearIndependent.rank_matrix + rank_transpose), which is all of m → K, so Mᵀ.row is a spanning family. Extracting a linearly independent spanning subfamily (exists_linearIndependent') gives a basis, necessarily of size #m; reindexing it by m yields e : m → n with Mᵀ.row ∘ e linearly independent, i.e. the transpose of the selected minor has independent rows, i.e. the minor has nonzero determinant (linearIndependent_rows_iff_isUnit + det_transpose + isUnit_iff_ne_zero).

theorem Matrix.finite_setOf_not_linearIndependent_rows_along_affine_path {m : Type u_2} {n : Type u_3} {K : Type u_4} [Field K] [Finite m] [Finite n] (A B : Matrix m n K) {t₀ : K} (h : LinearIndependent K (A + t₀ • B).row) : {t : K | ¬LinearIndependent K (A + t • B).row}.Finite

Linear independence is cofinite along an affine path. Let A B : Matrix m n K over a field K. If the rows of A + t₀ • B are linearly independent for some t₀ : K, then the rows of A + t • B are linearly independent for all but finitely many t : K.

The proof uses a maximal minor rather than the Gram determinant det ((A + t • B) * (A + t • B)ᵀ), which detects independence only over a linearly ordered field (over ℂ the single row (1, i) is independent, while 1 + i² = 0): a column selection e witnessing the rows LI at t₀ (exists_submatrix_det_ne_zero_of_linearIndependent_rows) picks out a single minor Q := det (P selected on columns e) : Polynomial K of the polynomial-entry matrix P := X • C(B) + C(A), whose evaluation at t is the specialized minor's determinant ((evalRingHom t).map_det). Q is nonzero (nonzero at t₀), hence has finitely many roots (Polynomial.finite_setOfPred_isRoot); at any non-root t the specialized minor is nonsingular, so the rows are LI there too (linearIndependent_rows_of_specialized_submatrix_det_ne_zero). No infiniteness or characteristic hypothesis on K is needed: the argument only uses that a nonzero univariate polynomial has finitely many roots.

theorem Matrix.finite_setOf_not_linearIndependent_rows_of_polynomial {m : Type u_2} {n : Type u_3} {K : Type u_4} [Field K] [Finite m] [Finite n] (P : Matrix m n (Polynomial K)) {t₀ : K} (h : LinearIndependent K (P.map ⇑(Polynomial.evalRingHom t₀)).row) : {t : K | ¬LinearIndependent K (P.map ⇑(Polynomial.evalRingHom t)).row}.Finite

Linear independence of rows is cofinite along a polynomial-entry family. Generalizes finite_setOf_not_linearIndependent_rows_along_affine_path from the affine family A + t • B to an arbitrary polynomial-entry matrix P : Matrix m n (Polynomial K) over a field K: if the rows of the specialization P.map (eval t₀) are linearly independent at some t₀ : K, then the rows of P.map (eval t) are linearly independent for all but finitely many t : K.

The same maximal-minor argument as the affine case: a column selection e witnessing LI at t₀ (exists_submatrix_det_ne_zero_of_linearIndependent_rows) picks out the single minor Q := det (P selected on columns e) : Polynomial K, whose evaluation at t is the specialized minor's determinant; Q is nonzero (nonzero at t₀), so Polynomial.finite_setOfPred_isRoot bounds the bad-t set, and at any non-root t linearIndependent_rows_of_specialized_submatrix_det_ne_zero gives LI. The affine case is P = X • B.map C + A.map C. No infiniteness or characteristic hypothesis on K is needed.

theorem Matrix.exists_linearIndependent_rows_specialize {m : Type u_2} {n : Type u_3} {K : Type u_4} {σ : Type u_5} [Field K] [Infinite K] [Finite m] [Finite n] (P : Matrix m n (MvPolynomial σ K)) {p₀ : σ → K} (h : LinearIndependent K (P.map ⇑(MvPolynomial.eval p₀)).row) : ∃ (p : σ → K), LinearIndependent K (P.map ⇑(MvPolynomial.eval p)).row

Linear independence of rows is attained at a generic specialization (multivariate analogue of finite_setOf_not_linearIndependent_rows_along_affine_path). Let K be an infinite field and P : Matrix m n (MvPolynomial σ K) a polynomial-entry matrix. If the rows of the specialization P.map (eval p₀) are linearly independent at some point p₀ : σ → K, then there is a point p : σ → K at which the rows of P.map (eval p) are linearly independent.

The same maximal-minor argument, with an existence step in place of the finiteness step: a column selection e witnessing LI at p₀ picks out the single minor Q := det (P selected on columns e) : MvPolynomial σ K. Q is nonzero (nonzero at p₀), hence non-vanishing at some point p (MvPolynomial.exists_eval_ne_zero, the contrapositive of MvPolynomial.funext over the infinite domain K, where [Infinite K] is used); there linearIndependent_rows_of_specialized_submatrix_det_ne_zero gives LI. Unlike the univariate (affine-line) case, the bad set {p | rows dependent} is generally not finite — it is the zero locus of Q, whose complement is merely nonempty — so the conclusion is ∃ p, … rather than {bad}.Finite.

theorem LinearIndependent.finite_setOf_not_along_affine_path {K : Type u_1} {ι : Type u_2} {W : Type u_3} [Field K] [Finite ι] [AddCommGroup W] [Module K W] [Module.Finite K W] {a b : ι → W} {t₀ : K} (h : LinearIndependent K fun (i : ι) => a i + t₀ • b i) : {t : K | ¬LinearIndependent K fun (i : ι) => a i + t • b i}.Finite

Vector-form polynomial-along-line. For a finite-dim W-vector space over a field K and an affine family t ↦ fun i => a i + t • b i : K → ι → W (with ι finite), if the family is linearly independent at some t₀ : K, then it is LI for all but finitely many t : K.

Vector analogue of Matrix.finite_setOf_not_linearIndependent_rows_along_affine_path, derived by pulling along a basis-induced isomorphism W ≃ₗ[K] (Fin (finrank K W) → K). No infiniteness or characteristic hypothesis on K is needed.

theorem exists_le_finrank_span_polynomial {K : Type u_1} {ι : Type u_2} {W : Type u_3} {σ : Type u_4} [Field K] [Infinite K] [Finite ι] [AddCommGroup W] [Module K W] [Module.Finite K W] (g : (σ → K) → ι → W) (c : ι → Fin (Module.finrank K W) → MvPolynomial σ K) (φ : W ≃ₗ[K] Fin (Module.finrank K W) → K) (hg : ∀ (p : σ → K) (i : ι) (j : Fin (Module.finrank K W)), φ (g p i) j = (MvPolynomial.eval p) (c i j)) {p₀ : σ → K} {s : Set ι} (h : LinearIndependent K fun (i : ↑s) => g p₀ ↑i) : ∃ (p : σ → K), Nat.card ↑s ≤ Module.finrank K ↥(Submodule.span K (Set.range (g p)))

Vector-form multivariate rank attainment. For a finite-dim W-vector space over an infinite field K and a polynomial-coordinate family g : (σ → K) → ι → W whose basis coordinates are multivariate polynomial evaluations — fixed c : ι → Fin (finrank K W) → MvPolynomial σ K and a basis identification φ : W ≃ₗ[K] (Fin (finrank K W) → K) with φ (g p i) j = eval p (c i j) — if the subfamily indexed by a subset s : Set ι is linearly independent at some point p₀ : σ → K, then there is a point p : σ → K at which the span of the full family g p has finrank at least #s.

This is the multivariate analogue of the case of one affine line, where LinearIndependent.finite_setOf_not_along_affine_path keeps the subfamily on s independent for all but finitely many t ({bad}.Finite): here the parameter ranges over all of σ → K and a single good point is produced (∃ p, not a cofinite set), by Matrix.exists_linearIndependent_rows_specialize, whence the [Infinite K]. The subfamily on s is LI at the produced p, forcing the full span's finrank ≥ #s (finrank_span_eq_card + Submodule.finrank_mono).

theorem exists_finrank_dualCoannihilator_polynomial {K : Type u_1} {ι : Type u_2} {V : Type u_3} {σ : Type u_4} [Field K] [Infinite K] [Finite ι] [AddCommGroup V] [Module K V] [Module.Finite K V] (g : (σ → K) → ι → Module.Dual K V) (c : ι → Fin (Module.finrank K (Module.Dual K V)) → MvPolynomial σ K) (φ : Module.Dual K V ≃ₗ[K] Fin (Module.finrank K (Module.Dual K V)) → K) (hg : ∀ (p : σ → K) (i : ι) (j : Fin (Module.finrank K (Module.Dual K V))), φ (g p i) j = (MvPolynomial.eval p) (c i j)) {p₀ : σ → K} {s : Set ι} (h : LinearIndependent K fun (i : ↑s) => g p₀ ↑i) : ∃ (p : σ → K), Nat.card ↑s + Module.finrank K ↥(Submodule.span K (Set.range (g p))).dualCoannihilator ≤ Module.finrank K V

Codimension form: null-space finrank is attained at a generic specialization. The dual of exists_le_finrank_span_polynomial, stated for a polynomial-coordinate family of linear functionals g : (σ → K) → ι → Module.Dual K V over an infinite field K (with V finite-dimensional). If the subfamily indexed by s : Set ι is linearly independent at some p₀ : σ → K, then there is a point p : σ → K at which the common kernel of the full functional family — the dual coannihilator (span (range (g p))).dualCoannihilator = {x : V | ∀ i, g p i x = 0} (Submodule.coe_dualCoannihilator_span) — has finrank at most finrank V − #s.

The span form exists_le_finrank_span_polynomial is dualized here (inheriting its [Infinite K]). The span and its coannihilator have complementary dimension (Subspace.finrank_add_finrank_dualAnnihilator_eq + Subspace.finrank_dualCoannihilator_eq: finrank coann + finrank span = finrank (Dual K V) = finrank V), so "span finrank ≥ #s at the produced p" turns into "coann finrank ≤ finrank V − #s" verbatim. The conclusion is stated additively (#s + finrank coann ≤ finrank V) to sidestep ℕ-subtraction. The combinatorial-rigidity project's genericity device, exists_good_realization (Molecular/AlgebraicInduction/GenericityDevice.lean), applies it with V the space of screw assignments, where the coannihilator contains the infinitesimal motions.

theorem exists_polynomial_ne_zero_of_linearIndependent_at {K : Type u_1} {ι : Type u_2} {W : Type u_3} {σ : Type u_4} [Field K] [Finite ι] [AddCommGroup W] [Module K W] (g : (σ → K) → ι → W) (c : ι → Fin (Module.finrank K W) → MvPolynomial σ K) (φ : W ≃ₗ[K] Fin (Module.finrank K W) → K) (hg : ∀ (p : σ → K) (i : ι) (j : Fin (Module.finrank K W)), φ (g p i) j = (MvPolynomial.eval p) (c i j)) {p₀ : σ → K} {s : Set ι} (h : LinearIndependent K fun (i : ↑s) => g p₀ ↑i) : ∃ (Q : MvPolynomial σ K), (MvPolynomial.eval p₀) Q ≠ 0 ∧ ∀ (p : σ → K), (MvPolynomial.eval p) Q ≠ 0 → LinearIndependent K fun (i : ↑s) => g p ↑i

Vector-form rank-witnessing polynomial. For a finite-dim W-vector space over a field K and a polynomial-coordinate family g : (σ → K) → ι → W whose basis coordinates are multivariate polynomial evaluations — fixed c : ι → Fin (finrank K W) → MvPolynomial σ K and a basis identification φ : W ≃ₗ[K] (Fin (finrank K W) → K) with φ (g p i) j = eval p (c i j) — if the subfamily indexed by a subset s : Set ι is linearly independent at some point p₀ : σ → K, then there is a single multivariate polynomial Q : MvPolynomial σ K that is nonzero at p₀ (eval p₀ Q ≠ 0) and at every non-vanishing point of which the s-subfamily g p is again linearly independent.

This is the constructive refinement of exists_le_finrank_span_polynomial (which produces a single good point p via MvPolynomial.exists_eval_ne_zero, discarding the polynomial, and so needs [Infinite K]): here the witnessing minor Q := det (P.submatrix on a maximal column selection) is exposed instead, so several families' polynomials can be multiplied and MvPolynomial.exists_eval_ne_zero applied to the product once elsewhere, producing one shared non-vanishing point at which all the families are independent. This lemma itself never picks a point, so it needs no infiniteness or characteristic hypothesis on K. Q is built by selecting, via exists_submatrix_det_ne_zero_of_linearIndependent_rows, a square column subset e of the polynomial-entry submatrix P : Matrix s (Fin (finrank K W)) (MvPolynomial σ K) whose specialized minor at p₀ is nonsingular; eval p Q is then the specialized minor's determinant ((eval p).map_det), so eval p₀ Q ≠ 0 by construction and linearIndependent_rows_of_specialized_submatrix_det_ne_zero upgrades any other non-root p back to row independence. The LI of vectors ↔ LI of φ-coordinate rows is the same φ-pullback used in exists_le_finrank_span_polynomial. The combinatorial-rigidity project applies it through exists_rankPolynomial_of_rigidOn_linking and its variants (Molecular/AlgebraicInduction/GenericityDevice.lean), and Case I of its algebraic induction (CaseI.lean) multiplies such minors, so that one point serves the two realizations that Katoh–Tanigawa 2011 combine in (6.6), in the proof of their Lemma 6.3.

theorem exists_polynomial_ne_zero_of_linearIndependent_at_reindex {K : Type u_1} {ι : Type u_2} {W : Type u_3} {σ : Type u_4} {ν : Type u_5} [Field K] [Finite ι] [AddCommGroup W] [Module K W] (e : Fin (Module.finrank K W) ≃ ν) (g : (σ → K) → ι → W) (c : ι → ν → MvPolynomial σ K) (φ : W ≃ₗ[K] ν → K) (hg : ∀ (p : σ → K) (i : ι) (j : ν), φ (g p i) j = (MvPolynomial.eval p) (c i j)) {p₀ : σ → K} {s : Set ι} (h : LinearIndependent K fun (i : ↑s) => g p₀ ↑i) : ∃ (Q : MvPolynomial σ K), (MvPolynomial.eval p₀) Q ≠ 0 ∧ ∀ (p : σ → K), (MvPolynomial.eval p) Q ≠ 0 → LinearIndependent K fun (i : ↑s) => g p ↑i

exists_polynomial_ne_zero_of_linearIndependent_at, basis-flexible column-index form. The reindexing companion of exists_polynomial_ne_zero_of_linearIndependent_at, as exists_good_realization_reindex is of exists_good_realization (Molecular/AlgebraicInduction/GenericityDevice.lean): it accepts the coordinate identification φ against an arbitrary finite basis index ν (with the cardinality bridge e : Fin (finrank K W) ≃ ν) rather than forcing the canonical Fin (finrank K W) literally, since a concrete basis (e.g. b.dualBasis.equivFun for a project-supplied basis b) is indexed by whatever type b itself is indexed by, not by Fin (finrank K W) up to defeq. Reduces to the base lemma by precomposing φ with the index reindexing LinearEquiv.funCongrLeft K K e and pulling c back along e, exactly as exists_good_realization_reindex does. The combinatorial-rigidity project's abundance lemmas (SimpleGraph.exists_isGenericPlacement_abundance and its body-bar, panel and hinge analogues) and the files of Molecular/Molecule/Pencil/ use it.

theorem LinearIndependent.exists_notMem_of_polynomial_repr {K : Type u_1} {ι : Type u_2} {κ : Type u_3} {M : Type u_4} [Field K] [Infinite K] [Finite ι] [Finite κ] [AddCommGroup M] [Module K M] (b : Module.Basis κ K M) (g : K → ι → M) (P : ι → κ → Polynomial K) (hg : ∀ (t : K) (i : ι) (j : κ), (b.repr (g t i)) j = Polynomial.eval t (P i j)) (h0 : LinearIndependent K (g 0)) (bad : Finset K) : ∃ t ∉ bad, t ≠ 0 ∧ LinearIndependent K (g t)

One-variable rank transfer along a polynomial-coordinate family. For a basis b : Basis κ K M over an infinite field K (with κ finite) and a family g : K → ι → M (with ι finite) whose basis coordinates are univariate-polynomial evaluations — a fixed P : ι → κ → Polynomial K with b.repr (g t i) j = (P i j).eval t — if the family g 0 is linearly independent at t = 0, then there is a t avoiding any prescribed finite bad set and nonzero (t ∉ bad, t ≠ 0) at which g t is again linearly independent.

The proof pulls g t back along φ := b.equivFun : M ≃ₗ[K] (κ → K) (so φ (g t i) j = b.repr (g t i) j = (P i j).eval t, i.e. φ ∘ g t is the row family of (Matrix.of P).map (evalRingHom t)); LI transfers across φ (LinearMap.linearIndependent_iff), so finite_setOf_not_linearIndependent_rows_of_polynomial makes the dependent-t set finite (needing no infiniteness itself), and since K is infinite (Set.Finite.infinite_compl) some t lies outside that set and the finite bad ∪ {0}.

This is the polynomial form of a step in the proof of Katoh–Tanigawa 2011, Lemma 5.2 (p. 669), where each minor of R(G, pₜ) is a continuous function of t. The combinatorial-rigidity project applies it along the one-parameter shear of Case III (caseIIICandidate_exists_good_shear in Molecular/AlgebraicInduction/CaseIII/Candidate.lean): the family is independent at t = 0, and the bad set holds the shears at which the sheared normal is parallel to another (setOf_not_shear_linearIndependent_subsingleton in PanelLayer.lean).