feat(LinearAlgebra/Matrix/Rank): linearly independent rows give a surjective mulVec

[mlgraham]

LinearIndependent.rank_matrix says a matrix with linearly independent rows has full row rank. This adds the consequence that mulVec is then surjective.

Mathlib has mulVec_surjective_iff_exists_right_inverse and the square case mulVec_surjective_iff_isUnit, but nothing stating it from independence of the rows. I needed it to produce a vector raising every active constraint in a max-min argument.

The proof shows range M.mulVecLin = ⊤ by comparing finranks.

---

Some AI was used.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to Zulip and join the Lean community.
Thank you again for joining our community.

[github-actions]

PR summary f56f68d891

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Matrix.Rank	1719	1727	+8 (+0.47%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.SymplecticGroup	6
8 files Mathlib.Combinatorics.Configuration Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition Mathlib.LinearAlgebra.Matrix.Echelon.Pivot Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.LinearAlgebra.Matrix.Rank Mathlib.Tactic.Echelon.Bareiss Mathlib.Tactic.Echelon.Cert Mathlib.Tactic.NormRank	8

---

Declarations diff (regex)

+ _root_.LinearIndependent.mulVec_surjective
+ _root_.LinearIndependent.vecMul_surjective
+ mulVec_surjective_iff_rank_eq_card
+ vecMul_surjective_iff_rank_eq_card

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f56f68d).

• +4 new declarations
• −0 removed declarations

+LinearIndependent.mulVec_surjective
+LinearIndependent.vecMul_surjective
+Matrix.mulVec_surjective_iff_rank_eq_card
+Matrix.vecMul_surjective_iff_rank_eq_card

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit f56f68d891
Reference commit dec5b2b780

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

can you also add the vecMul versions please?

[themathqueen]

I don't think rewriting a definition backwards is nice

Suggested change

	exact Submodule.eq_top_of_finrank_eq <| by rw [← rank, h.rank_matrix, Module.finrank_pi]
	exact Submodule.eq_top_of_finrank_eq <| by rw [Module.finrank_pi, ← h.rank_matrix, rank]

[themathqueen]

maybe add:

theorem mulVec_surjective_iff_rank_eq_card [Field R] [Fintype m] {M : Matrix m n R} :
    M.mulVec.Surjective ↔ M.rank = Fintype.card m := by
  rw [← coe_mulVecLin, ← LinearMap.range_eq_top, rank, ← Module.finrank_pi R]
  exact ⟨fun h ↦ by rw [h, finrank_top], eq_top_of_finrank_eq⟩

and then this can be

Suggested change

	rw [← coe_mulVecLin, ← LinearMap.range_eq_top]
	exact Submodule.eq_top_of_finrank_eq <| by rw [← rank, h.rank_matrix, Module.finrank_pi]
	rw [mulVec_surjective_iff_rank_eq_card, h.rank_matrix]

[mlgraham]

Thanks, that's cleaner. Added mulVec_surjective_iff_rank_eq_card as suggested (with Submodule.eq_top_of_finrank_eq, since the bare name doesn't resolve in the Matrix namespace) and reduced LinearIndependent.mulVec_surjective to the one-line rw.

[SnirBroshi]

Could you generalize beyond Fields?
Here's a possible proof for IsSemisimpleRing:

example {m n R : Type*} [Ring R] [IsSemisimpleRing R] [Fintype n] {M : Matrix m n R}
    (h : LinearIndependent R M.row) : M.mulVec.Surjective := by
  nontriviality R using M.mulVec.surjective_to_subsingleton
  have := @Fintype.ofFinite m h.finite_of_isNoetherian
  classical
  have ⟨f, hf⟩ := IsSemisimpleModule.extension_property M.toLinearMapRight'
    (vecMul_injective_iff.mpr h) .id
  have : M * f.toMatrixRight' = 1 := toLinearMapRight'.injective <| by simpa using hf
  exact fun v ↦ ⟨f.toMatrixRight' *ᵥ v, by simp [this]⟩

There's also this [CommRing R] [IsArtinianRing R] proof but it's only for square matrices:

example {m R : Type*} [CommRing R] [IsArtinianRing R] [Fintype m] {M : Matrix m m R}
    (h : LinearIndependent R M.row) : M.mulVec.Surjective := by
  classical
  rwa [mulVec_surjective_iff_isUnit, IsArtinianRing.isUnit_iff_isRightRegular,
    isRightRegular_iff_vecMul_injective, vecMul_injective_iff]

The rectangular case might require more API, not sure

[mlgraham]

Done, with your proof verbatim — the theorem is now [Ring R] [IsSemisimpleRing R]. This requires importing Mathlib.RingTheory.SimpleModule.Basic; the summary bot shows the resulting import-graph change.

I've left out the IsArtinianRing square version: IsArtinianRing.isUnit_iff_isRightRegular and isRightRegular_iff_vecMul_injective don't seem to exist yet, so that direction would need new API — better a follow-up PR.

[SnirBroshi]

IsArtinianRing.isUnit_iff_isRightRegular and isRightRegular_iff_vecMul_injective don't seem to exist yet

What? They do exist. Are you using an LLM to respond?

[mlgraham]

can you also add the vecMul versions please?

Added both: Matrix.vecMul_surjective_iff_rank_eq_card and LinearIndependent.vecMul_surjective (via mulVec_transpose and rank_transpose). These stay over fields — the transpose identity needs commutativity, so a semisimple version of the vecMul direction would need a right-module formulation.

[mlgraham]

-awaiting-author

[SnirBroshi]

Some AI was used.

Could you please elaborate, per the guidelines? Thanks!