[Merged by Bors] - chore: Move power lemmas earlier by YaelDillies · Pull Request #12736 · leanprover-community/mathlib4

YaelDillies · 2024-05-07T18:44:44Z

Move a bunch of pow lemmas from Algebra.Group.Commute.Defs and Algebra.GroupPower.Basic to Algebra.Group.Defs and Algebra.Group.Basic with little to no changes to their proofs.

I would like some opinions on what should go in Algebra.Group.Defs vs Algebra.Group.Basic.

Move a bunch of `pow` lemmas from `Algebra.Group.Commute.Defs` and `Algebra.GroupPower.Basic` to `Algebra.Group.Defs` and `Algebra.Group.Basic` with little to no changes to their proofs.

Vierkantor

So if I have it right, the split is essentially:

lemmas about pow and monoid operations go to Defs
lemmas about zpow or group operations go to Basic

? I suppose that is as good a criterion as any.

Again I'm not convinced that making a huge Group.Basic / Group.Defs file is the best way to go but I agree that moving the power lemmas upstream is a good idea. So I'm still willing to be convinced. Is the reason that you want to put these lemmas there because that ensures everyone imports them, or something else?

Mathlib/Algebra/Group/Commute/Defs.lean

Mathlib/Algebra/Group/Basic.lean

YaelDillies · 2024-05-08T09:05:46Z

So if I have it right, the split is essentially:

lemmas about pow and monoid operations go to Defs

lemmas about zpow or group operations go to Basic

? I suppose that is as good a criterion as any.

I don't really think that's true. If anything, the pow/zpow split is a result of zpow lemmas generally being harder to prove than their pow counterpart and are less "foundational" (in that they show up in fewer proofs of basic stuff, in particular default structure fields and forgetful inheritance instances). The actual way I did the split was to put in Defs results that looked like existing lemmas from Defs so long as they didn't require lemmas in Basic, and the rest went to Basic. I'm not super happy with the reasoning, but rearranging Defs and Basic is probably a job for another PR.

Is the reason that you want to put these lemmas there because that ensures everyone imports them, or something else?

Basically yes. More precisely, I want mul and pow to be on an equal footing import-wise because they mathematically are and because the current situation pushes people to consider pow to be a more advanced concept and reflect that in their file structure further downstream: See all the files called Power and the folder Algebra.GroupPower. For now, I am waging war against the latter, because it is the mother of almost all import oddities I have found in the past two months, eg what I am fixing in #11863 or the import that @grunweg tried removing in #12714.

I'm not convinced that making a huge Group.Basic / Group.Defs file is the best way to go

To me, that's a second-order problem. Once we have put mul and pow on an equal footing import-wise, we can think about stratifying the files about them, but not along the mul vs pow axis. I don't have a specific suggestion there, but that thread gave a few ideas. All I want is for this brain-storming to happen after I have annihilated Algebra.GroupPower, so that we don't overfit the file structure to a powerless library.

After #12736, `powMonoidHom` and `zpowGroupHom` can move to `Algebra.Group.Hom.Basic` at no cost. This PR moves them and deletes the now empty `Algebra.GroupPower.Hom`.

After #12736, all lemmas in `Algebra.GroupWithZero.Power` can move to the earlier files where they belong. The changes to their proofs are minimal. It's just a matter of using the new Lean 4 `Nat`- and `Int`-specific lemmas instead of the generic algebraic order ones.

Vierkantor

Alright. Your follow-up PRs have convinced me this is a good idea overall (although I hope that cleaning up Group.Defs and Group.Basic isn't an empty idea!)

bors r+

Move a bunch of `pow` lemmas from `Algebra.Group.Commute.Defs` and `Algebra.GroupPower.Basic` to `Algebra.Group.Defs` and `Algebra.Group.Basic` with little to no changes to their proofs.

mathlib-bors · 2024-05-13T11:07:35Z

Pull request successfully merged into master.

Build succeeded: