Rank bounds are closed conditions

For a matrix Z and r : ℕ, the condition rank Z ≤ r says that every (r + 1) × (r + 1) minor of Z vanishes (Matrix.rank_le_iff_forall_det_submatrix_eq_zero). Each such minor is a polynomial in the entries of Z, with integer coefficients, and so is each minor of a power Z ^ j of a square matrix. Hence the conditions rank Z ≤ r and rank (Z ^ j) ≤ r are Zariski closed: they pass from a set of matrices to every point of the zero locus of the polynomials vanishing on that set. Over a field with continuous ring operations and closed points, such as ℂ, they are also closed in the usual topology. The Zariski closure is expressed through Mathlib's MvPolynomial.zeroLocus and MvPolynomial.vanishingIdeal.

The same holds for a linear family φ : V →ₗ[K] M →ₗ[K] N of linear maps between finite-dimensional spaces, read in the coordinates of a basis of the parameter space V: the entries of the matrix of φ x are linear in the coordinates of x, so its minors are polynomials in them. The bound rank (φ x) ≤ p is therefore Zariski closed in x. Over an infinite field the complementary condition p ≤ rank (φ x) cuts out a Zariski-open set, which is Zariski dense as soon as it is nonempty, because a nonzero polynomial cannot vanish on the complement of a hypersurface. For the adjoint representation of a Lie algebra this gives the openness and density of the elements whose centralizer has minimal dimension.

Main results

• Matrix.rank_le_of_mem_zeroLocus_vanishingIdeal and Matrix.rank_pow_le_of_mem_zeroLocus_vanishingIdeal: a bound on the rank of a matrix, or of its j-th power, holding on a set of matrices holds on its Zariski closure.
• Matrix.isClosed_setOfPred_rank_le and Matrix.isClosed_setOfPred_rank_pow_le: the matrices of rank at most r, and the square matrices Z with rank (Z ^ j) ≤ r, form closed sets.
• Matrix.isOpen_setOfPred_mulVec_surjective: full row rank is an open condition on matrices.
• LinearMap.exists_eval_eq_det_submatrix: each minor of the matrix of a linear family φ x is a polynomial in the coordinates of x.
• LinearMap.finrank_range_le_of_mem_zeroLocus_vanishingIdeal: a rank bound on a linear family of linear maps passes to the Zariski closure in the coordinates of the parameter.
• LinearMap.vanishingIdeal_setOfPred_le_finrank_range_eq_bot: over an infinite field, a nonempty locus p ≤ rank (φ x) is Zariski dense.

theorem Matrix.rank_le_of_mem_zeroLocus_vanishingIdeal {n : Type u_1} [Fintype n] {k : Type u_2} {K : Type u_3} [Field k] [Field K] [Algebra k K] {m : Type u_4} [Finite m] {S : Set (Matrix m n K)} {r : ℕ} (hS : ∀ Z ∈ S, Z.rank ≤ r) {Y : Matrix m n K} (hY : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' S))) : Y.rank ≤ r

Rank bounds are Zariski closed. If rank Z ≤ r for every matrix Z of a set S, then rank Y ≤ r for every Y on which all polynomials vanishing on S vanish.

theorem Matrix.rank_pow_le_of_mem_zeroLocus_vanishingIdeal {n : Type u_1} [Fintype n] [DecidableEq n] {k : Type u_2} {K : Type u_3} [Field k] [Field K] [Algebra k K] {S : Set (Matrix n n K)} {j r : ℕ} (hS : ∀ Z ∈ S, (Z ^ j).rank ≤ r) {Y : Matrix n n K} (hY : Function.uncurry Y ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal k (Function.uncurry '' S))) : (Y ^ j).rank ≤ r

Rank bounds are Zariski closed. If rank (Z ^ j) ≤ r for every matrix Z of a set S, then rank (Y ^ j) ≤ r for every Y on which all polynomials vanishing on S vanish.

