Ring Theory - A Rosetta Stone

• addition is commutative: for all \(x,y\in R\), we have \(x+y=y+x\) (Abelian)
• associativity of addition \((x+y)+z=x+(y+z)\) for all \(x,y,z\in R\) (add-associative)
• additive inverse: for each \(x\in R\), there exists a \(y\in R\) such that \(x+y=0\) (i.e., every element is right_complementable)
• additive identity \(x+0=x\) (right_zeroed) and by commutativity \(0+x=x\) for all \(x\in R\)
• multiplication is associative: for all \(x,y,z\in R\) we have \((xy)z=x(yz)\)
• it is well-unital: for all \(x\in R\), we have \(x\cdot 1=x\) and \(1\cdot x=x\)
• multiplication is distributive over addition: for all \(x,y,z\in R\) we have \(x(y+z)=xy+xz\) and \((x+y)z=xz+yz\)

• Remark. Sadly, Mizar's ring is defined to always be unital. Therefore we will tend to drop the "unital" prefix.

1. The integers form a ring, which Mizar calls INT.Ring
2. The real numbers form a field which Mizar calls F_Real
3. The rational numbers form a field which Mizar calls F_Rat
4. The complex numbers form a field which Mizar calls F_Complex
5. The integers modulo \(n\) forms a commutative ring which Mizar calls INT.Ring n
6. The quaternions form a ring \(\mathbb{H}\) which Mizar calls R_Quaternion
7. If \(A\) is a ring and \(X\) is a nonempty set, then the set \(R\) of all functions \(X\to A\) forms a ring Missing from Mizar

1. For all \(a\in R\) we have \(0a=a0=0\) (vectsp_1:7 and vectsp_1:14)
2. For all \(a,b\in R\) we have
   • (vectsp_1:8) \(a(-b)=-(ab)\)
   • (vectsp_1:9) \((-a)b=-(ab)\)
3. For all \(a,b\in R\) we have \((-a)(-b)=ab\) (vectsp_1:10)
4. For all \(a\in R\) we have \(-a=(-1)a\) (vectsp_1:14)

1. We say \(x\in R\) is a Zero Divisor if there is a \(y\in R\) such that \(y\neq0\) and \(xy=0\). Mizar requires \(R\) to be commutative. (ringfrac)
2. If \(R\) is nondegenerate (i.e., \(1\neq0\)), we say \(x\in R\) is Unital if there exists some \(y\in R\) such that \(xy=1\) and \(yx=1\) (gcd_1:def 2)

• The example \(\mathbb{Q}(\sqrt{D})\) where \(D^{2}\notin\mathbb{Q}\) is a specialized example of adjoining the squareroot of a nonsquare element of a field. In Mizar, this is done by FieldAdjunction(F,{sqrt a}) (see, e.g., Lemma dega in field_9)

• domRing-like: for any \(x,y\in R\), if \(xy=0\) then \(x=0\) or \(y=0\)

• \(\mathbb{Z}\) is a subring of \(\mathbb{Q}\) (ring_3:47)
• \(\mathbb{Q}\) is a subring of \(\mathbb{R}\) (liouvil2:4)
• \(\mathbb{R}\) is a subring of \(\mathbb{C}\) (liouvil2:3)
• The integral quaternions \(S=\mathbb{Z}+i\mathbb{Z}+j\mathbb{Z}+k\mathbb{Z}\) is a subring of the quaternions Missing from Mizar
• If \(R\) is a subring of a field \(F\) that contains the identity, then \(R\) is an integral domain Missing from Mizar

1. additive: \(\varphi(a+b)=\varphi(a)+\varphi(b)\) for all \(a,b\in R\)
2. multiplicative: \(\varphi(ab)=\varphi(a)\varphi(b)\) for all \(a,b\in R\)
3. unity-preserving: \(\varphi(1)=1\)

1. The image of \(\varphi\) is a subring of \(S\) (ring_2:def 6)
2. The kernel of \(\varphi\) is a subring of \(R\).

1. • (ideal_1:def 18) \(rI = \{ra\mid a\in I\}\) and
   • Missing from Mizar \(Ir = \{ar\mid a\in I\}\)
2. A subset \(I\) of \(R\) is a Left Ideal of \(R\) (ideal_1) if
   1. \(I\) is a subring of \(R\) and \(I\) is add-closed: for any \(x,y\in I\), \(x+y\in I\)
   2. left-ideal: \(I\) is closed under left multiplication by elements from \(R\), i.e., \(rI\subset I\) for all \(r\in R\)
