Commit 2021-08-01 17:17 f961b280

View on Github →

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 changeing 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 (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 to be private multiset.map_aux and then redefine 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_homs. 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 and just nuking our current 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 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.

Estimated changes

modified theorem additive.is_add_group_hom
modified theorem additive.is_add_hom
modified theorem additive.is_add_monoid_hom
added structure is_add_group_hom
added structure is_add_hom
added structure is_add_monoid_hom
modified theorem is_group_hom.comp
added theorem
modified theorem is_group_hom.injective_iff
modified theorem is_group_hom.inv
modified theorem is_group_hom.map_inv
added theorem is_group_hom.map_mul
modified theorem is_group_hom.map_one
added structure is_group_hom
modified theorem is_monoid_hom.comp
added theorem
added theorem is_monoid_hom.inv
deleted theorem is_monoid_hom.of_mul
added structure is_monoid_hom
modified theorem is_mul_hom.comp
added theorem
modified theorem is_mul_hom.inv
added structure is_mul_hom
modified theorem'
modified theorem monoid_hom.coe_of
modified def monoid_hom.of
added theorem mul_equiv.is_group_hom
added theorem mul_equiv.is_mul_hom
modified theorem multiplicative.is_group_hom
modified theorem multiplicative.is_mul_hom
modified theorem units.coe_map'
modified def'
modified theorem is_ring_hom.comp
added theorem
modified theorem is_ring_hom.map_neg
modified theorem is_ring_hom.map_sub
modified theorem is_ring_hom.map_zero
modified theorem is_ring_hom.of_semiring
added structure is_ring_hom
modified theorem is_semiring_hom.comp
added theorem
added structure is_semiring_hom
modified theorem ring_hom.coe_of
modified def ring_hom.of
modified theorem field.closure_subset
modified theorem field.closure_subset_iff
added theorem image.is_subfield
added theorem is_subfield.Inter
modified theorem is_subfield.div_mem
added theorem is_subfield.inter
modified theorem is_subfield.pow_mem
added structure is_subfield
added theorem preimage.is_subfield
added theorem range.is_subfield
added theorem univ.is_subfield
modified theorem group.closure_subgroup
modified theorem group.closure_subset
modified theorem group.closure_subset_iff
modified theorem group.conjugates_of_subset
modified theorem group.image_closure
modified theorem group.normal_closure_subset
deleted theorem is_add_subgroup.gsmul_coe
added structure is_add_subgroup
modified theorem is_group_hom.inv_iff_ker'
modified theorem is_group_hom.inv_iff_ker
modified theorem is_group_hom.inv_ker_one'
modified theorem is_group_hom.inv_ker_one
modified theorem is_group_hom.one_ker_inv'
modified theorem is_group_hom.one_ker_inv
added theorem is_group_hom.preimage
added structure is_normal_add_subgroup
added structure is_normal_subgroup
added theorem is_subgroup.Inter
deleted theorem is_subgroup.coe_gpow
deleted theorem is_subgroup.coe_inv
modified theorem is_subgroup.div_mem
modified theorem is_subgroup.eq_trivial_iff
added theorem is_subgroup.inter
modified theorem is_subgroup.mem_norm_comm
added structure is_subgroup
added theorem subgroup.is_subgroup
modified def subgroup.of
added theorem subgroup.of_normal
deleted def subtype.comm_group
deleted def
deleted theorem image.is_submonoid
deleted theorem is_add_submonoid.smul_coe
modified theorem is_add_submonoid.smul_mem
added structure is_add_submonoid
added theorem is_submonoid.Inter
deleted theorem is_submonoid.coe_mul
deleted theorem is_submonoid.coe_one
deleted theorem is_submonoid.coe_pow
added theorem is_submonoid.image
added theorem is_submonoid.inter
modified theorem is_submonoid.list_prod_mem
modified theorem is_submonoid.pow_mem
modified theorem is_submonoid.power_subset
added theorem is_submonoid.preimage
added structure is_submonoid
modified theorem monoid.closure_subset
modified theorem monoid.image_closure
added theorem powers.is_submonoid
added theorem range.is_submonoid
added theorem submonoid.is_submonoid
modified def submonoid.of
deleted def subtype.comm_monoid
deleted def subtype.monoid
added theorem univ.is_submonoid
added theorem is_subring.Inter
deleted theorem is_subring.coe_subtype
added theorem is_subring.inter
deleted def is_subring.subtype
added structure is_subring
modified theorem ring.closure_subset
modified theorem ring.closure_subset_iff
deleted def subring.domain
deleted def subset.comm_ring
deleted def subset.ring
deleted def subtype.comm_ring
deleted def subtype.ring