chore: make RingHom.comp implicit_reducible by sgouezel · Pull Request #38315 · leanprover-community/mathlib4

sgouezel · 2026-04-20T20:56:05Z

This change is useful to solve diamonds in #38451, and doesn't have bad performance impact (in fact, a noticeable improvement, but that's not the main reason for the PR).

Discussion at #mathlib4 > backward.isDefEq.respectTransparency: bundled homomorphisms @ 💬

mathlib-bors · 2026-04-20T20:56:13Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

github-actions · 2026-04-20T20:57:07Z

PR summary 79540a76d4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

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

github-actions · 2026-04-20T20:57:28Z

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

feat (feature)
fix (bug fix)
doc (documentation)
style (formatting, missing semicolons, ...)
refactor
test (when adding missing tests)
chore (maintain)
perf (performance improvement, optimization, ...)
ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

Data/Nat/Basic
Algebra/Group/Defs
Topology/Constructions

<subject> has the following constraints:

do not capitalize the first letter
no dot(.) at the end
use imperative, present tense: "change" not "changed" nor "changes"

sgouezel · 2026-04-21T05:09:09Z

!radar

leanprover-radar · 2026-04-21T05:09:27Z

Benchmark results for 64837c4 against 79540a7 are in. There are significant results. @sgouezel

✅ build//instructions: -136.9G (-0.08%)

Large changes (1✅)

✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -83.2G (-33.18%)

Medium changes (2✅)

✅ build/module/Mathlib.Algebra.Category.BialgCat.Monoidal//instructions: -11.6G (-17.72%)
✅ build/module/Mathlib.AlgebraicGeometry.GammaSpecAdjunction//instructions: -5.7G (-5.84%)

Small changes (11✅, 3🟥)

🟥 build/module/Mathlib.Algebra.Ring.TransferInstance//instructions: +243.4M (+2.34%)
✅ build/module/Mathlib.AlgebraicGeometry.SpreadingOut//instructions: -609.1M (-2.19%)
✅ build/module/Mathlib.AlgebraicGeometry.ValuativeCriterion//instructions: -672.1M (-2.78%)
🟥 build/module/Mathlib.Data.Matrix.Auto//instructions: +134.0M (+3.60%)
✅ build/module/Mathlib.FieldTheory.CardinalEmb//instructions: -2.3G (-1.87%)
✅ build/module/Mathlib.FieldTheory.Extension//instructions: -2.3G (-3.05%)
✅ build/module/Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits//instructions: -916.7M (-3.41%)
✅ build/module/Mathlib.RingTheory.Bialgebra.Hom//instructions: -782.2M (-2.79%)
✅ build/module/Mathlib.RingTheory.Etale.QuasiFinite//instructions: -9.3G (-3.19%)
✅ build/module/Mathlib.RingTheory.GradedAlgebra.AlgHom//instructions: -966.2M (-3.30%)
✅ build/module/Mathlib.RingTheory.TensorProduct.Maps//instructions: -9.1G (-4.69%)
✅ build/module/Mathlib.RingTheory.WittVector.IsPoly//instructions: -647.3M (-2.35%)
✅ build/module/Mathlib.Tactic.Linarith//instructions: -297.4M (-6.51%)
🟥 build/module/Mathlib.Tactic.MinImports//instructions: +132.1M (+2.63%)

robin-carlier · 2026-04-24T16:40:54Z

Can you add some context as to what is happening in the PR description? Namely, is there a good explanation for why this gives such a speedup?

(But really nice!!)

kbuzzard · 2026-04-24T20:24:23Z

Should NonUnitalRingHom.comp (same file) also be @[implicit_reducible]?

sgouezel · 2026-04-24T20:56:09Z

I tried this because I need it to fix diamonds in #38451 (around Algebra structures, which are often constructed composing ring homs). I expected a performance hit, not a performance gain. My guess is that when Lean can unfold the ring homs, it realizes much more quickly that some instances are defeq -- and also maybe it helps for some unification questions. But that's just a guess, I haven't investigated the traces in detail.

Two experiments I've done is try making LinearMap.comp implicit-reducible, and try making ContinuousLinearMap.comp implicit-reducible. For both, the outcome was a minor performance hit. We could try with other classes as well, but it seems to me that it's quite specific to composition of ring homs because they show up in Algebra instances.

eric-wieser · 2026-04-24T23:13:39Z

I think we want a principled solution here; either we:

make every .comp and .id and funLeft and compLeft and ... implicit_reducible
declare that typeclasses must never use any of these
declare that something is wrong with the new reducibility behavior

eric-wieser · 2026-04-24T23:14:56Z

Note that this has already been discussed twice on Zulip, it would be best to find those discussions before re-hashing them here.

kbuzzard · 2026-04-25T11:17:29Z

Here's a diagnosis of the speedup in algebraic geometry. This line

  erw [SheafedSpace.comp_hom_c_app, toOpen_comp_comap_assoc]

(around line 300 of the GammaSpecAdjunction file, in the proof of comp_ring_hom_ext) has gone from 30074054 mheartbeats to 8264781. The culprit is this: on master we have

[Meta.isDefEq] [22949078.000000] ❌️ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
                          X.toToΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r) ≫
                            X.presheaf.map (eqToHom ⋯) =?= X.presheaf.map ?f ≫ X.presheaf.map ?g ▶

which is an extremely long failure. On this branch we have

[1679321.000000] ❌️ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
                          X.toToΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r) ≫
                            X.presheaf.map (eqToHom ⋯) =?= X.presheaf.map ?f ≫ X.presheaf.map ?g ▶

kbuzzard · 2026-04-25T11:54:28Z

