mathlib3

f961b280 - chore(deprecated/*): Make deprecated classes into structures (#8178)

chore(deprecated/*): Make deprecated classes into structures (#8178) I make the deprecated classes `is_group_hom`, `is_subgroup`, ... into structures, and delete some deprecated constructions which become inconvenient or essentially unusable after these changes. I do not completely remove all deprecated imports in undeprecated files, however I push these imports much further towards the edges of the hierarchy. More detailed comments about what is going on here: In the `src/deprecated/` directory, classes such as `is_ring_hom` and `is_subring` are defined (and the same for groups, fields, monoids...). These are predicate classes on functions and sets respectively, formerly used to handle ring morphisms and subrings before both were bundled. Amongst other things, this PR changes all the relevant definitions from classes to structures and then picks up the pieces (I will say more about what this means later). Before I started on this refactor, my opinion was that these classes should be turned into structures, but should be left in mathlib. After this refactor, I am now moving towards the opinion that it would be no great loss if these structures were removed completely -- I do not see any time when we really need them. The situation I previously had in mind where the substructures could be useful is if one is (in the middle of a long tactic proof) defining an explicit subring of a ring by first defining it as a subset, or `add_subgroup` or whatever, and then doing some mathematics to prove that this subset is closed under multiplication, and hence proving that it was a subring after all. With the old approach this just involves some `S : set R` with more and more properties being proved of it and added to the type class search as the proof progresses. With the bundled set-up, we might have `S : set R` and then later on we get `S_subring : subring R` whose underlying subset equals S, and then all our hypotheses about `S` built up during the proof can no longer be used as rewrites, we need to keep rewriting or `change`ing `x \in S_subring` to `x \in S` and back again. This issue showed up only once in the refactor, in `src/ring_theory/integral_closure.lean`, around line 230, where I refactored a proof to avoid the deprecated structures and it seemed to get a bit longer. I can definitely live with this. One could imagine a similar situation with morphisms (define f as a map between rings, and only later on prove that it's a ring homomorphism) but actually I did not see this situation arise at all. In fact the main issue I ran into with morphism classes was the following (which showed up 10 or so times): there are many constructions in mathlib which actually turn out to be, or (even worse) turn out under some extra assumptions to be, maps which preserve some structure. For example `multiset.map (f : X -> Y) : multiset X -> multiset Y` (which was in mathlib since it was born IIRC) turns out to be an add_group_hom, once the add_group structure is defined on multisets. So here I had a big choice to make: should I actually rename `multiset.map` to be `private multiset.map_aux` and then redefine `multiset.map` to be the `add_monoid_hom`? In retrospect I think that there's a case for this. In fact `data.multiset.basic` is the biggest source of these issues -- `map` and `sum` and `countp` and `count` are all `add_monoid_hom`s. I did not feel confident about ripping out these fundamental definitions so I made four new ones, `map_add_monoid_hom`, `sum_add_monoid_hom` etc. The disadvantage with this approach is that again rewrites get a bit more painful: some lemma which involves `map` may need to be rewritten so that it involves `map_add_monoid_hom` so that one can apply `add_monoid_hom.map_add`, and then perhaps rewritten back so that one can apply other rewrites. Random example: line 43 of `linear_algebra.lagrange`, where I have to rewrite `coe_eval_ring_hom` in both directions. Let me say that I am most definitely open to the idea of renaming `multiset.map_add_monoid_hom` to `multiset.map` and just nuking our current `multiset.map` or making it private or `map_aux` or whatever but we're already at 92 files changed so it might be best to get this over with and come up with a TODO list for future tidy-ups. Another example: should the fields of `complex` be `re'` and `im'`, and `complex.re` be redefined as the R-linear map? Right now in mathlib we only use the fact that it's an `add_group_hom`, and I define `re_add_group_hom` for this. Note however one can not always get away with this renaming trick, for example there are instances when a certain fundamental construction only preserves some structure under additional conditions -- for example `has_inv.inv` on groups is only a group homomorphism when the underlying group is abelian (and the same for `pow` and `gpow`). In the past this was dealt with by a typeclass `is_group_hom` on `inv` which fired in the presence of a `comm_group` but not otherwise; now this has to be dealt with by a second definition `inv_monoid_hom` whose underlying function is `inv`. You can't just get away with applying the proof of `inv (a * b) = inv a * inv b` when you need it, because sometimes you want to apply things like `monoid_hom.map_prod` which needs a `monoid_hom` as input, so won't work with `inv`: you need to rewrite one way, apply `monoid_hom.map_prod` and then rewrite back the other way now :-/ I would say that this was ultimately the main disadvantage of this approach, but it seems minor really and only shows up a few times, and if we go ahead with the renaming plan it will happen even fewer times. I had initially played with the idea of just completely removing all deprecated imports in non-deprecated files, but there were times near the end when I just didn't feel like it (I just wanted it to be over, I was scared to mess around in `control` or `test`), so I removed most of them but added some deprecated imports higher up the tree (or lower down the tree, I never understand which way up this tree is, I mean nearer the leaves -- am I right in that computer scientists for some reason think the root of a tree is at the top?). It will not be too hard for an expert to remove those last few deprecated imports in src outside the `deprecated` directory in subsequent PR's, indeed I could do it myself but I might I might need some Zulip help. Note: it used to be the case that `subring` imported `deprecated.subring`; this is now the other way around, which is much more sensible (and matches with submonoid). Outside the deprecated directory, there are only a few deprecated imports: `control.fold` (which I don't really want to mess with),`group_theory.free_abelian_group` (there is a bunch of `seq` stuff which I am not sure is ever used but I just couldn't be bothered, it might be the sort of refactor which someone finds interesting or fun though), `ring_theory.free_comm_ring` (this file involves some definitional abuse which either needs to be redone "mathematically" or rewritten to work with bundled morphisms) and `topology.algebra.uniform_group` (which I think Patrick is refactoring?) and a test file. If you look at the diffs you see that various things are deleted (lots of `is_add_monoid_hom foo` proofs), but many of these deletions come with corresponding additions (e.g. a new `foo_group_hom` definition if it was not there already, plus corresponding `simp` lemma, which is randomly either a `coe` or an `apply` depending on what mood I was in; this could all be done with `@[simps]` trickery apparently but I didn't read the thread carefully yet). Once nice achievement was that I refactored a bunch of basic ring and field theory to avoid the `is_` classes completely, which I think is a step in the right direction (people were occasionally being forced to use deprecated stuff when doing stuff like Galois theory because some fundamental things used to use them; this is no longer the case -- in particular I think Abel-Ruffini might now be deprecated-free, or very nearly so). `finset.sum_hom` and `finset.prod_hom` are gone. It is very funny to do a search for these files in mathlib current master as I write -- 98% of the time they're used, they're used backwards (with `.symm` or `\l` with a rewrite). The bundled versions (`monoid_hom.map_prod` etc) are written the other way around. I could have just left them and not bothered, but it seemed easier just to get rid of them if we're moving to bundled morphisms. One funny observation was that unary `-` seemed to be a special case: we seem to prefer `-\sum i, f i` to `\sum i, -(f i)` . For almost every other function, we want it to go the other way.