Splitting up `algebra/lie/basic.lean`

Stream: general

[Oliver Nash]

The file algebra/lie/classical.lean is currently 2224 lines long. I think it would be helpful to split it up, and I am keen to attempt this. With this in mind, I have sketched out a plan for refactoring below. I would be grateful for any feedback, even (indeed especially) if it differs wildly from what I sketch out below. Please also feel free to ignore my lengthy waffle and just offer general remarks.

[Oliver Nash]

0. Details aside:

   • Are people in favour of a refactor with the primary goal of splitting up this relatively large file?
   • Is it acceptable to attempt such a refactor with one enormous PR? This is my preference because I worry about losing momentum but of course I welcome dissenting opinions.

[Oliver Nash]

1. I propose:

   • Prioritising progress over perfection

   • Concentrating on splitting up algebra/lie/basic.lean and not worrying about the other Lie theory files files, which are:

     • algebra/lie/classical.lean
     • algebra/lie/direct_sum.lean
     • algebra/lie/skew_adjoint.lean
     • algebra/lie/universal_enveloping.lean
       and which, I claim, are in comparatively good shape anyway.

   • Trying not to include anything new. Mostly preferring to note any gaps / possible improvements which I notice, rather than bundling them up with what may well be hard-to-review changes.

[Oliver Nash]

2. I propose aiming to split algebra/lie/basic.lean into the following 10 files with
   contents approximately as indicated:

   • algebra/lie/basic.lean:

     • definitions of Lie rings, algebras, modules
     • morphisms, equivs of the above
       (this should essentially just be a truncation of algebra/lie/basic.lean at about line 442)

   • algebra/lie/subalgebra.lean:

     • definition of Lie subalgebras
     • closely related definitions / results including:
       • lie_subalgebra.incl
       • lie_subalgebra.map
       • lie_algebra.morphism.range
       • lie_algebra.equiv.of_injective
       • lie_algebra.equiv.of_eq
       • lie_algebra.equiv.of_subalgebras
   • algebra/lie/of_associative.lean:
     • Lie algebra obtained from associative algebra via commutator
     • handful of related results (assoc subalgebras yield Lie subalgebras, Abelian iff commutative, ...)
     • Lie module as Lie morphism to Lie algebra of endomorphisms (in particular adjoint action)
   • algebra/lie/submodule.lean:
     • definition of Lie submodules, Lie ideals
     • lattice structure
     • closely related definitions / results including:
       • lie_submodule.incl
       • lie_submodule.map
       • lie_submodule.comap
       • lie_algebra.morphism.ker
       • lie_algebra.morphism.ideal_range
       • lie_ideal.map_comap_eq
       • lie_ideal.comap_map_eq
   • algebra/lie/ideal_operations.lean:
     • the bracket operation of Lie ideals on Lie submodules of a Lie module
     • closely related definitions / results including:
       • lie_submodule.lie_ideal_oper_eq_linear_span
       • lie_submodule.lie_abelian_iff_lie_self_eq_bot
       • lie_ideal.comap_bracket_incl_of_le
   • algebra/lie/solvable.lean
     • definition of derived series, derived length, solvable algebras, radical
     • closely related definitions / results including:
       • lie_ideal.derived_series_eq_bot_iff
       • lie_algebra.derived_abelian_of_ideal
       • lie_algebra.radical_is_solvable
   • algebra/lie/semisimple.lean
     • definition of semisimple Lie algebras
     • closely related definitions / results including:
       • lie_algebra.is_semisimple_iff_no_solvable_ideals
       • lie_algebra.is_semisimple_of_is_simple
   • algebra/lie/nilpotent.lean:
     • definitions of lower central series, nilpotent modules
     • closely related definitions / results including:
       • lie_module.trivial_is_nilpotent
       • lie_algebra.is_solvable_of_is_nilpotent

   • algebra/lie/quotient.lean:
     Essentially a direct copy-paste of the namespace quotient blob as it stands.

   • algebra/lie/matrix.lean:
     Essentially a direct copy-paste of the section matrices blob as it stands.

[Oliver Nash]

3. I propose the following changes to the namespaces which are created in algebra/lie/basic.lean:

   • remove ring_commutator and use extant ring, algebra namespaces instead
   • rename lie_algebra.morphism → lie_hom
   • rename lie_algebra.equiv → lie_equiv

   For reference, here is a summary of all namespaces currently created in algebra/lie/basic.lean:

   • Those with correpsonding classes:
     • Type-valued:
       • lie_ring
       • lie_algebra
       • lie_ring_module
       • lie_module
     • Prop-valued:
       • lie_module.is_trivial
       • lie_module.is_irreducible
       • lie_module.is_nilpotent
       • lie_algebra.is_simple
       • lie_algebra.is_solvable
       • lie_algebra.is_semisimple
   • Those with corresponding non-class structures:
     • lie_algebra.morphism
     • lie_algebra.equiv
     • lie_module_hom
     • lie_module_equiv
     • lie_subalgebra
     • lie_submodule
   • Two other namespaces created directly (i.e., not via class or structure):
     • ring_commutator
     • lie_submodule.quotient

[Oliver Nash]

4. I propose the following bonus changes, related the the proposed namespace changes:

   • Use set_option old_structure_cmd true for lie_algebra.is_simple
   • Rename the field map_lie in the structure lie_module_hom to map_lie' so that we can swap the roles of lie_module_hom.map_lie and lie_module_hom.map_lie' for consistency with naming conventions elsewhere in Mathlib.
   • Rename the field map_lie in the structure lie_algebra.morphism to map_lie' so that if we rename lie_algebra.morphism to lie_hom we can still have a simp lemma named map_lie. Currently this is not an issue because the field map_lie lives in lie_algebra.morphism and the simp lemma map_lie lives in lie_algebra but this solution evaporates if we collapse the namespace lie_algebra.morhpism to just lie_hom as I propose above. See also this comment about enabling dot notation for map_zero which should be addressed as part of these changes.