The big speed-up in Mathlib.Algebra.Category.CommAlgCat.Monoidal seems to be all down to one declaration -- instance : BraidedCategory (CommAlgCat.{u} R). Elaboration is the same on the branch and master, but typechecking is abysmal on master:

[Elab.async] [1679650.000000] ✅️ Lean.addDecl ▼
  [Kernel] [1679597.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_1] 
[Elab.async] [1683173.000000] ✅️ Lean.addDecl ▼
  [Kernel] [1683113.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_2] 
[Elab.async] [64120523.000000] ✅️ Lean.addDecl ▼
  [Kernel] [64120442.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_3] 
[Elab.async] [69206222.000000] ✅️ Lean.addDecl ▼
  [Kernel] [69206169.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_4]

and is much better on this branch

[Elab.async] [447933.000000] ✅️ Lean.addDecl ▼
  [Kernel] [447880.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_1] 
[Elab.async] [449989.000000] ✅️ Lean.addDecl ▼
  [Kernel] [449936.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_2] 
[Elab.async] [1523761.000000] ✅️ Lean.addDecl ▼
  [Kernel] [1523708.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_3] 
[Elab.async] [1543964.000000] ✅️ Lean.addDecl ▼
  [Kernel] [1543911.000000] ✅️ typechecking declarations [CommAlgCat.instBraidedCategory._proof_4]

(note in particular the two last proofs are typechecking 40x faster). This is the sort of problem where it's very hard for me to go any further and if you ask a core person what's going on they'll ask for a mathlib-free minimisation, which is extremely difficult to pull off.

In particular, I think this is a rather bad explanation for why this gives such a speedup.

Edit: apparently a monoidal category is some data and then ten axioms, all of whose proofs are omitted in this instance, so all of which are being solved by cat_disch which calls aesop which is for some reason creating very kernel-unfriendly proofs on master, and the change in this PR makes this better.

Edit: replacing the proof of pentagon with intros; ext <;> simp (which takes 100M mHeartbeats) doesn't give much speedup but does reveal a bit more about what's going on -- there are many many typeclass unification slowdowns coming from

[] [84093.000000] ✅️ leftAlgebra =?= instAlgebra ▶

Probably one reason for the speedup in this branch is that on master we have

[] [563075.000000] ✅️ AlgHom.comp ?φ₁
                            ?φ₂ =?= (((Algebra.TensorProduct.map (AlgHom.id R ↑W) ↑(assoc R R R ↑X ↑Y ↑Z)).comp
                                    ↑(assoc R R R (↑W) (↑X ⊗[R] ↑Y) ↑Z)).comp
                                (Algebra.TensorProduct.map (↑(assoc R R R ↑W ↑X ↑Y)) (AlgHom.id R ↑Z))).comp
                            includeLeft ▶

kbuzzard · 2026-04-25T13:02:45Z

I think that the conclusion here is that the change in this PR generally has a negligible effect on mathlib (which is not a reason either for or against merging) except that there happen to be two or three slow definitions in mathlib for which the change has a huge effect; hence if it is decided not to merge this PR then one could make the transparency change locally for these declarations and still reap the speed benefits.

The declaration affected in Mathlib.Algebra.Category.BialgCat.Monoidal is BialgCat.MonoidalCategory.inducingFunctorData, where on master we have things like

[Elab.async] [5761139.000000] ✅️ Lean.addDecl ▼
  [Kernel] [5761073.000000] ✅️ typechecking declarations [BialgCat.MonoidalCategory.inducingFunctorData._proof_5]

and on this branch

[Elab.async] [522387.000000] ✅️ Lean.addDecl ▼
  [Kernel] [522321.000000] ✅️ typechecking declarations [BialgCat.MonoidalCategory.inducingFunctorData._proof_5]

, an over 10x speedup.

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

try

64837c4

sgouezel marked this pull request as draft April 20, 2026 20:56

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

sgouezel changed the title ~~try~~ chore: make RingHom.comp implicit_reducible Apr 21, 2026

sgouezel marked this pull request as ready for review April 21, 2026 13:38

sgouezel mentioned this pull request Apr 24, 2026

chore: fix diamonds around R and C structures #38451

Open

3 tasks

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026

sgouezel removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026

sgouezel mentioned this pull request Apr 25, 2026

chore: make RingHom.id implicit-reducible #38509

Open

themathqueen reviewed Apr 25, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Ring/Hom/Defs.lean Outdated

Update Mathlib/Algebra/Ring/Hom/Defs.lean

3cce977

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

Conversation

sgouezel commented Apr 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-bors Bot commented Apr 20, 2026

Uh oh!

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

Uh oh!

PR summary 79540a76d4

Import changes for modified files

Declarations diff

Uh oh!

github-actions Bot commented Apr 20, 2026

🚨 PR Title Needs Formatting

Uh oh!

sgouezel commented Apr 21, 2026

Uh oh!

leanprover-radar commented Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robin-carlier commented Apr 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kbuzzard commented Apr 24, 2026

Uh oh!

sgouezel commented Apr 24, 2026

Uh oh!

eric-wieser commented Apr 24, 2026

Uh oh!

eric-wieser commented Apr 24, 2026

Uh oh!

kbuzzard commented Apr 25, 2026

Uh oh!

kbuzzard commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kbuzzard commented Apr 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

sgouezel commented Apr 20, 2026 •

edited

Loading

github-actions Bot commented Apr 20, 2026 •

edited

Loading

leanprover-radar commented Apr 21, 2026 •

edited

Loading

robin-carlier commented Apr 24, 2026 •

edited

Loading

kbuzzard commented Apr 25, 2026 •

edited

Loading

kbuzzard commented Apr 25, 2026 •

edited

Loading