chore(Algebra): extract `Submonoid.IsLocalizationMap` #29596

Stream: PR reviews

[Johan Commelin]

chore(Algebra): extract Submonoid.IsLocalizationMap #29596

I am quite confused by the performance reports on this PR. There's a 10% regression, but @Junyan Xu and I both don't understand where it's coming from. Local measurements don't add up to this global measurement.

[Kevin Buzzard]

We're talking about this comment https://github.com/leanprover-community/mathlib4/pull/29596#issuecomment-3590610070 on github, right?

I did

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true

for both the "before" commit 09610fd and the "after" commit 8f19afb, cut and pasted the contents of the infoview into two files (because I am not very good at computers), and compared. The salient points in the diff (i.e. where things differed by more than a percent or so, at least according to my manual editing of the diff file) were:

1147c1150
< [Elab.command] [6966900.000000] open TensorProduct in
---
> [Elab.command] [10370119.000000] open TensorProduct in
...
1155c1158
< [Elab.command] [6962591.000000] instance (S : Submonoid R) [Module.FinitePresentation R M] :
---
> [Elab.command] [10365810.000000] instance (S : Submonoid R) [Module.FinitePresentation R M] :
...
1399c1402
< [Elab.command] [69497508.000000] open IsLocalizedModule in
---
> [Elab.command] [83775961.000000] open IsLocalizedModule in
...
1453c1456
< [Elab.command] [69486773.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
---
> [Elab.command] [83765226.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
...
1502c1505
< [Elab.command] [69493036.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
---
> [Elab.command] [83771489.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
...
1551c1554
< [Elab.command] [69493297.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
---
> [Elab.command] [83771750.000000] /-- Let `M` `N` be a finitely presented `R`-modules.
1600c1603
< [Elab.async] [28983120.000000] elaborating proof of Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule ▶
---
> [Elab.async] [30673007.000000] elaborating proof of Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule ▶
1604c1607
< [Elab.async] [828241.000000] Lean.addDecl ▶
---
> [Elab.async] [809897.000000] Lean.addDecl ▶
...
1793c1796
< [Elab.command] [37911723.000000] /-- Let `M` be a finitely presented `R`-module, `N` a `R`-module, `S : Submonoid R`.
---
> [Elab.command] [55835961.000000] /-- Let `M` be a finitely presented `R`-module, `N` a `R`-module, `S : Submonoid R`.
1801c1804
< [Elab.command] [37917857.000000] /-- Let `M` be a finitely presented `R`-module, `N` a `R`-module, `S : Submonoid R`.
---
> [Elab.command] [55842095.000000] /-- Let `M` be a finitely presented `R`-module, `N` a `R`-module, `S : Submonoid R`.
...
1820c1823
< [Elab.command] [8747670.000000] theorem linearEquivMapExtendScalars_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
---
> [Elab.command] [15709420.000000] theorem linearEquivMapExtendScalars_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
...
1827c1830
< [Elab.command] [8753801.000000] theorem Module.FinitePresentation.linearEquivMapExtendScalars_apply [Module.FinitePresentation R M]
---
> [Elab.command] [15715551.000000] theorem Module.FinitePresentation.linearEquivMapExtendScalars_apply [Module.FinitePresentation R M]
1834c1837
< [Elab.command] [8754057.000000] lemma Module.FinitePresentation.linearEquivMapExtendScalars_apply [Module.FinitePresentation R M]
---
> [Elab.command] [15715807.000000] lemma Module.FinitePresentation.linearEquivMapExtendScalars_apply [Module.FinitePresentation R M]
1841c1844
< [Elab.async] [3423361.000000] elaborating proof of Module.FinitePresentation.linearEquivMapExtendScalars_apply ▶
---
> [Elab.async] [3689707.000000] elaborating proof of Module.FinitePresentation.linearEquivMapExtendScalars_apply ▶
...
1852c1855
< [Elab.command] [9579825.000000] @[simp]
---
> [Elab.command] [16996922.000000] @[simp]
1860c1863
< [Elab.command] [9585958.000000] @[simp]
---
> [Elab.command] [17003055.000000] @[simp]
1869c1872
< [Elab.command] [9586216.000000] @[simp]
---
> [Elab.command] [17003313.000000] @[simp]
1878c1881
< [Elab.async] [3436681.000000] elaborating proof of Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply ▶
---
> [Elab.async] [3702937.000000] elaborating proof of Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply ▶

In particular there certainly have been some big changes here.

Because I've got everything up and running let's take a look at one of the biggest offenders: Module.FinitePresentation.linearEquivMapExtendScalars_apply. Before this is

[Elab.command] [8746016.000000] theorem linearEquivMapExtendScalars_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
        Module.FinitePresentation.linearEquivMapExtendScalars S ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
          (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
              (Localization S))
            f :=
      IsLocalizedModule.linearEquiv_apply S _ _ f ▶

and after it's

[Elab.command] [15709622.000000] theorem linearEquivMapExtendScalars_apply [Module.FinitePresentation R M] (f : M →ₗ[R] N) :
        Module.FinitePresentation.linearEquivMapExtendScalars S ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) =
          (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
              (Localization S))
            f :=
      IsLocalizedModule.linearEquiv_apply S _ _ f ▶

which is nearly twice as long. Taking apart the traces, one place where they diverge is here.

Before:

              [Meta.synthInstance] [210793.000000] ✅️ IsLocalization S (Localization S) ▼
                [whnf] [28.000000] Non-easy whnf: IsLocalization S (Localization S)
                [whnf] [28.000000] Non-easy whnf: IsLocalization S (Localization S)
                [] [517.000000] new goal IsLocalization S (Localization S) ▶
                [] [138685.000000] ✅️ apply @Localization.isLocalization to IsLocalization S (Localization S) ▶
                [isDefEq] [69702.000000] ✅️ IsLocalization S (Localization S) =?= IsLocalization S (Localization S) ▶
                [check] [1183.000000] ✅️ Localization.isLocalization ▶
              [Meta.isDefEq] [78550.000000] ✅️ ?m.135 =?= Localization.isLocalization ▶

After:

              [Meta.synthInstance] [1551976.000000] ✅️ IsLocalization S (Localization S) ▼
                [whnf] [131.000000] Non-easy whnf: IsLocalization S (Localization S) ▶
                [whnf] [131.000000] Non-easy whnf: IsLocalization S (Localization S) ▶
                [] [1294.000000] new goal S.IsLocalizationMap ⇑(algebraMap R (Localization S)) ▶
                [] [1247685.000000] ✅️ apply @Localization.isLocalization to S.IsLocalizationMap ⇑(algebraMap R (Localization S)) ▶
                [isDefEq] [300550.000000] ✅️ S.IsLocalizationMap ⇑(algebraMap R (Localization S)) =?= IsLocalization S (Localization S) ▶
                [check] [1183.000000] ✅️ Localization.isLocalization ▶
              [Meta.isDefEq] [276737.000000] ✅️ ?m.135 =?= Localization.isLocalization ▶

The traces appear to diverge at this point: the "new goal" is more complex in the "after" commit and typeclass inference takes a lot longer to solve it.

In short, there is definitely a difference between the two commits and it seems that typeclass inference is behaving differently.

[Kevin Buzzard]

Looking at the contents of the PR, could this be the culprit:
Screenshot from 2025-12-03 01-28-56.png

[Junyan Xu]

Thanks for the diagnosis! IsLocalization is Prop-valued so I don't think this makes a difference. I realized that I could make IsLocalization extend IsLocalizationMap (instead of an abbrev of IsLocalizationMap) and hopefully that alleviates the performance issue.

[Junyan Xu]

Definitely the IsLocalization instance synthesis gets much slower, but also the Module and IsScalarTower instance syntheses, and I'm puzzled what could have affected those ...
image.png

[Junyan Xu]

Oh I see, LocalizedModule.isModule takes a IsLocalization instance.

[Junyan Xu]

extends doesn't work well; it blocks the name IsLocalization.surj etc.

invalid declaration name `IsLocalization.surj`, structure `IsLocalization` has field `surj`

but doesn't add IsLocalization.surj to the environment. If it doesn't block the name so I could add a version with different argument explicitness that would be great. Looks like the best solution now is to make IsLocalization a structure with IsLocalizationMap as the only field.

[Junyan Xu]

Figured out a trick to solve this:

/-- An auxiliary typeclass to avoid auto-generated declarations
under the `IsLocalization` namespace. -/
class IsLocalization' : Prop extends M.IsLocalizationMap (algebraMap R S)
abbrev IsLocalization := @IsLocalization'