[Merged by Bors] - refactor: make several NonUnitalAlgHom definitions take a particular algebra homomorphism by grunweg · Pull Request #43579 · leanprover-community/mathlib4

grunweg · 2026-09-08T13:17:49Z

as opposed to a NonUnitalAlgHomClass.
Specifically, this PR changes NonUnitalSubalgebra.{map, comap} as well as NonUnitalAlgHom.{range,rangeRestrict,codRestrict,equalizer}.

Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines
and align them with standard mathlib style.

Adapt (almost) all theorems about them to take in a concrete morphism also.

This follows the general patterns established in #31365:

we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions.

Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.

Continuation of #43377.

…er} take in a concrete morphism instead and fix associated theorems

github-actions · 2026-09-08T13:19:03Z

PR summary c31a893819

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

++-- codRestrict
++-- coe_range
++-- mem_range_self

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

⚠️ No declarations diff yet: there is no built master snapshot at this PR's merge-base (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

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

Current commit c31a893819
Reference commit 38f65a093a

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

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

themathqueen

Looks good! Thanks!

maintainer delegate

github-actions · 2026-09-09T09:43:35Z

🚀 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

…algebra homomorphism (#43579) as opposed to a `NonUnitalAlgHomClass`. Specifically, this PR changes `NonUnitalSubalgebra.{map, comap}` as well as `NonUnitalAlgHom.{range,rangeRestrict,codRestrict,equalizer}`. Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines and align them with standard mathlib style. Adapt (almost) all theorems about them to take in a concrete morphism also. This follows the general patterns established in #31365: > we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions. > Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.

mathlib-bors · 2026-09-09T17:34:30Z

Build failed:

ci (staging) / Lint style

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

grunweg · 2026-09-09T17:35:56Z

CI error looks intermittent and unrelated:
bors merge

…algebra homomorphism (#43579) as opposed to a `NonUnitalAlgHomClass`. Specifically, this PR changes `NonUnitalSubalgebra.{map, comap}` as well as `NonUnitalAlgHom.{range,rangeRestrict,codRestrict,equalizer}`. Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines and align them with standard mathlib style. Adapt (almost) all theorems about them to take in a concrete morphism also. This follows the general patterns established in #31365: > we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions. > Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.

mathlib-bors · 2026-09-09T17:38:16Z

Build failed:

ci (staging) / Lint style

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

bryangingechen · 2026-09-09T20:03:21Z

bors r+

…algebra homomorphism (#43579) as opposed to a `NonUnitalAlgHomClass`. Specifically, this PR changes `NonUnitalSubalgebra.{map, comap}` as well as `NonUnitalAlgHom.{range,rangeRestrict,codRestrict,equalizer}`. Since this removes all uses of a bundled morphism class, we also remove the assocated variable lines and align them with standard mathlib style. Adapt (almost) all theorems about them to take in a concrete morphism also. This follows the general patterns established in #31365: > we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions. > Given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.

mathlib-bors · 2026-09-09T22:04:21Z

Pull request successfully merged into master.

Build succeeded:

grunweg added 3 commits September 8, 2026 14:39

chore: make NonUnitalAlgHom.{range,codRestrict,rangeRestrict, equaliz…

867cec8

…er} take in a concrete morphism instead and fix associated theorems

A few more theorems

7aa4002

Also change NonUnitalSubalgebra.{map,comap}

428ce9b

grunweg added the tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip label Sep 8, 2026

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

grunweg added 3 commits September 8, 2026 15:38

More tweaks

3c9ea9b

Revert codRestrict... now it works. Hm...

6bbfa04

Broken proof!

4b9902f

eric-wieser reviewed Sep 8, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean Outdated

eric-wieser reviewed Sep 8, 2026

View reviewed changes