3. A subset \(I\) of \(R\) is a Right Ideal of \(R\) (ideal_1) if
   1. \(I\) is add-closed: for any \(x,y\in I\), \(x+y\in I\)
   2. right-ideal: \(Ir\subset I\) for all \(r\in R\)
4. A subset \(I\) of \(R\) is a Two-Sided Ideal (ideal_1) if it is both a left and right ideal of \(R\)

1. First isomorphism theorem (ring_2:15): If \(\varphi\colon R\to S\) is a ring morphism, then \(R/\ker(\varphi)\cong\varphi(R)\)
2. If \(I\) is any ideal of \(R\), then the map \(R\to R/I\) defined by \(r\mapsto r+I\) is a surjective ring morphism with kernel \(I\) which Mizar calls the Canonical Morphism of \(I\) (ring_2:def 5). Thus every ideal is the kernel of a morphism, and vice-versa.

1. The subrings \(R\) and \(\{0\}\) are ideals (ideal_1:10).

   An ideal \(I\) is proper if \(I\neq R\).

   The ideal \(\{0\}\) is called the Trivial Ideal and denoted by \(0\) (ideal_1:def 4).

2. The sets \(n\mathbb{Z}\) are ideals of \(\mathbb{Z}\) for any \(n\in\mathbb{Z}\) (although this is Missing from Mizar, its significance for Dummit and Foote is only to construct \(\mathbb{Z}/n\mathbb{Z}\) which is done explicitly in Mizar)
3. Let \(R=\mathbb{Z}[x]\) be the ring of polynomials in \(x\) with integer coefficients. Let \(I\) be the set of polynomials whose terms are of degree at least 2 (i.e., they all look like \(a_{n}x^{n}+\dots+a_{2}x^{2}\)). Then \(I\) is an ideal of \(R\). Missing from Mizar

1. Second isomorphism theorem for rings: Let \(A\) be a subring of \(R\), let \(I\) be an ideal of \(R\). Then \(A+I\) is a subring of \(R\), \(A\cap I\) is an ideal of \(A\), and \((A+I)/I\cong A/(A\cap I)\)
2. Third isomorphism theorem for rings: Let \(I\) and \(J\) be ideals of \(R\) with \(I\subset J\). Then \(J/I\) is an ideal of \(R/I\) and \((R/I)/(J/I)\cong R/J\).
3. Fourth isomorphism theorem for rings: Let \(I\) be an ideal of \(R\). The correspondence \(A\leftrightarrow A/I\) is an inclusion-preserving bijection between the set of subrings \(A\) of \(R\) which contain \(I\) and the set of subrings of \(R/I\). Furthermore, \(A\) (a subring containing \(I\)) is an ideal of \(R\) if and only if \(A/I\) is an ideal of \(R/I\).

1. The Sum of \(I\) and \(J\) is \(I+J=\{a+b\mid a\in I,b\in J\}\) (ideal_1:def 19)
2. The Product of \(I\) and \(J\) is the set \(IJ\) of all finite sums of terms of the form \(ab\) with \(a\in I\) and \(b\in J\) (ideal_1:def 21)
3. For any \(n\geq1\), define the n-th power of \(I\), denoted by \(I^{n}\), to be the set consisting of all finite sums of elements of the form \(a_{1}a_{2}(\dots)a_{n}\) for \(a_{i}\in I\) for all \(i\). That is to say \(I^{1}=I\) and \(I^{n+1}=II^{n}\) (ideal_2:def 2)

1. The Ideal Generated by \(A\) is the smallest ideal \((A)\) of \(R\) containing \(A\) (ideal_1:def 14); this also generalizes to "left ideals generated by \(A\)" and "right ideals generated by \(A\)"
2. Let \(AR=\{\sum^{n}_{i=1}a_{i}r_{i}\mid n\in\mathbb{N},a_{i}\in A,r_{i}\in R\}\) and \(RA=\{\sum^{n}_{i=1}r_{i}a_{i}\mid n\in\mathbb{N},a_{i}\in A,r_{i}\in R\}\)
3. A Principal Ideal is the ideal generated by a single element (ideal_1:def 27)
4. An ideal generated by a finite set is called a Finitely-Generated Ideal (ideal_1:def 25)