[Mario Carneiro]

Pure file splitting can be done in one big PR, but it's best if you don't make too many side changes at the same time because it doesn't show up well in the git log

[Oliver Nash]

Thanks, that's helpful. Already that suggests perhaps I should attempt items 2, 3, 4 in three successive PRs.

[Johan Commelin]

I think this looks like a very solid plan. If possible, I would try to first make a PR that only splits things, and then touch up everything in follow-up PRs.

[Oliver Nash]

Thanks also, the more I think about it, the more I think this would be easiest for me too.

[Johan Commelin]

On the other hand, you know this part of the library best. And I don't think there a many dependencies on it (yet). So there is some leeway on the "no big PRs rule"

[Patrick Massot]

Yes, that's a very general principle. You still need to cope with namespaces and variables commands, that's enough trouble even if you only try a pure split.

[Patrick Massot]

Note this is much easier than in the pre-linter era where it was very easy to add unnecessary assumptions in such a move.

[Oliver Nash]

Great point.

[Patrick Massot]

Ideally you should be able to check that exported declarations don't change.

[Patrick Massot]

But keeping the ordering of arguments will be very difficult.

[Patrick Massot]

(I mean implicit and type class arguments).

[Oliver Nash]

Yes, understood. I think it would basically be impossible to avoid such reordering.

[Patrick Massot]

You can still try to use leanproject export to yaml to inspect that.

[Oliver Nash]

I'd love to try that!

[Oliver Nash]

Is there an easy example of how to ask leanproject to do this?

[Patrick Massot]

With some python smallish python work you could even check the yaml export up to reordering

[Patrick Massot]

I hope this is covered in the documentation

[Oliver Nash]

Ah another case of RTFM :-) I'll look now.

[Patrick Massot]

At least you can leanproject decls --help

[Patrick Massot]

There is isn't much to say: make sure your mathlib is fully built, run leanproject decls and go get a coffee (or beer, depending on your local time and CPU power).

[Patrick Massot]

That will dump a self-explanatory decls.yaml

[Oliver Nash]

I see, excellent. Thanks, I'll try that.

[Patrick Massot]

Then you can inspect this yaml using any programming language you like.

[Patrick Massot]

wait

[Oliver Nash]

Understood. I'd probably reach for Python as you suggest though I'm reluctant to commit to guaranteeing identical exports modulo reordering until I've made an attempt.

[Patrick Massot]

Maybe I'm confused by my own mess of tools.

[Patrick Massot]

Maybe the version in leanproject only dumps enough information for use in the blueprint machine.

[Patrick Massot]

If this is true then you'll need the one from leancrawler

[Oliver Nash]

Well I've kicked it off here anyway so I'll find out in the not-too-distant future.

[Patrick Massot]

And of course Rob's lean-doc also builds all the relevant information

[Oliver Nash]

OK thanks. It would be great if I could lean on such tooling to deliver a certificate that any changes I propose conform to a contract I claim. I have a free day tomorrow so I will attempt this then.

[Patrick Massot]

It's definitely doable, only a matter of time and energy to put in.

[Patrick Massot]

The version in leanproject doesn't record enough information. But leancrawler should work.

[Oliver Nash]

Thanks, I’ll definitely try it out.

[Kevin Buzzard]

I split a 2000 line ordered_group file, 1000 lines of which were about ordered monoids, into two 1000 lines files, one called ordered_group and one called ordered_monoid. I did it because I wanted to add a bunch more stuff about ordered monoids but I really could not face editing a 2000 line file. My first PR was just to break the file in two, and to add a module docstring (and no new lemmas), and I think that breaking a file into ten files is an even better idea. Then I added more ordered monoid stuff later. Note however that what I did had the rather annoying consequence that now git blame says that every lemma about ordered monoids was written by me. I don't know if this is preventable. In your case it might well be the case that the lemmas really _are_ due to you though!

[Oliver Nash]

First cut at this is now here https://github.com/leanprover-community/mathlib/pull/6141 I will pick it up again tomorrow.

[Oliver Nash]

I claim that :point_up: PR is now ready for review. In particular I took @Patrick Massot 's advice and used leancrawler to check the exported declarations do not change. To get this to work I had to make a trivial change to leancrawler which I have pushed up in this leancrawler PR.

[Johan Commelin]

@Oliver Nash thanks so much for doing this!

[Johan Commelin]

The fact that you checked this using leancrawler means that we can confidently merge this

[Oliver Nash]

Johan Commelin said:

Oliver Nash thanks so much for doing this!

Thanks. Of course I'm just clearing up my own mess ;-)

[Oliver Nash]

I am extremely happy that my enormous file-splitting PR has now been merged. Since I confined myself to simply moving things around in that PR I have a small amount of other refactoring still pending. In particular I propose the following changes to the namespaces which are created in the Lie theory corner of Mathlib:

- remove ring_commutator and use extant ring, algebra namespaces instead
- rename lie_algebra.morphism → lie_hom
- rename lie_algebra.equiv → lie_equiv

[Oliver Nash]

Does this seem like a good idea?

[Johan Commelin]

I like all three of them.

[Oliver Nash]

OK great, I'll attempt them later this afternoon and we can see how it works out.

[Oliver Nash]

I decided I'd bundle the ring_commutator change with some other tweaks in a final round of refactoring but I now have a PR with the other namespace changes: https://github.com/leanprover-community/mathlib/pull/6179