Ensure that theorems in Part 18 (Additional material, deprecated) have an extensible structure version

[tirix]

From Norm in this post:

The intent is for theorems in Part 18 to be removed when someone goes through them and verifies that we have an extensible structure version, or adds the extensible structure version if it is missing, or determines the Part 18 theorem isn't useful and should just be deleted.

I'm opening this issue to track this action.

[avekens]

I tried to work on this by adding "the extensible structure version if it is missing", but my approach was rejected by @nmegill and @digama0 mainly, see #1389. I see no other way to get rid of Part 18, except by waiting until there are "real applications" (according to @nmegill and @digama0) for magmas, internal operations, etc. - and this could take long, if at all. And I think it is more disturbing (especially for beginners and non-mathematicians) to have these obscure deprecated material in set.mm (for a long time or forever) than the clean definitions and applications as proposed in #1389.

The only short term solution I see would be to delete this part radically (and all the theorems in the mathboxes referencing it), or to transform it into a mathbox (let's call it "Mathbox for Nicolas Bourbaki" ;-) ) so that it is not contained in the main body of set.mm anymore. The latter proposal goes in the direction @david-a-wheeler proposed in #1389 - we can move the definitions/theorems from my mathbox into this new mathbox later, replacing the current, deprecated definitions and theorems, and anybody who wants to work in this field can do it (it would be no personal mathbox).

[digama0]

From a cursory look at part 18, I see nothing that we are missing. Delete?

I haven't gone though the algebraic lemmas in e.g. 18.2.1 in detail to make sure we have analogues for each one, but I would expect that we have all of them or almost all.

---

A breakdown of the sections:

• 18.1.1: Group, inverse, division, power. We have all of these, with much better coverage, in main. (The notation is additive though, so it's called addition, subtraction, and group multiple.)
• 18.1.2: Abelian groups. Again, totally covered in main.
• 18.1.3: Subgroups. Covered.
• 18.1.4: Associative, unital mixin. Rejected (for now), no theorems.
• 18.1.5: Magma. Rejected (for now). There are a few theorems here:
  • opidon, rngopid, opidon2: the same theorem written three different ways. It doesn't look very useful, but maybe someone wants to adopt it.
  • isexid2: trivial when you replace X with Base
  • exidu1: Covered (in the context of monoids; this theorem would be generalized if the general structure found use).
• 18.1.5: Semigroups. Rejected (for now). No theorems.
• 18.1.5: Monoids. Covered, no theorems.
• 18.1.6: Examples of abelian groups, specifically: the trivial group, addition on Z and R, and multiplication on nonzero complexes. I'm not sure where the trivial group is, but I think it's around somewhere, and the others are available through general abstract nonsense.
• 18.1.7: Group homomorphisms & isomorphisms. Covered.
  • There are some actual theorems in this section though, and we may not have all of them. ghgrp looks important, and efghgrp and circgrp is a curiosity but I don't think we've duplicated it.
• 18.2.1: Rings. Covered. (There are a lot of algebra theorems here but none of them look nontrivial and I'm pretty sure they are all covered.)
• 18.2.2: The trivial ring. This should really be an extensible structure: a singleton set has a bunch of algebraic structure on it.
• 18.2.3: Division rings. Covered, no theorems.
• 18.2.4: Star fields. Covered, no theorems.
• 18.2.5: Commutativity mixin. Rejected (for now), no theorems.
• 18.2.5: Fields. Covered.
  • rngosn3, rngosn4, rngosn6, rngoueqz: should be in a section about the trivial group/ring
  • zerdivemp1, rngoridfz: Covered.

I didn't see a whole lot worth saving. There are only a handful of theorems that aren't definitely covered, so the work to supplant this section seems to be already nearly complete.

[avekens]

* 18.1.5: Magma. Rejected (for now). There are a few theorems here:
  * opidon, rngopid, opidon2: the same theorem written three different ways. It doesn't look very useful, but maybe someone wants to adopt it.

Yes, they are useful. I think I will provide a (one!) corresponding theorem for monoids.

* 18.1.6: Examples of abelian groups, specifically: the trivial group, addition on Z and R, and multiplication on nonzero complexes. I'm not sure where the trivial group is, but I think it's around somewhere, and the others are available through general abstract nonsense.

Theorems about the trivial group are in my mathbox! See ~ mnd1, ~grp1, ~ abl1. I would move these into the main body of set.mm then.

* 18.2.2: The trivial ring. This should really be an extensible structure: a singleton set has a bunch of algebraic structure on it.

Also in my mathbox: ~rng1 Also to be moved.

* 18.2.5: Fields. Covered.
  * rngosn3, rngosn4, rngosn6, rngoueqz: should be in a section about the trivial group/ring

I can have a look at these theorems after I moved ~rng1 to main set.mm

[avekens]

* 18.1.5: Magma. Rejected (for now). There are a few theorems here:
  * opidon, rngopid, opidon2: the same theorem written three different ways. It doesn't look very useful, but maybe someone wants to adopt it.

Yes, they are useful. I think I will provide a (one!) corresponding theorem for monoids.

I just saw that such a theorem is already available - see ~mndfo.

[benjub]

I just saw that such a theorem is already available - see ~mndfo.

Except that ~opidon and friends show that this holds for any unital magma (that's a side remark, and it probably suffices to have ~mndfo).

I hope the extensible structure versions of ghgrp, ghablo will be clearer, because several hypotheses currently appear as hacks. In any case, their comments are inaccurate, because they prove that the image of a group (resp. abelian group) under a magma morphism (or something even more general) is a group (resp.\ abelian group). Similarly with ghsubgo, gsubablo.

As for ~circgrp: I do not know if this is a curiosity in its current form. What I know is that the Lie group S^1 \simeq \R / \Z is very important and could be defined as an extensible structure. However, I would define it in set.mm as \R / \Z rather than as a multiplicative subgroup of \C.

A note which I think is important: in a way or another, there should remain some crediting to FL, who contributed many of these. If, for instance, a newer theorem is pretty close to FL's original version, it could be credited like "Contributed by FL... Revised by ...".

[avekens]

A note which I think is important: in a way or another, there should remain some crediting to FL, who contributed many of these. If, for instance, a newer theorem is pretty close to FL's original version, it could be credited like "Contributed by FL... Revised by ...".

I did it exactly in this way (where appropriate), see PR #1433.

[tirix]

Thanks all! It appears we can now delete section 18, and consistently use extensible structures throughout set.mm. I'll keep this issue open until section 18 is actually deleted. As a note, it will always be possible to recover section 18 for example using git checkout 41d9f987070e87819ff403fa5b97630ef35982ee (which is the current latest version as I write this note)

[benjub]

@tirix: are you sure ? See @digama0's " ghgrp looks important, and efghgrp and circgrp is a curiosity but I don't think we've duplicated it." and my comments to it above, which also mention ghsubgo, gsubablo. Is it dealt with ?

On Fri, Jan 24, 2020 at 11:01 AM tirix notifications@github.com wrote:

Thanks all! It appears we can now delete section 18, and consistently use extensible structures throughout set.mm. I'll keep this issue open until section 18 is actually deleted. As a note, it will always be possible to recover section 18 for example using git checkout 41d9f987070e87819ff403fa5b97630ef35982ee (which is the current latest version as I write this note)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/metamath/set.mm/issues/1432?email_source=notifications&email_token=AJZP56YHTNCIPPMFCOUPOYLQ7K37VA5CNFSM4KKRHHX2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEJ2JIVI#issuecomment-578065493, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJZP56Y2MMITGYF2AO5WRP3Q7K37VANCNFSM4KKRHHXQ .

[avekens]

What about the references in the mathboxes to theorems of part 18? The referencing theorems have also to be deleted. I have 2-3 theorems referencing such theorems in my mathbox - these can be deleted.

[avekens]

With PR #1433 and #1438, I provided extensible structure versions of the following theorems in Part 18 as promised:

* 18.1.5: Magma. Rejected (for now). There are a few theorems here:
  * opidon, rngopid, opidon2: the same theorem written three different ways. It doesn't look very useful, but maybe someone wants to adopt it.

Yes, they are useful. I think I will provide a (one!) corresponding theorem for monoids.

• ~opidon, ~rngopid, ~opidon2 -> ~mndpfo

• 18.1.6: Examples of abelian groups, specifically: the trivial group, addition on Z and R, and multiplication on nonzero complexes. I'm not sure where the trivial group is, but I think it's around somewhere, and the others are available through general abstract nonsense.

  
  Theorems about the trivial group are in my mathbox! See ~ mnd1, ~grp1, ~ abl1. I would move these into the main body of set.mm then.

• ~ablosn -> ~abl1
• ~gidsn -> ~mnd1id
• ~cnaddablo -> ~cnaddabl

• 18.2.2: The trivial ring. This should really be an extensible structure: a singleton set has a bunch of algebraic structure on it.

Also in my mathbox: ~rng1 Also to be moved.

* 18.2.5: Fields. Covered.
  * rngosn3, rngosn4, rngosn6, rngoueqz: should be in a section about the trivial group/ring

I can have a look at these theorems after I moved ~rng1 to main set.mm

• ~rngosn3 -> ~srg1zr, ~rng1zr
• ~rngosn4 ->~rngen1zr
• ~rngosn6 ->~srgen1zr, ~ringen1zr
• ~rngoueqz ->~0rng01eqbi

The corresponding theorems of part 18 are marked as obsolete and could be removed (if there are no references in theorems of the following mathboxes).

[tirix]

@tirix: are you sure ? See @digama0's " ghgrp looks important, and efghgrp and circgrp is a curiosity but I don't think we've duplicated it." and my comments to it above, which also mention ghsubgo, gsubablo. Is it dealt with ?

You're right Benoît, thank you! I've covered ~ghgrp in #1440, as ~ghmgrp. I'll look at ~efgrp and ~circgrp next. I've been interested in the unit circle as a manifold and these might actually be interesting for that! The others remain. I think ~ghsubgo will be covered by ~ghmgrp, since we already have the fact that any subgroup is a group. Remains ~ghsubablo, which I would rename ~ghmabl.

[benjub]

Thanks @tirix. As for ~circgrp, see my comment above (search "Lie group"), i.e. R/Z rather than a subgroup of the multiplicative group of CC.

[digama0]

Regarding the circle vs. R/Z, they are both important. You don't get the geometrical properties of a circle by looking at R/Z, although there is a significant amount of material that needs S^n and CC won't cut it for that. I got pretty far in proving the existence of universal covers in order to prove that the fundamental group of the circle is Z, but I never finished that work. The core of it is the isomorphism between the groups S^1 (the geometric object) and R/Z.

[tirix]

There are some actual theorems in this section though, and we may not have all of them. ghgrp looks important, and efghgrp and circgrp is a curiosity but I don't think we've duplicated it.

With #1442, those are now covered.

For R/Z, as mentioned by Benoit, I also believe this is interesting, but this goes beyond covering the same material as section 18, and could be tracked with another issue if necessary.

Is there anything else missing?

[tirix]

PS. In set.mm, R/Z can be defined as ( RRfld /s ( RRfld ~QG ZZ ) ). I have proven that it is a group in ~rzgrp. Next step would be to prove it's isomorphic with the unit circle!

[benjub]

It is indeed crucial to prove that R/Z with the quotient structure is isomorphic to S^1 as a subgroup of the multiplicative group of CC. First as groups, then as topological groups, and ultimately as Lie groups! A good symbol for R/Z as an extensible structure is blackboard bold T. It is probably already used in one form or another in the recent results in Fourier theory.

[tirix]

@nmegill if nothing is missing anymore, we could start marking those theorems as *OLD, so that they get deleted by the next cleanup? That way I could close this "issue"! As I wrote, once deleted, they will not be lost forever, since Git stores them for us, but it will still take some effort to recover them.

[nmegill]

@nmegill if nothing is missing anymore, we could start marking those theorems as *OLD, so that they get deleted by the next cleanup? That way I could close this "issue"!

Definitely, please do mark them OLD. The comment should have "Obsolete [version of ~ xxx] as of dd-mmm-2020. " with a space following the period. I typically search for "mmm-yyyy. " or just "yyyy. " to find the OLDs a year or more old, and usually that only matches in the *OLDs. BTW the cleanup is a little overdue, if anyone feels like doing it. Otherwise I will eventually.

[avekens]

@tirix Please do not start renaiming the definitions/theorems of part 18 until I have finished #1457. I have to rename some definitions/theorems of part 18 by myself, because there are some name clashes.

[avekens]

@nmegill There are some theorems in JM's mathbox using definitions/theorems of part 18. What shall we do with them?

[avekens]

@tirix what's the status of this issue? I have done everything I can/had to do, so you can start your final actions (see your comment on 2 Feb) and close this issue afterwards.

[tirix]

@avekens sorry I really have not had this on my bucket list! If anyone wants to do this, feel free! Indeed I think all the preparation work is done, so it would be about going through that chapter and marking those theorems as OLD.

[avekens]

With PR #2162, I made the first step to clean up Part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)". Subsection 18.1.7 and section 18.2 are already removed, mainly (almost completely) moved into the mathboxes of PC and JM, because there are a lot of theorems in these mathboxes which depend on the definitions/theorems of the removed sections. The owners of the mathboxes can decide by themselves to remove the definition/theorems (together with their own theorems) or to transform their theorems to be based on the official definitions in the main part of set.mm. For details see the comment in #2162.

The next step would be to "remove" subsections 18.1.5 and 18.1.6 in the same way, looking for material which should be kept in a transformed version.

[nmegill]

I appreciate the cleanup, thanks.

JM has been inactive for about 10 years and I think it is safe to assume probably won't be making any more changes. I'm not sure what to do about the ones using deprecated material; ideally the most important ones would be converted but that could be a lot of work. If similar but non-deprecated material now exists elsewhere, then they can be deleted, possibly with JM acknowledged as the original contributor of the newer version and the current contributor becoming a "Revised by" contributor, depending on similarity and date precedence.

[avekens]

With PR #2166, I made the second step to clean up Part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)". Subsection 18.1.5 and 18.1.6 are removed, resp. moved into mathboxes. Most of it is moved into JM's mathbox. If JM is not active anymore, somebody else should look at his theorems, revise them accordingly and put the revised theorems into the main body of set.mm, as Norm proposed.

The following subsections are concerned (about 140 theorems): 21.19.13 Groups and related structures exidcl 32745 21.19.14 Rings rngonegcl 32755 21.19.15 Ring homomorphisms crnghom 32770 21.19.16 Commutative rings ccring 32799 21.19.17 Ideals cidl 32811 21.19.18 Prime rings and integral domains cprrng 32850 21.19.19 Ideal generators cigen 32863

[avekens]

With PR #2168, I removed subsection "Groups" and "Group homomorphism and isomorphism" from PC's mathbox, which mostly contained material which was moved from Part 18 before. 12 theorems of PC were either lemmata or are covered by theorems in main set.mm. In detail:

• ghomgrpilem1: --- (lemma)
• ghomgrpilem2: --- (lemma)
• ghomgrpi: ghmrn
• ghomsn: idghm
• ghomgrplem: --- (lemma)
• ghomgrp (closed form of ghomgrpi): ghmrn
• ghomfo: --- (follows from ghmf and ffrn)
• ghomcl: --- (follows from ghmf and ffvelrn)
• ghomgsg: ghmghmrn
• ghomf1olem: --- (lemma)
• ghomf1o: --- (follows from ghmf1 and ffrn)
• elgiso: isgim

~ ghmghmrn is a revision of ~ghomgsg by me, where I mentioned PC as contributor. What about ~isgim, ~idghm, ~ghmrn? Shall PC be the contributor of these theorems, revised by SO (the current contributor)? @sorear what's your opinion?

Finally, I moved material of subsection "Group homomorphism and isomorphism" in PC's mathbox to JM's mathbox, which is used there. By this, I could reactivate the previously deactivated theorems in JM's mathbox. All deprecated material which was removed from Part 18, but which cannot be deleted (because it is stillused), is collected in JM's mathbox now, so only this mathbox must be regarded in further clean-ups.

[avekens]

With PR #2171, further two subsections of Part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)" are removed. Subsection "Definition and basic properties of Abelian groups", however, had to be moved to Part "COMPLEX TOPOLOGICAL VECTOR SPACES" (which is also deprecated), because many theorems in this part are using its definition and theorems. It seems that the remaining subsection "Definitions and basic properties for groups " must be moved to Part "COMPLEX TOPOLOGICAL VECTOR SPACES" for the most part, too. But then, Part 18 can be deleted completely, and the remaining clean-up can be done in this part (and JM's mathbox).

[avekens]

With PR #2175, the (former) part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)" is deleted, and many of its definitions and theorems. There are, however, a lot of definitions and theorems still existing, which had to be moved to the (new) Part 18 "COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)" and to JM's mathbox, because these are used there.

Should this issue be closed anyway? I propose to close it, and to open a new one called "Ensure that theorems in Part 18 "COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)" have an extensible structure version".

Here is a complete "cross reference" between the definitions and theorems of the former part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)" and its counterparts in main set.mm: Cleanup_Part_18.pdf

[avekens]

PS: All relevant definitions and theorems of the former part 18 "ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)" should have a counterpart in main set.mm now (see cross-reference in Cleanup_Part_18.pdf), so that the remaining definitions and theorems can be removed immediately as soon as they are not used anymore.

[avekens]

A proposed on 4-Sep-2021, I just opened a new issue #2201 for the revision of the (new) part 18 "COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)". Therefore, this issue can be closed now (by @tirix).

[tirix]

Thank you Alexander for your continuous efforts! I'm closing this issue.