refactor of group_theory.coset and friends

Stream: general

[Scott Morrison]

group_theory.coset and its descendants still import deprecated.subgroup.

[Scott Morrison]

Does anyone plan to fix this?

[Scott Morrison]

I just went through group_theory.coset and managed to convert everything over except for one broken proof I'm still thinking about

[Scott Morrison]

but there are then many more files which break

[Scott Morrison]

I'm also losing enthusiasm...

[Scott Morrison]

unfortunately this refactor is also getting in the way of other things I want to do (e.g. proving that Ab is an abelian category, so we can start doing homological algebra), where I really don't want to layer more work on top of deprecated stuff.

[Scott Morrison]

So... any enthusiasm for helping with / doing this refactor? :-)

[Johan Commelin]

I would, if it weren't for the fact that I have three maths papers that I should be working on, a workshop coming up next week, and two exams that I need to design.

[Scott Morrison]

Sounds good. :-) We can get there eventually!

[Scott Morrison]

I've pushed a branch quotient_group_refactor, which anyone should feel invited to hack on. :-)

[Scott Morrison]

In fact, I made it into a WIP PR, as #3321

[Kevin Buzzard]

I can help. I also want to see the back of this.

[Kevin Buzzard]

Ok I've finished the day job and I'm starting

[Kevin Buzzard]

The broken proof seems to be a wacky bug -- defining subgroup.subtype clobbers subtype notation in the namespace: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/subgroup.2Esubtype.20clobbers.20subtype.20notation.20in.20namespace/near/203296154

[Yury G. Kudryashov]

I think that quotient groups should use con

[Yury G. Kudryashov]

This way we can prove several general facts about cons and use the same type for group and mood quotients

[Yury G. Kudryashov]

E.g., we actually don't need the group structure for abelianization

[Kevin Buzzard]

Can you explain more? I don't know what con is and I've been struggling through quotient groups this evening. Still not quite done.

[Kevin Buzzard]

@Scott Morrison I got up to the first isomorphism theorem in quotient_group but didn't finish it. There are many many files which import this stuff. Maybe it's possible to add the deprecated import back once you've got what you need for Ab?

[Yury G. Kudryashov]

src#con is an equivalence relation on a monoid such that x ≈ y and x' ≈ y' implies x * x' ≈y * y'.

[Yury G. Kudryashov]

In other words, it is a setoid s such that (*) lifts to s.quotient.

[Yury G. Kudryashov]

We have a complete_lattice structure on cons, so we can define ab_con (M : Type*) [monoid M] := Inf {r : con M | ∀ a b, r (a * b) (b * a)} and abelianization M := (ab_con M).quotient.

[Yury G. Kudryashov]

This way we get the universal property for free.

[Yury G. Kudryashov]

For s : submonoid M we can define s.con := Inf {r : con M | ∀ a ∈ s, r a 1}, and we'll know for sure that f : M →* N such that ∀ x ∈ s, f x = 1 lifts to f : s.con.quotient →* N.

[Yury G. Kudryashov]

For a normal subgroup we'll have s.con x y = y⁻¹ * x ∈ s.

[Sebastien Gouezel]

Yury G. Kudryashov said:

In other words, it is a setoid s such that (*) lifts to s.quotient.

Argh, please don't use lift like that, it takes way too long to parse :)

[Scott Morrison]

I made a bit more progress on this. There's just one more sorry in quotient_group. (There was a weird problem with an include statement that went on for too long.) I also fixed a few other files.

[Kevin Buzzard]

(deleted)

[Scott Morrison]

I made some further progress. group_theory.abelianization and group_theory.presented_group are now good.

[Scott Morrison]

free_abelian_group has two broken proofs

[Kevin Buzzard]

What is the goal here? For abelianisation I noticed that it was importing the deprecated subgroups but we broke it anyway because of the change in syntax for quotients. On the other hand presumably some broken files can just be fixed by adding the deprecated imports back

[Kevin Buzzard]

o_O the major subgroup refactor might have finished! There must still be some deprecated imports here and there, but the key point is that (a) mathlib compiles (hopefully -- I just merged master) and (b) the quotient group file now uses bundled subgroups. I'm just waiting to see if mathlib compiles after the merge. There will probably be a few more PR's before we can completely remove the deprecated imports, but quotient groups are now using bundled subgroups in the quotient_group_refactor branch, and a lot of files were using quotient groups and have now also been updated.

What happened here was that about a year ago I got sick of people saying "subgroups should be bundled and it will be a major refactor" but nobody was doing the refactor, and I wanted bundled subgroups anyway, and so encouraged some Imperial undergrads (Amelia and Jason) to bundle submonoids/subgroups regardless, and persuaded people to let them coexist in mathlib with the unbundled classes. This was a bit of a weird way to go about things -- for example when Mario refactored modules he just did everything in one go. So for a while now we've had two ways of dealing with subgroups, and newer mathlib files have been able to use the newer bundled approach, whilst some files needed the older approach. When Scott wanted to prove that Ab was an abelian category, he wanted to use quotient groups, which unfortunately were still using the old approach, Scott couldn't face building on what should be deprecated code, so he bit the bullet and started the refactor. Of course changing the quotient group file basically broke a bunch of mathlib -- the main reason people were still using unbundled subgroups was that they needed quotients.

Another Imperial student, Ashvni, is currently bundling subrings (I think that writing these bundled classes is quite a good way to learn Lean). Hopefully the refactor of these will be less painful.

[Scott Morrison]

In fact, deprecated.subgroup is now only imported anywhere in mathlib by ring_theory.subring, so when Ashvni gets to a PR on bundling subrings, we should be ready to drop this file entirely!

[Scott Morrison]

Nice work on the refactor!

[Scott Morrison]

We should definitely make sure the 3rd iso theorem gets proved soon. :-)

[Mario Carneiro]

Let's not remove the deprecated files for a while yet, even after all uses are gone

[Kevin Buzzard]

I just placated the linter.