1. \(I=R\) if and only if \(I\) contains a unit (ideal_1:20)
2. Assume \(R\) is commutative. Then \(R\) is a field if and only if its only ideals are \(0\) and \(R\). (ideal_1:22)

1. Every element of \(Q\) is of the form \(rd^{-1}\) for some \(r\in R\) and \(d\in D\).
2. (Uniqueness of \(Q\)) The ring \(Q\) is the "smallest" ring containing \(R\) in which all elements of \(D\) are units, in the sense that for any commutative unital ring \(S\) and for any injective ring morphism \(\varphi\colon R\to S\) such that \(\varphi(d)\) is a unit for all \(d\in D\), then there exists an injective ring morphism \(\Phi\colon Q\to S\) such that \(\Phi|_{R}=\varphi\)

1. The ring \(Q\) is called the Ring of Fractions of \(D\) with respect to \(R\) and is denoted \(Q^{-1}R\) (ringfrac:def 18). Mizar uses the notation Q ~ R instead of \(Q^{-1}R\).
2. If \(R\) is an integral domain and \(D=R\setminus\{0\}\), then \(Q\) is called the Field of Fractions or Quotient Field of \(R\); this is defined for any nondegenerate unital commutative ring, where it's called the Total Quotient Ring (ringfrac:def 24).

Definition. The integral domain \(R\) is said to be a Euclidean Domain if there exists a function \(N\colon R\to\mathbb{N}_{0}\) with \(N(0)=0\) and for any \(a,b\in R\) with \(b\neq0\) there exists elements \(q,r\in R\) such that \(a=qb+r\) and \(r=0\) or \(N(r)\lt N(b)\) (int_3:def 8)

The function \(N\) is called the Degree Function in Mizar (int_3:def 9).

1. We say \(a\) is a multiple of \(b\) if there exists an element \(x\in R\) with \(a=bx\). In this case, we also say \(b\) Divides \(a\) (gcd_1:def 1)
2. A Greatest Common Divisor of \(a\) and \(b\) is a nonzero element \(d\) such that \(d\) divides \(a\), and \(d\) divides \(b\), and for any other \(d'\in R\) if \(d'\) divides both \(a\) and \(b\) then \(d'\) divides \(d\). (This is generalized in gcd_1:def 12 and especially ring_4:def 10)

1. \(d\) is a greatest common divisor of \(a\) and \(b\) (Missing from Mizar), and
2. The principal ideal \((d)\) is the ideal generated by \(a\) and \(b\) (Missing from Mizar but seems to follow from ring_2:18)

1. \(d\) is a greatest common divisor of \(a\) and \(b\) Missing from Mizar
2. \(d\) can be written as an $R$-linear combination of \(a\) and \(b\), i.e., there exists \(x\) and \(y\) in \(R\) with \(d=ax+by\) Missing from Mizar
3. \(d\) is unique up to multiplication by a unit of \(R\) Missing from Mizar

• Suppose \(r\in R\) is nonzero and is not a unit. Then \(r\) is called Irreducible if whenever \(r=ab\) with \(a,b\in R\), then either \(a\) is a unit in \(R\) or \(b\) is a unit in \(R\) or both; otherwise \(r\) is called Reducible (ring_2:def 9)
• The nonzero element \(p\in R\) is called Prime in \(R\) if the ideal \((p)\) generated by \(p\) is a prime ideal. In other words, a nonzero element \(p\) is prime if it is not a unit and whenever \(p\mid ab\) either \(p\mid a\) or \(p\mid b\) (ring_2:def 8)
• Two elements \(a,b\in R\) differing by a unit are said to be Associated if \(a=ub\) for some unit \(u\in R\) (gcd_1:def 3)

1. \(r\) can be written as a finite product of irreducibles \(p_{i}\) of \(R\), i.e., \(r=p_{1}p_{2}\dots p_{n}\); and
2. the decomposition in (1) is unique up to associates

1. \(\deg(p(x)q(x))=\deg(p(x))+\deg(q(x))\) (hurwitz:23)
2. the units of \(R[x]\) is just the units of \(R\) Missing from Mizar
3. \(R[x]\) is an integral domain Missing from Mizar

• Although this is easier for informal mathematics, Mizar formalizes a notion of "bags" to describe monomials as a function from the set of unknowns to the exponent for each unknown. A polynomial is then a formal $R$-linear combination of bags.