chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass by grunweg · Pull Request #43376 · leanprover-community/mathlib4

grunweg · 2026-09-03T06:29:24Z

This rename is a small part of #31365, step (2) and the analogue of #43368 for semi-linear maps.

In addition, this PR goes one step further by removing the existing LinearMap.ofClass: both definitions mean the same, so we only need one. Note that neither LinearMap nor SemilinearMap is a definition, and LinearMapClass is defined in terms of SemilinearMapClass.

Rename a few lemmas using ofClass, so their names match the naming convention.
And delete LinearMap.coe_semilinearMap, which would have been misnamed now, as an exact duplicate of the now-called LinearMap.coe_ofClass.

github-actions · 2026-09-03T06:30:39Z

PR summary 4b21aa9501

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ LinearMapClass.linearMap
+ SemilinearMapClass.semilinearMap
+ coe_ofClass
+ ofClass_eq_toLinearMap
+ ofClass_injective
+ toLinearMap_eq_ofClass
- instCoeToLinearMap
- linearMap
- semilinearMap

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 4b21aa9).

+6 new declarations
−3 removed declarations

+LinearEquiv.toLinearMap_eq_ofClass
+LinearMap.coe_ofClass
+LinearMap.ofClass.congr_simp
+LinearMap.ofClass_injective
-LinearMapClass.instCoeToLinearMap
+Representation.IntertwiningMap.ofClass_eq_toLinearMap
-SemilinearMapClass.semilinearMap.congr_simp
+instIsLocalizedModuleTensorProductOfClassAlgHomToAlgHom
-instIsLocalizedModuleTensorProductSemilinearMapAlgHomToAlgHom

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

Current commit 4b21aa9501
Reference commit a4d9f2fdd2

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).

mcdoll · 2026-09-03T07:54:52Z

I think your deprecation is not correct, see the bot above

grunweg · 2026-09-03T08:02:50Z

Good catch! Should be fixed now.

grunweg · 2026-09-07T07:04:29Z


 /-- The range of a linear map from a finite module is finite. -/
 instance range [Module.Finite R M] (f : M →ₗ[R] N) : Module.Finite R f.range :=
-  of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict


This proof was just unnecessarily convoluted: the SemilinearMapClass.semilinearMap was already doing nothing.

…ingly And deprecate a lemma which is now an exact duplicate

grunweg · 2026-09-07T09:41:45Z

-theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
-    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
-  rfl
+@[deprecated (since := "2026-09-07")] alias coe_semilinearMap := coe_ofClass


These statements were exact duplicates even before this PR.

grunweg · 2026-09-07T09:48:00Z

I have reworked the PR.
-awaiting-author

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

themathqueen

Thanks!

maintainer delegate

github-actions · 2026-09-07T14:53:58Z

🚀 Pull request has been placed on the maintainer queue by themathqueen.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

j-loreaux

Thanks!

bors merge

…43376) This rename is a small part of #31365, step (2) and the analogue of #43368 for semi-linear maps. In addition, this PR goes one step further by removing the existing `LinearMap.ofClass`: both definitions mean the same, so we only need one. Note that neither `LinearMap` nor `SemilinearMap` is a definition, and `LinearMapClass` is defined in terms of `SemilinearMapClass`. Rename a few lemmas using `ofClass`, so their names match the naming convention. And delete `LinearMap.coe_semilinearMap`, which would have been misnamed now, as an exact duplicate of the now-called `LinearMap.coe_ofClass`.

mathlib-bors · 2026-09-08T03:39:20Z

Build failed:

ci (staging) / Build

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

grunweg requested a review from mcdoll September 3, 2026 06:29

github-actions Bot added the t-ring-theory Ring theory label Sep 3, 2026

grunweg mentioned this pull request Sep 3, 2026

Fixing Mathlib's morphism hierarchy #31365

Open

17 tasks

grunweg changed the title ~~chore: rename SemiinearMapClass.semilinearMap to SemilinearMap.ofClass~~ chore: rename SemilinearMapClass.semilinearMap to SemilinearMap.ofClass Sep 3, 2026

mcdoll added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 3, 2026

grunweg commented Sep 3, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/Defs.lean Outdated

grunweg removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 3, 2026

themathqueen reviewed Sep 3, 2026

View reviewed changes

Comment thread Mathlib/RepresentationTheory/Intertwining.lean

themathqueen reviewed Sep 3, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/Defs.lean Outdated

github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 3, 2026

wip

4996b16

grunweg force-pushed the semilinearmap-ofclass branch from 573303e to 4996b16 Compare September 7, 2026 07:03

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 7, 2026

grunweg commented Sep 7, 2026

View reviewed changes

eric-wieser reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/Defs.lean Outdated

Docs; fix bad merge

351e453

grunweg mentioned this pull request Sep 7, 2026

chore(LinearMap/Defs): misc minor clean-up #43518

Open

1 task

grunweg added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 7, 2026

grunweg added 2 commits September 7, 2026 11:34

chore: remove LInearMap.ofClass instead

6fd0951

Minor follow-up clean-up: use ofClass more and fix lemma names accord…

6d0e811

…ingly And deprecate a lemma which is now an exact duplicate

grunweg commented Sep 7, 2026

View reviewed changes

grunweg changed the title ~~chore: rename SemilinearMapClass.semilinearMap to SemilinearMap.ofClass~~ chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass Sep 7, 2026

fix deprecation

22c4dea

github-actions Bot removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 7, 2026

Fix deprecations and one proof

a944082

eric-wieser reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/Defs.lean Outdated

themathqueen reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Bialgebra/Convolution.lean Outdated

themathqueen reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Bialgebra/Convolution.lean Outdated

themathqueen reviewed Sep 7, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LinearMap/Defs.lean Outdated

grunweg and others added 2 commits September 7, 2026 13:31

Fix deprecation; update comments

38994ef

Update Mathlib/Algebra/Module/LinearMap/Defs.lean

cb16955

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

themathqueen added t-algebra Algebra (groups, rings, fields, etc) and removed t-ring-theory Ring theory labels Sep 7, 2026

themathqueen reviewed Sep 7, 2026

View reviewed changes

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

themathqueen reviewed Sep 7, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 7, 2026

Update Mathlib/Algebra/Module/LinearMap/Defs.lean

4b21aa9

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

j-loreaux reviewed Sep 8, 2026

View reviewed changes

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Sep 8, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 8, 2026

mathlib-bors Bot added bors-staging This PR is currently being built by bors on the staging branch. awaiting-requeue This PR was on the bors queue but came off after a build failure or other issue. labels Sep 8, 2026

mathlib-bors Bot removed ready-to-merge This PR has been sent to bors. bors-staging This PR is currently being built by bors on the staging branch. labels Sep 8, 2026

Uh oh!

Conversation

grunweg commented Sep 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 4b21aa9501

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mcdoll commented Sep 3, 2026

Uh oh!

Uh oh!

grunweg commented Sep 3, 2026

Uh oh!

Uh oh!

Uh oh!

grunweg Sep 7, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg Sep 7, 2026

Choose a reason for hiding this comment

Uh oh!

grunweg commented Sep 7, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

themathqueen left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Sep 7, 2026

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Sep 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Sep 3, 2026 •

edited

Loading

github-actions Bot commented Sep 3, 2026 •

edited

Loading