[Merged by Bors] - feat: LinearMap.HasFiniteRange and the associated relation by ADedecker · Pull Request #39468 · leanprover-community/mathlib4

ADedecker · 2026-05-16T17:03:15Z

We add two predicates on linear maps: HasFiniteRange says that the range is finitely generated, and HasNoetherianRange says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition.

This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators.

This also adds four supporting lemmas: map_smul_le_map, range_smul_le_range, ker_le_ker_smul and isNoetherian_map.

depends on: [Merged by Bors] - chore: semilinearize LinearMap.submodule[Co]map #39726

github-actions · 2026-05-16T17:04:35Z

PR summary cf64666bd1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Module.LinearMap.FiniteRange` (new file)	1268

Declarations diff

+ HasFiniteRange
+ HasFiniteRange.add
+ HasFiniteRange.cofg_ker
+ HasFiniteRange.comp_left
+ HasFiniteRange.comp_right
+ HasFiniteRange.fg_range
+ HasFiniteRange.hasNoetherianRange
+ HasFiniteRange.neg
+ HasFiniteRange.of_finite_dom
+ HasFiniteRange.of_isNoetherian_rng
+ HasFiniteRange.smul
+ HasFiniteRange.sub
+ HasFiniteRange.zero
+ HasNoetherianRange
+ HasNoetherianRange.add
+ HasNoetherianRange.comp_left
+ HasNoetherianRange.comp_right
+ HasNoetherianRange.hasFiniteRange
+ HasNoetherianRange.isNoetherian_range
+ HasNoetherianRange.neg
+ HasNoetherianRange.of_isNoetherian_dom
+ HasNoetherianRange.of_isNoetherian_rng
+ HasNoetherianRange.quotient_ker
+ HasNoetherianRange.smul
+ HasNoetherianRange.sub
+ HasNoetherianRange.zero
+ equiv_comp
+ equiv_comp_left
+ equiv_comp_right
+ equiv_iff_eqLocus_coFG
+ equiv_iff_hasFiniteRange
+ equiv_iff_hasNoetherianRange
+ equiv_iff_isNoetherian_quotient_eqLocus
+ equiv_of_eqOn_coFG
+ equiv_of_eqOn_of_isNoetherian
+ finiteRange
+ hasFiniteRange_iff_range
+ hasNoetherianRange_iff_hasFiniteRange
+ hasNoetherianRange_iff_quotient_ker
+ hasNoetherianRange_iff_range
+ isNoetherian_map
+ ker_coFG_iff_hasFiniteRange
+ ker_le_ker_smul
+ map_smul_le_map
+ mem_finiteRange_iff_hasFiniteRange
+ mem_finiteRange_iff_hasNoetherianRange
+ range_smul_le_range

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.

No changes to strong technical debt.

No changes to weak technical debt.

ocfnash

I think we should name the new file Mathlib.LinearAlgebra.LinearMap.FiniteRank rather than Mathlib.LinearAlgebra.FiniteRankLinearMap.

Other than this, and the question about what should be the definition, this all looks perfect.

… pm_hasFiniteRank

ADedecker · 2026-05-23T12:34:40Z

-awaiting-author

ADedecker · 2026-05-23T12:35:51Z

Regarding the naming, there's no LinearAlgebra/LinearMap folder and I don't think we should create it just for this. But I am again open to other suggestions.

mathlib-dependent-issues · 2026-05-25T09:53:57Z

This PR/issue depends on:

~~[Merged by Bors] - chore: semilinearize LinearMap.submodule[Co]map #39726~~
By Dependent Issues (🤖). Happy coding!

ocfnash

Thanks! Very nice.

As to the location for the new file, I had a typo in this comment but I intended to suggest that the new file could be a sibling of the existing Defs file in which LinearMap is defined. That would make it: Mathlib.Algebra.Module.LinearMap.FiniteRange.

However what you have proposed is also fine so I'll let you decide.

bors d+

ocfnash · 2026-05-25T10:00:07Z

+theorem hasFiniteRange_iff_ker {f : V →ₗ[K] V₂} :
+    f.HasFiniteRange ↔ f.ker.CoFG :=


Assuming the simpNF linter is happy I suggest we flip the LHS and RHS and add simp:

Suggested change

theorem hasFiniteRange_iff_ker {f : V →ₗ[K] V₂} :

f.HasFiniteRange ↔ f.ker.CoFG :=

@[simp] theorem ker_coFG_iff {f : V →ₗ[K] V₂} :

f.ker.CoFG ↔ f.HasFiniteRange :=

(if not, this can stay as it is)

Done, but I kept hasFiniteRange in the name.

mathlib-bors · 2026-05-25T10:02:40Z

✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

ADedecker · 2026-05-25T14:53:18Z

Thanks for the review!

bors merge

ADedecker · 2026-05-25T14:54:45Z

bors r-

mathlib-bors · 2026-05-25T14:54:48Z

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

ADedecker · 2026-05-25T14:57:10Z

bors merge

@PatrickMassot

We add two predicates on linear maps: `HasFiniteRange` says that the range is finitely generated, and `HasNoetherianRange` says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition. This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators. This also adds four supporting lemmas: `map_smul_le_map`, `range_smul_le_range`, `ker_le_ker_smul` and `isNoetherian_map`.

mathlib-bors · 2026-05-25T16:38:38Z

Pull request successfully merged into master.

Build succeeded:

@PatrickMassot

…r-community#39468) We add two predicates on linear maps: `HasFiniteRange` says that the range is finitely generated, and `HasNoetherianRange` says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition. This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators. This also adds four supporting lemmas: `map_smul_le_map`, `range_smul_le_range`, `ker_le_ker_smul` and `isNoetherian_map`.

@PatrickMassot

…r-community#39468) We add two predicates on linear maps: `HasFiniteRange` says that the range is finitely generated, and `HasNoetherianRange` says that the range is noetherian. We also add the equivalence relation on linear maps saying that two maps differ by a linear map with noetherian range, and prove that it's compatible with addition and composition. This was originally written by @PatrickMassot at the May 2026 ICERM workshop as part of the project on Fredholm operators. This also adds four supporting lemmas: `map_smul_le_map`, `range_smul_le_range`, `ker_le_ker_smul` and `isNoetherian_map`.

ADedecker added 2 commits May 16, 2026 12:19

feat: LinearMap.HasFiniteRank and the associated relation

4bc2f68

done?

e3aad8e

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 16, 2026

ADedecker added 2 commits May 16, 2026 13:55

mk_all

ea51438

docstrings on defs

35fccd4

This was referenced May 16, 2026

[Merged by Bors] - feat: define LinearMap.IsQuasiInverse #39475

Closed

WIP: Fredholm operators #39274

Draft

ocfnash reviewed May 19, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/FiniteRange.lean

Comment thread Mathlib/LinearAlgebra/FiniteRankLinearMap.lean Outdated

ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes. label May 19, 2026

ADedecker added 7 commits May 21, 2026 11:38

tmp

abf9571

I need another dependent PR...

16319d7

chore: semilinearize LinearMap.submodule[Co]map

a51f01e

Merge remote-tracking branch 'ADedecker/AD_semilin_submoduleMap' into…

8b070c3

… pm_hasFiniteRank

Almost done

0ec5fc6

Remove test

c51e42e

rename

9471ccb

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 23, 2026

ADedecker added 2 commits May 23, 2026 14:24

Rewrite doc

9010bb9

other suggestion

995998e

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 23, 2026

ADedecker changed the title ~~feat: LinearMap.HasFiniteRank and the associated relation~~ feat: LinearMap.HasFiniteRange and the associated relation May 23, 2026

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 25, 2026

ocfnash approved these changes May 25, 2026

View reviewed changes

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 25, 2026

Merge remote-tracking branch 'upstream/master' into pm_hasFiniteRank

f2a3616

ADedecker added 2 commits May 25, 2026 16:11

Move file

5fa6f09

suggestions from review

3eefcab

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 25, 2026

mathlib-triage Bot removed ready-to-merge This PR has been sent to bors. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels May 25, 2026

did half the suggestion...

cf64666

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 25, 2026

mathlib-bors Bot changed the title ~~feat: LinearMap.HasFiniteRange and the associated relation~~ [Merged by Bors] - feat: LinearMap.HasFiniteRange and the associated relation May 25, 2026

mathlib-bors Bot closed this May 25, 2026

		theorem hasFiniteRange_iff_ker {f : V →ₗ[K] V₂} :
		f.HasFiniteRange ↔ f.ker.CoFG :=

Uh oh!

Conversation

ADedecker commented May 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cf64666bd1

Import changes for modified files

Declarations diff

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ADedecker commented May 23, 2026

Uh oh!

ADedecker commented May 23, 2026

Uh oh!

mathlib-dependent-issues Bot commented May 25, 2026

Uh oh!

ocfnash left a comment

Choose a reason for hiding this comment

Uh oh!

ocfnash May 25, 2026

Choose a reason for hiding this comment

Uh oh!

ADedecker May 25, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented May 25, 2026

Uh oh!

ADedecker commented May 25, 2026

Uh oh!

ADedecker commented May 25, 2026

Uh oh!

mathlib-bors Bot commented May 25, 2026

Uh oh!

ADedecker commented May 25, 2026

Uh oh!

mathlib-bors Bot commented May 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ADedecker commented May 16, 2026 •

edited

Loading

github-actions Bot commented May 16, 2026 •

edited

Loading