Zulip Chat Archive
Stream: general
Topic: Splitting up `algebra/lie/basic.lean`
Oliver Nash (Feb 08 2021 at 21:08):
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 (Feb 08 2021 at 21:09):

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 (Feb 08 2021 at 21:09):

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 hardtoreview changes.
Oliver Nash (Feb 08 2021 at 21:09):

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 ofalgebra/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 copypaste of thenamespace quotient
blob as it stands. 
algebra/lie/matrix.lean
:
Essentially a direct copypaste of thesection matrices
blob as it stands.

Oliver Nash (Feb 08 2021 at 21:09):

I propose the following changes to the namespaces which are created in
algebra/lie/basic.lean
: remove
ring_commutator
and use extantring
,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 nonclass 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
 remove
Oliver Nash (Feb 08 2021 at 21:10):

I propose the following bonus changes, related the the proposed namespace changes:
 Use
set_option old_structure_cmd true
forlie_algebra.is_simple
 Rename the field
map_lie
in the structurelie_module_hom
tomap_lie'
so that we can swap the roles oflie_module_hom.map_lie
andlie_module_hom.map_lie'
for consistency with naming conventions elsewhere in Mathlib.  Rename the field
map_lie
in the structurelie_algebra.morphism
tomap_lie'
so that if we renamelie_algebra.morphism
tolie_hom
we can still have asimp
lemma namedmap_lie
. Currently this is not an issue because the fieldmap_lie
lives inlie_algebra.morphism
and thesimp
lemmamap_lie
lives inlie_algebra
but this solution evaporates if we collapse the namespacelie_algebra.morhpism
to justlie_hom
as I propose above. See also this comment about enabling dot notation formap_zero
which should be addressed as part of these changes.
 Use
Mario Carneiro (Feb 08 2021 at 21:11):
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 (Feb 08 2021 at 21:11):
Thanks, that's helpful. Already that suggests perhaps I should attempt items 2, 3, 4 in three successive PRs.
Johan Commelin (Feb 08 2021 at 21:13):
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 followup PRs.
Oliver Nash (Feb 08 2021 at 21:14):
Thanks also, the more I think about it, the more I think this would be easiest for me too.
Johan Commelin (Feb 08 2021 at 21:14):
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 (Feb 08 2021 at 21:14):
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 (Feb 08 2021 at 21:15):
Note this is much easier than in the prelinter era where it was very easy to add unnecessary assumptions in such a move.
Oliver Nash (Feb 08 2021 at 21:15):
Great point.
Patrick Massot (Feb 08 2021 at 21:16):
Ideally you should be able to check that exported declarations don't change.
Patrick Massot (Feb 08 2021 at 21:16):
But keeping the ordering of arguments will be very difficult.
Patrick Massot (Feb 08 2021 at 21:16):
(I mean implicit and type class arguments).
Oliver Nash (Feb 08 2021 at 21:16):
Yes, understood. I think it would basically be impossible to avoid such reordering.
Patrick Massot (Feb 08 2021 at 21:16):
You can still try to use leanproject export to yaml to inspect that.
Oliver Nash (Feb 08 2021 at 21:17):
I'd love to try that!
Oliver Nash (Feb 08 2021 at 21:17):
Is there an easy example of how to ask leanproject
to do this?
Patrick Massot (Feb 08 2021 at 21:17):
With some python smallish python work you could even check the yaml export up to reordering
Patrick Massot (Feb 08 2021 at 21:17):
I hope this is covered in the documentation
Oliver Nash (Feb 08 2021 at 21:18):
Ah another case of RTFM :) I'll look now.
Patrick Massot (Feb 08 2021 at 21:18):
At least you can leanproject decls help
Patrick Massot (Feb 08 2021 at 21:19):
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 (Feb 08 2021 at 21:19):
That will dump a selfexplanatory decls.yaml
Oliver Nash (Feb 08 2021 at 21:20):
I see, excellent. Thanks, I'll try that.
Patrick Massot (Feb 08 2021 at 21:20):
Then you can inspect this yaml using any programming language you like.
Patrick Massot (Feb 08 2021 at 21:21):
wait
Oliver Nash (Feb 08 2021 at 21:21):
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 (Feb 08 2021 at 21:21):
Maybe I'm confused by my own mess of tools.
Patrick Massot (Feb 08 2021 at 21:21):
Maybe the version in leanproject
only dumps enough information for use in the blueprint machine.
Patrick Massot (Feb 08 2021 at 21:22):
If this is true then you'll need the one from leancrawler
Oliver Nash (Feb 08 2021 at 21:22):
Well I've kicked it off here anyway so I'll find out in the nottoodistant future.
Patrick Massot (Feb 08 2021 at 21:22):
And of course Rob's leandoc also builds all the relevant information
Oliver Nash (Feb 08 2021 at 21:24):
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 (Feb 08 2021 at 21:32):
It's definitely doable, only a matter of time and energy to put in.
Patrick Massot (Feb 08 2021 at 21:34):
The version in leanproject
doesn't record enough information. But leancrawler should work.
Oliver Nash (Feb 08 2021 at 21:36):
Thanks, I’ll definitely try it out.
Kevin Buzzard (Feb 08 2021 at 22:18):
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 (Feb 09 2021 at 21:11):
First cut at this is now here https://github.com/leanprovercommunity/mathlib/pull/6141 I will pick it up again tomorrow.
Oliver Nash (Feb 10 2021 at 17:38):
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 (Feb 10 2021 at 18:11):
@Oliver Nash thanks so much for doing this!
Johan Commelin (Feb 10 2021 at 18:12):
The fact that you checked this using leancrawler means that we can confidently merge this
Oliver Nash (Feb 10 2021 at 18:24):
Johan Commelin said:
Oliver Nash thanks so much for doing this!
Thanks. Of course I'm just clearing up my own mess ;)
Oliver Nash (Feb 11 2021 at 12:34):
I am extremely happy that my enormous filesplitting 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 (Feb 11 2021 at 12:34):
Does this seem like a good idea?
Johan Commelin (Feb 11 2021 at 12:40):
I like all three of them.
Oliver Nash (Feb 11 2021 at 12:40):
OK great, I'll attempt them later this afternoon and we can see how it works out.
Oliver Nash (Feb 11 2021 at 14:40):
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/leanprovercommunity/mathlib/pull/6179
Last updated: Aug 03 2023 at 10:10 UTC