[Merged by Bors] - feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] by kbuzzard · Pull Request #21123 · leanprover-community/mathlib4

kbuzzard · 2025-01-27T11:07:14Z

If a monoid or semiring M acts on A then a submonoid or subsemiring of M also acts on A. But we can kill two birds with one stone by letting a SubmonoidClass of M act on A.

This is a variant of #20983 which only does one thing at once, namely generalizing many submonoid instances to submonoidclass.

A basic example of the change I'm making here is that the instance

instance smul [SMul M' α] (S : Submonoid M') : SMul S α := ...

is now generalized to the instance

variable [SMul M' α] {S' : Type*} [SetLike S' M'] (s : S')

@[to_additive]
instance : SMul s α := ...

The full list:

for SetLike, SMul for the object gives SMul for the subobject, FaithfulSMul transfers to the subobject and SMulCommClass transfers (in both variables).
For SubmonoidClass, the instances which transfer are MulAction, DistribMulAction, MulDistribMulAction and MulSemiringAction.
For SubsemiringClass, the transferring instances are SMulWithZero, MulActionWithZero and Module.

It turns out that many of the instances I was generalizing were explicitly named because they are explicitly used in mathlib, so I have kept all the original instances and proved them with inferInstance. Note that #11304 tried to take things further and delete all the now-redundant instances, and this caused slowdowns in mathlib, so I've decided just to leave everything there. It might be an interesting experiment to run TryAtEachStep on mathlib with the tactic infer_instance before and after this PR.

The refactor meant that shake could minimise some imports and then has to put some more back later; the original version of this PR imported the short new file Mathlib/Algebra/Group/Submonoid/MulAction.lean (which I made in #21067) into Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean; shake then did all the other import changes, which are reducing imports overall.

github-actions · 2025-01-27T11:08:09Z

PR summary 4e84203d6a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Submonoid.DistribMulAction	278	261	-17 (-6.12%)
Mathlib.RingTheory.OreLocalization.Basic	381	366	-15 (-3.94%)
Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero	432	429	-3 (-0.69%)
Mathlib.Algebra.Ring.Action.Subobjects	386	387	+1 (+0.26%)
Mathlib.Algebra.Ring.Subsemiring.Basic	619	618	-1 (-0.16%)

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Group.Submonoid.DistribMulAction`	-17
`Mathlib.RingTheory.OreLocalization.Basic`	-15
`Mathlib.Algebra.Group.Subgroup.Actions` `Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero`	-3
11 files `Mathlib.Algebra.Ring.Semireal.Defs` `Mathlib.Algebra.Ring.Subring.Basic` `Mathlib.Algebra.Ring.Subring.MulOpposite` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Ring.Subsemiring.Basic` `Mathlib.Algebra.Ring.Subsemiring.MulOpposite` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.Algebra.Ring.SumsOfSquares` `Mathlib.Algebra.Star.Subsemiring` `Mathlib.RingTheory.LocalRing.Subring` `Mathlib.RingTheory.SimpleRing.Field`	-1
`Mathlib.Algebra.Ring.Action.Subobjects`	1

Declarations diff

+ instance (priority := low) [AddMonoid α] [DistribMulAction M α] : DistribMulAction s α
+ instance (priority := low) [Monoid α] [MulDistribMulAction M α] : MulDistribMulAction s α
+ instance (priority := low) [MulAction M' α] : MulAction s α
+ instance (priority := low) [MulSemiringAction M R] {S : Type*} [SetLike S M] (s : S)
+ instance (priority := low) [SMul M' α] : SMul s α
+ instance (priority := low) [SMul M' β] [SMul α β] [SMulCommClass M' α β] : SMulCommClass s α β
+ instance (priority := low) [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] :
+ instance (priority := low) [SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α s β
+ instance (priority := low) {M' α : Type*} [SMul M' α] {S' : Type*}
++ instance (priority := low) [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R']
++ instance (priority := low) {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S')

You can run this locally as follows

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

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

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

No changes to technical debt.

You can run this locally as

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

grunweg · 2025-01-27T15:43:42Z

Can you change the PR title to something descriptive, please? Thanks!

kbuzzard · 2025-01-27T19:37:37Z

Yeah apologies for this. I am wondering whether the two machines I use for Lean have different behaviour when it comes to opening a PR. As you can see the commit message for the first commit was supposed to be the title of the PR and I am pretty darn sure that sometimes when I publish, this actually happens. But apparently not always -- it seems that here the title was the name of the branch rather than the commit message of the first commit.

kbuzzard · 2025-01-27T22:10:08Z

!bench

leanprover-bot · 2025-01-27T22:39:46Z

Here are the benchmark results for commit d012251.
There were significant changes against commit 2bce15b:

  Benchmark                                              Metric         Change
  ============================================================================
- ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper   instructions    36.9%
- ~Mathlib.Analysis.Normed.Lp.lpSpace                    instructions     6.4%

github-actions · 2025-01-27T22:40:10Z

File	Instructions	%
`build`	+78.444⬝10⁹	(+0.05%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper`	+15.865⬝10⁹	(+36.91%)
`Mathlib.Analysis.Normed.Lp.lpSpace`	+11.350⬝10⁹	(+6.39%)
`Mathlib.FieldTheory.Galois.Infinite`	+8.313⬝10⁹	(+12.80%)
`Mathlib.FieldTheory.Relrank`	+6.445⬝10⁹	(+5.23%)
`Mathlib.FieldTheory.PurelyInseparable`	+5.589⬝10⁹	(+3.45%)
`Mathlib.Algebra.Algebra.Subalgebra.Rank`	+4.630⬝10⁹	(+7.35%)
`Mathlib.Analysis.Complex.UpperHalfPlane.Basic`	+3.582⬝10⁹	(+5.16%)

3 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.RingTheory.LinearDisjoint`	+2.999⬝10⁹	(+1.54%)
`Mathlib.Algebra.Star.NonUnitalSubalgebra`	+2.836⬝10⁹	(+2.02%)
`Mathlib.Algebra.Algebra.NonUnitalSubalgebra`	+2.168⬝10⁹	(+2.91%)

5 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Ring.Subsemiring.Basic`	+1.690⬝10⁹	(+4.59%)
`Mathlib.Analysis.NormedSpace.BallAction`	+1.544⬝10⁹	(+2.65%)
`Mathlib.FieldTheory.Extension`	+1.331⬝10⁹	(+1.12%)
`Mathlib.Data.Array.Lemmas`	+1.85⬝10⁹	(+29.10%)
`Mathlib.FieldTheory.LinearDisjoint`	+1.79⬝10⁹	(+0.61%)

CI run

kbuzzard · 2025-01-28T11:02:21Z

Youch, this deserves further investigation.

kbuzzard · 2025-01-29T10:37:41Z

OK so the further investigation shows me that basically this idea derails certain instance searches e.g. in the theory of graded rings, where the grade 0 piece A 0 of a graded ring A might act on something, and now typeclass inference wants to find the action by finding an action of all of A. I am not convinced that the slowdown here is worth paying for, so I propose closing this. @eric-wieser do you want to argue for this PR?

kbuzzard · 2025-01-29T10:46:55Z

Actually maybe I'll try once more with low prio for the instances?

Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean

Mathlib/Algebra/Group/Submonoid/MulAction.lean

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

kbuzzard · 2025-01-29T17:39:12Z

!bench

leanprover-bot · 2025-01-29T18:08:56Z

Here are the benchmark results for commit da778f9.
There were no significant changes against commit 2bce15b.

github-actions · 2025-01-29T18:09:20Z

File	Instructions	%
`build`	+15.7⬝10⁹	(+0.00%)
`Mathlib.FieldTheory.PurelyInseparable`	+5.675⬝10⁹	(+3.51%)

2 files, Instructions +2.0⬝10⁹

File	Instructions	%
`Mathlib.Algebra.Ring.Subsemiring.Basic`	+2.656⬝10⁹	(+7.21%)
`Mathlib.FieldTheory.Relrank`	+2.82⬝10⁹	(+1.69%)

3 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper`	+1.960⬝10⁹	(+4.56%)
`Mathlib.FieldTheory.Galois.Infinite`	+1.468⬝10⁹	(+2.26%)
`Mathlib.Analysis.NormedSpace.BallAction`	+1.253⬝10⁹	(+2.15%)

CI run

kbuzzard · 2025-01-29T18:25:46Z

Ok this looks much more reasonable.

riccardobrasca · 2025-02-20T12:57:56Z

It looks reasonable to me, and the bench is good. Any reason to not merge this?

ocfnash · 2025-02-21T11:35:54Z

It looks reasonable to me, and the bench is good. Any reason to not merge this?

No reason IMHO!

bors merge

… M] (#21123) If a monoid or semiring M acts on A then a submonoid or subsemiring of M also acts on A. But we can kill two birds with one stone by letting a SubmonoidClass of M act on A.

mathlib-bors · 2025-02-21T12:18:31Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (823 commits) chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) chore: rename PushNeg.lean to Push.lean (#22108) feat: add Is{Open,Closed}Embedding.sum_elim (#22070) feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) feature(Topology/Algebra/Module/WeakBilin): Linear map from F into the topological dual of E with the weak topology (#21078) feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square (#22110) chore(ChartedSpace.lean): group constructions together (#22107) feat(CategoryTheory/MorphismProperty): more basic API (#22099) chore(Data/Fintype): split `Fintype/Card.lean` (#21840) chore(SetTheory/Cardinal/Cofinality): make `IsStrongLimit` into a structure (#21971) feat(Combinatorics/SimpleGraph): Add a theorem about cliques in induced subgraphs (#20705) ...

@pechersky

* polynomial-sequences: (558 commits) Correct the TODO to mention IsCancelAdd which does exist. Talk about strict monotonicity instead, thanks @pechersky. Mention the TODO on li generalization to semirings. One more dedent. Same injectivity twiddling for basis. nontiviality to simplify this proof, and some dedenting. Hopefully more correct injectivity lemmas matching the naming convention. Fix the empty docstring. Update Mathlib/Algebra/Polynomial/Sequence.lean Fix the variable naming. Apply suggestions from code review chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) ...

kbuzzard added 2 commits January 27, 2025 11:00

feat: extend instances from Submonoid/Subsemiring to SubmonoidClass

c658fb2

fix name

f0d94bb

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 27, 2025

unused arguments linter

e1f167c

kbuzzard changed the title ~~Kbuzzard submonoidclass instances~~ feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] Jan 27, 2025

lake shake

d012251

kbuzzard mentioned this pull request Jan 29, 2025

feat(Data/SetLike/SMul): extend scalar action to setlike subterms #20983

Closed

kbuzzard commented Jan 29, 2025

View reviewed changes

Try with low priority

19558e7

kbuzzard added the WIP Work in progress label Jan 29, 2025

long line linter

da778f9

kbuzzard removed the WIP Work in progress label Jan 29, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 11, 2025

merge master

4e84203

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 Feb 14, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Feb 21, 2025

mathlib-bors bot changed the title ~~feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M]~~ [Merged by Bors] - feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] Feb 21, 2025

mathlib-bors bot closed this Feb 21, 2025

mathlib-bors bot deleted the kbuzzard-submonoidclass-instances branch February 21, 2025 12:18

Conversation

kbuzzard commented Jan 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4e84203d6a

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Jan 27, 2025

Uh oh!

kbuzzard commented Jan 27, 2025

Uh oh!

kbuzzard commented Jan 27, 2025

Uh oh!

leanprover-bot commented Jan 27, 2025

Uh oh!

github-actions bot commented Jan 27, 2025

Uh oh!

kbuzzard commented Jan 28, 2025

Uh oh!

kbuzzard commented Jan 29, 2025

Uh oh!

kbuzzard commented Jan 29, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kbuzzard commented Jan 29, 2025

Uh oh!

leanprover-bot commented Jan 29, 2025

Uh oh!

github-actions bot commented Jan 29, 2025

Uh oh!

kbuzzard commented Jan 29, 2025

Uh oh!

riccardobrasca commented Feb 20, 2025

Uh oh!

ocfnash commented Feb 21, 2025

Uh oh!

mathlib-bors bot commented Feb 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

kbuzzard commented Jan 27, 2025 •

edited

Loading

github-actions bot commented Jan 27, 2025 •

edited

Loading