Prime Ideals

[Thierry Arnoux]

Hi all,

This is just a notice that I've been rewriting some of Jeff Madsen's
theorems about prime ideals using "extensible structures".

I'll see if I can continue with the definition of maximal ideals and the
corresponding theorems.

This work is candidate to being moved to the main part of set.mm, so it
might be of interest to Jeff, some 14 years after his initial
contribution...

BR,
_
Thierry

[Alexander van der Vekens]

I started to transform the definition and theorems for prime rings currently contained in Jeff Madsen's mathbox. 

Like Thierry, I will put the transformed material into my mathbox first. Since prime rings are based on prime ideals, however, Thierry's material has to be moved to main before. I can do that in a preceding PR (or would you like to do it by yourself, Thierry?).

In general: What do we do with the theorems in Jeff's Mathbox? We should, at least, mark them as deprecated - " (Proof modification is discouraged.) (New usage is discouraged.)", and provide a reference to the transformed theorems.

Sooner or later, these old theorems should be removed completely.

Is Jeff Madson still active? If he is, we should hear and obey his opinion, of course.

I remember that I already moved some deprecated theorems (mainly contributed by FL) to Jeff's mathbox some years ago, because his mathbox was the only place where these theorems are still used. These concerns the following subsections in Jeff's mathbox:

            21.24.13  Operation properties   cass 38294
            21.24.14  Groups and related structures   cmagm 38300
            21.24.15  Group homomorphism and isomorphism   cghomOLD 38335
            21.24.16  Rings   crngo 38346
            21.24.17  Division Rings   cdrng 38400
            21.24.18  Ring homomorphisms   crngohom 38412
            21.24.19  Commutative rings   ccm2 38441
            21.24.20  Ideals   cidl 38459
            21.24.21  Prime rings and integral domains   cprrng 38498
            21.24.22  Ideal generators   cigen 38511

I think these subsections can be removed, after their theorems are translated.

[Thierry Arnoux]

Hi Alexander,

Yes, we routinely move to main theorems from other people's mathbox when we need them in ours. From my point of view, you can do it together with the addition of the new theorems in your mathbox, or, if it is a lot like possibly in this case, in a preceding PR. Feel free to do it yourself.

It seems unlikely that Jeff (of Frédéric) would like to resume working on those theorems, and I think we would strongly advise to use the new structures if they wish to, so I think it's safe to first mark them as deprecated.

From the chapter list, it looks like prime rings would be the last definition not yet converted to structures: I think we already cover all the rest (and Miss youch more, of course).

BR,
_
Thierry