theorem Matrix.isClosed_setOfPred_rank_le {n : Type u_1} [Fintype n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] {m : Type u_3} [Finite m] (r : ℕ) : IsClosed {A : Matrix m n K | A.rank ≤ r}

Over a field with continuous ring operations and closed points, the matrices of rank at most r form a closed set.

theorem Matrix.isOpen_setOfPred_mulVec_surjective {n : Type u_1} [Fintype n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] {m : Type u_3} [Finite m] : IsOpen {A : Matrix m n K | Function.Surjective A.mulVec}

Over a field with continuous ring operations and closed points, surjectivity of A.mulVec is an open condition on matrices A with finitely many rows. When m is nonempty, full row rank is the complement of the closed condition rank A ≤ card m - 1; when m is empty, A.mulVec is always surjective.

theorem Matrix.isClosed_setOfPred_rank_pow_le {n : Type u_1} [Fintype n] [DecidableEq n] {K : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] (j r : ℕ) : IsClosed {Z : Matrix n n K | (Z ^ j).rank ≤ r}

Over a field with continuous ring operations and closed points, the matrices Z with rank (Z ^ j) ≤ r form a closed set.

theorem LinearMap.exists_eval_eq_det_submatrix {K : Type u_1} {V : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [Finite ι] (φ : V →ₗ[K] M →ₗ[K] N) (b : Module.Basis ι K V) {κ : Type u_6} {κ' : Type u_7} [Fintype κ] [DecidableEq κ] [Finite κ'] (bM : Module.Basis κ K M) (bN : Module.Basis κ' K N) {p : ℕ} (r : Fin p → κ') (c : Fin p → κ) : ∃ (q : MvPolynomial ι K), ∀ (x : V), (MvPolynomial.eval (b.equivFun x)) q = (((toMatrix bM bN) (φ x)).submatrix r c).det

The minors of the matrices of a linear family of linear maps are polynomials in the coordinates of the parameter: for bases bM and bN and row and column selections r and c, some polynomial q evaluates at the b-coordinates of x to the minor of the matrix of φ x.

theorem LinearMap.finrank_range_le_of_mem_zeroLocus_vanishingIdeal {K : Type u_1} {V : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [Finite ι] (φ : V →ₗ[K] M →ₗ[K] N) (b : Module.Basis ι K V) [FiniteDimensional K M] [FiniteDimensional K N] {S : Set V} {p : ℕ} (hS : ∀ y ∈ S, Module.finrank K ↥(φ y).range ≤ p) {x : V} (hx : b.equivFun x ∈ MvPolynomial.zeroLocus K (MvPolynomial.vanishingIdeal K (⇑b.equivFun '' S))) : Module.finrank K ↥(φ x).range ≤ p

Rank bounds on a linear family are Zariski closed. Let φ be a linear family of linear maps parametrized by a vector space V with basis b. If rank (φ y) ≤ p for every y in a set S, then rank (φ x) ≤ p for every x whose coordinates lie in the common zero locus of the polynomials vanishing on the coordinates of S.

theorem LinearMap.vanishingIdeal_setOfPred_le_finrank_range_eq_bot {K : Type u_1} {V : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [Finite ι] (φ : V →ₗ[K] M →ₗ[K] N) (b : Module.Basis ι K V) [FiniteDimensional K M] [FiniteDimensional K N] [Infinite K] {p : ℕ} {x₀ : V} (hx₀ : p ≤ Module.finrank K ↥(φ x₀).range) : MvPolynomial.vanishingIdeal K (⇑b.equivFun '' {x : V | p ≤ Module.finrank K ↥(φ x).range}) = ⊥

A nonempty rank lower bound locus is Zariski dense. Over an infinite field, if some member of a linear family φ of linear maps has rank at least p, then the only polynomial vanishing on the coordinates of every x with p ≤ rank (φ x) is zero.