Sketch for the development of quotient rings

[Taneb]

I've been thinking for a while about how to "correctly" implement modular arithmetic, such that it is:

• Easy to prove properties about
• Easily extensible to other rings (e.g. polynomials over the rationals)

Here's my plan as it stands, I'd like to gather design thoughts before I render it into existence

• Algebra.Ideal: left, right, two-sided, and symmetric ideals, defined as (left-, right-, bi-) modules with a monomorphism to Algebra.Module.Construct.TensorUnit.whatever. Possibly also prime and maximal ideals.
• Algebra.Ideal.Construct.Principal: for every element of a ring we can find the smallest ideal containing that element
• Algebra.Ideal.Construct.Sum: given two ideals, we can form another ideal consisting of all the elements {a + b | a in A, b in B}
• Algebra.Ideal.Construct.Intersection: given two ideals, we can form another ideal consisting of the elements that are in both ideals
• Algebra.Construct.Quotient.Ring: we can construct a new ring by quotienting a ring by an ideal. This could be extended to groups and normal subgroups too but I don't know how to make that fit quite yet
• Algebra.Ideal.Relation.Binary.Coprime: two ideals are coprime if their sum is isomorphic to the ambient ring
• Algebra.ChineseRemainderTheorem: if two ideals are coprime, then the product of their quotients is isomorphic to the quotient of their intersection
• Algbera.RIng.Bézout: a Bézout ring is one where the sum of two principal ideals is itself principal (up to isomorphism). The integers are an example of this.

Once we have this, we can make other modules specialized to the integers, and that's a high road to modular arithmetic.

Other things to prove:

• when are quotient rings fields or integral domains? For this we need to better define fields and integral domains (see e.g. Discrete fields #1826)
• Most quotient rings over the integers are finite (we should have a definition of finite algebraic structures Add a notion of finite algebraic structures #1881 but we can show they're isomorphic as sets to Fin n)

[jamesmckinna]

Modulo module names/hierarchy decisions, go for it! But actually some more critical discussion might be in order...

...for example how to 'do without' the necessary existence of Prime and Maximal ideals (though the relativisation might be too horribly painful). Choice functions are just about acceptable for the Diaconescu/Hedberg-like results on booleanness/decidability, but opening a new sub hierarchy of Axiom is not somewhere I would want to go just now...

[jamesmckinna]

What's the relationship between the design sketched here, and your work on #2729 ?
Can that PR be viewed as closing this issue at some point downstream?

[Taneb]

#2729 started as an attempt to implement this. Some things changed during the implementation. That PR can absolutely be seen as closing this.