theory Ring_ZF_4 imports Ring_ZF_2 CommutativeSemigroup_ZF
begin
This theory develops the theory of commutative rings. We define the commutative_ring locale, characterize principal ideals, and study the relationship between prime rings, prime ideals, and the absence of zero divisors.
Commutative rings
A commutative ring is a ring in which multiplication satisfies the commutativity law. We establish that principal ideals take a simple form in this setting.
A commutative ring is defined as a ring0 in which multiplication is commutative.
locale commutative_ring = ring0 +
assumes commutative: \( M\text{ is commutative on }R \)
For any element \(x\) of a commutative ring, the set \(\{x \cdot y \mid y \in R\}\) is an ideal of the ring.
lemma (in commutative_ring) mult_by_elem:
assumes \( x\in R \)
shows \( \{x\cdot y.\ y\in R\}\triangleleft R \)proof have \( x\cdot 1 \in \{x\cdot y.\ y\in R\} \) using Ring_ZF_1_L2(2)
then have I: \( \{x\cdot y.\ y\in R\}\neq 0 \)
{
fix \( t \)
assume t: \( t\in \{x \cdot y .\ y \in R\} \)
then obtain \( y \) where y: \( y\in R \), \( t=x\cdot y \)
then have \( t\in R \) using Ring_ZF_1_L4(3), assms
then have II: \( \{x \cdot y .\ y \in R\} \subseteq R \)
{
fix \( t \) \( h \)
assume ty: \( t\in \{x \cdot y .\ y \in R\} \), \( h\in R \)
from ty(1) obtain \( y \) where y: \( y:R \), \( t=x\cdot y \)
from y(2) have \( t\cdot h=(x\cdot y)\cdot h \)
then have \( t\cdot h= x\cdot (y\cdot h) \) using Ring_ZF_1_L11(2), assms, y(1), ty(2)
moreover
have \( y\cdot h\in R \) using y(1), ty(2) using Ring_ZF_1_L4(3)
ultimately have E1: \( t\cdot h\in \{x \cdot y .\ y \in R\} \)
then have III: \( \forall t\in \{x \cdot y .\ y \in R\}.\ \forall h\in R.\ t \cdot h \in \{x \cdot y .\ y \in R\} \)
{
fix \( t \) \( h \)
assume ty: \( t\in \{x \cdot y .\ y \in R\} \), \( h\in R \)
from ty(1) obtain \( y \) where y: \( y:R \), \( t=x\cdot y \)
from y(2) have \( h\cdot t = h\cdot (x\cdot y) \)
then have \( h\cdot t = h\cdot (y\cdot x) \) using commutative, assms, y(1) unfolding IsCommutative_def
then have \( h\cdot t = (h\cdot y)\cdot x \) using Ring_ZF_1_L11(2), assms, y(1), ty(2)
moreover
have \( h\cdot y\in R \) using y(1), ty(2) using Ring_ZF_1_L4(3)
ultimately have \( h\cdot t = x\cdot (h\cdot y) \), \( h\cdot y\in R \) using commutative, assms unfolding IsCommutative_def
then have \( h\cdot t\in \{x \cdot y .\ y \in R\} \)
then have IV: \( \forall t\in \{x \cdot y .\ y \in R\}.\ \forall h\in R.\ h \cdot t \in \{x \cdot y .\ y \in R\} \)
{
fix \( t \) \( h \)
assume th: \( t:\{x \cdot y .\ y \in R\} \), \( h:\{x \cdot y .\ y \in R\} \)
then obtain \( yt \) \( yh \) where y: \( t=x\cdot yt \), \( yt:R \), \( h=x\cdot yh \), \( yh:R \)
then have \( t + h = (x\cdot yt) + (x\cdot yh) \)
then have \( t + h = x\cdot (yt + yh) \) using ring_oper_distr(1), assms, y(2,4)
moreover
have \( yt + yh :R \) using y(2,4), Ring_ZF_1_L4(1)
ultimately have \( t + h:\{x \cdot y .\ y \in R\} \)
then have V: \( \forall xa\in \{x \cdot y .\ y \in R\}.\ \forall y\in \{x \cdot y .\ y \in R\}.\ xa + y \in \{x \cdot y .\ y \in R\} \)
from I, II, III, IV, V show \( thesis \) using ideal_intro
qed
In a commutative ring the principal ideal generated by an element \(x\) equals \(\{x \cdot y \mid y \in R\}\).
theorem (in commutative_ring) principal_ideal:
assumes \( x\in R \)
shows \( \langle \{x\}\rangle _I = \{x \cdot y .\ y \in R\} \)proof have \( x\cdot 1 \in \{x\cdot y.\ y\in R\} \) using Ring_ZF_1_L2(2)
then have xx: \( x\in \{x\cdot y.\ y\in R\} \) using Ring_ZF_1_L3(5), assms
then show \( \langle \{x\}\rangle _I \subseteq \{x \cdot y .\ y \in R\} \) using generated_ideal_small, mult_by_elem, assms
{
fix \( J \)
assume j: \( \{x\} \subseteq J \), \( J\triangleleft R \), \( J\in Pow(R) \)
{
fix \( t \)
assume t: \( t\in \{x \cdot y .\ y \in R\} \)
then obtain \( y \) where y: \( y:R \), \( t=x\cdot y \)
with j have \( t\in J \) using ideal_dest_mult(1)
then have \( \{x \cdot y .\ y \in R\} \subseteq J \)
moreover
qed
have \( \{x \cdot y .\ y \in R\}\in \{J\in Pow(R).\ J \triangleleft R \wedge \{x\}\subseteq J\} \) using assms, Ring_ZF_1_L4(3), xx, mult_by_elem
then have \( \{J\in Pow(R).\ J \triangleleft R \wedge \{x\}\subseteq J\}\neq 0 \)
ultimately have \( \{x \cdot y .\ y \in R\} \subseteq \bigcap \{J\in Pow(R).\ J \triangleleft R \wedge \{x\}\subseteq J\} \)
then show \( \{x \cdot y .\ y \in R\} \subseteq \langle \{x\}\rangle _I \) using generatedIdeal_def, assms
Prime ideals
We characterize prime rings in terms of zero divisors and show that the quotient of a ring by a prime ideal is a prime ring, or equivalently, has no zero divisors in the commutative case.
Commutative prime rings are the same as commutative rings with no zero divisors.
lemma (in commutative_ring) prime_ring_zero_divs_1:
assumes \( [R,A,M]\text{ is a prime ring } \)
shows \( \text{HasNoZeroDivs}(R,A,M) \)proof{
}
fix \( aa \) \( b \)
assume as: \( aa\in R \), \( b\in R \), \( M \langle aa, b\rangle =\text{ TheNeutralElement}(R,A) \), \( b\neq \text{ TheNeutralElement}(R,A) \)
with assms have \( (\forall z\in R.\ M \langle M \langle aa, z\rangle , b\rangle = 0 ) \longrightarrow \)
\( (aa = 0 \vee b = 0 ) \) using primeRing_def, ringAssum
moreover {
}
ultimately have \( aa = 0 \vee b = 0 \)
fix \( z \)
assume z: \( z\in R \)
have \( (aa\cdot z)\cdot b = (z\cdot aa)\cdot b \) using as(1), z(1), commutative unfolding IsCommutative_def
then have \( (aa\cdot z)\cdot b = z\cdot (aa\cdot b) \) using Ring_ZF_1_L11(2), as, z
then have \( (aa\cdot z)\cdot b = z\cdot 0 \) using as(3)
then have \( (aa\cdot z)\cdot b = 0 \) using Ring_ZF_1_L6(2), z
with as(4) have \( aa=\text{ TheNeutralElement}(R,A) \)
then show \( thesis \) unfolding HasNoZeroDivs_def
qed
A commutative ring with no zero divisors is a prime ring.
lemma (in commutative_ring) prime_ring_zero_divs_2:
assumes \( \text{HasNoZeroDivs}(R,A,M) \)
shows \( [R,A,M]\text{ is a prime ring } \)proof{
}
fix \( aa \) \( b \)
assume as: \( aa\in R \), \( b\in R \), \( \forall z\in R.\ M \langle M \langle aa, z\rangle , b\rangle = \text{ TheNeutralElement}(R, A) \), \( b\neq \text{ TheNeutralElement}(R,A) \)
with assms have \( \forall c\in R.\ \forall b\in R.\ M \langle c, b\rangle = 0 \longrightarrow \)
\( c = 0 \vee b = 0 \) unfolding HasNoZeroDivs_def
with as(1,2) have \( M \langle aa, b\rangle = 0 \longrightarrow aa = 0 \vee b = 0 \)
with as(4) have \( M \langle aa, b\rangle = 0 \longrightarrow aa = 0 \)
moreover
from as(3) have \( M\langle M \langle aa, 1 \rangle , b\rangle = 0 \) using Ring_ZF_1_L2(2)
then have \( aa\cdot b = 0 \) using Ring_ZF_1_L3(5), as(1)
ultimately have \( aa = \text{ TheNeutralElement}(R, A) \)
then show \( thesis \) using primeRing_def, ringAssum
qed
The quotient ring of a ring by a prime ideal is a prime ring.
theorem (in ring0) prime_ideal_no_zero_divs:
assumes \( I\triangleleft _pR \)
shows \( [ \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I), \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)]\text{ is a prime ring } \)proof have ideal: \( I\triangleleft R \) using assms unfolding primeIdeal_def
from primeRing_def, quotientBy_is_ring, assms have \( \)
\( (\forall x\in \text{QuotientBy}(I).\ \)
\( \forall y\in \text{QuotientBy}(I).\ \)
\( (\forall z\in \text{QuotientBy}(I).\ \)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \)
\( \langle \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \langle x, z\rangle , y\rangle =\)
\( \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I))) \longrightarrow \)
\( x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \vee \)
\( y = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I))) \longrightarrow \)
\([QuotientBy\)
\( (I),QuotientGroupOp\)
\( (R, A, I), \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)]\text{ is a prime ring } \) unfolding primeIdeal_def
moreover
qed
have \( \forall x\in \text{QuotientBy}(I).\ \)
\( \forall y\in \text{QuotientBy}(I).\ \)
\( (\forall z\in \text{QuotientBy}(I).\ \)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \)
\( \langle \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \langle x, z\rangle , y\rangle =\)
\( \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I))) \longrightarrow \)
\( x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \vee \)
\( y = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \)proof
ultimately show \( thesis \)
{
}
}
}
}
}
fix \( x \) \( y \)
assume as: \( x\in \text{QuotientBy}(I) \), \( y\in \text{QuotientBy}(I) \), \( \forall z\in \text{QuotientBy}(I).\ \)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \)
\( \langle \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \langle x, z\rangle , y\rangle =\)
\( \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \), \( y \neq \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \)
{
fix \( xx \)
assume xx: \( xx\in R \), \( \text{QuotientGroupRel}(R, A, I)\{xx\} = x \)
{
fix \( yy \)
assume yy: \( yy\in R \), \( \text{QuotientGroupRel}(R, A, I)\{yy\} = y \)
{
fix \( zz \)
assume zz: \( zz\in R \)
from ideal have equiv: \( \text{equiv}(R, \text{QuotientGroupRel}(R, A, I)) \) and cong2: \( \text{Congruent2}( \text{QuotientGroupRel}(R, A, I), M) \) using ideal_equiv_rel, quotientBy_mul_monoid(1)
have \( \bigwedge x y r f.\ \text{equiv}(R,r) \Longrightarrow \text{Congruent2}(r,f) \Longrightarrow x\in R \Longrightarrow y\in R \Longrightarrow \text{ProjFun2}(R, r, f) \)
\( \langle r \{x\}, r \{y\}\rangle =\)
\( r \{f \langle x, y\rangle \} \) using EquivClass_1_L10
then have \( \bigwedge x y.\ \text{equiv}(R, \text{QuotientGroupRel}(R, A, I)) \Longrightarrow \text{Congruent2}( \text{QuotientGroupRel}(R, A, I),M) \Longrightarrow x\in R \Longrightarrow y\in R\)
\( \Longrightarrow \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \)
\( \langle \text{QuotientGroupRel}(R, A, I) \{x\}, \text{QuotientGroupRel}(R, A, I) \{y\}\rangle =\)
\( \text{QuotientGroupRel}(R, A, I) \{M \langle x, y\rangle \} \)
with equiv, cong2 have eq: \( \bigwedge x y.\ x\in R \Longrightarrow y\in R \Longrightarrow \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M) \)
\( \langle \text{QuotientGroupRel}(R, A, I) \{x\}, \text{QuotientGroupRel}(R, A, I) \{y\}\rangle =\)
\( \text{QuotientGroupRel}(R, A, I) \{M \langle x, y\rangle \} \)
have \( \text{QuotientGroupRel}(R, A, I)\{xx\cdot zz\cdot yy\} =\)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)\langle \text{QuotientGroupRel}(R, A, I)\{xx\cdot zz\}, \text{QuotientGroupRel}(R, A, I)\{yy\}\rangle \) using eq, xx(1), yy(1), zz, Ring_ZF_1_L4(3)
then have \( \text{QuotientGroupRel}(R, A, I)\{xx\cdot zz\cdot yy\} = \)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)\langle \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)\langle \text{QuotientGroupRel}(R, A, I)\{xx\}, \text{QuotientGroupRel}(R, A, I)\{zz\}\rangle , \text{QuotientGroupRel}(R, A, I)\{yy\}\rangle \) using eq, xx(1), zz
with xx(2), yy(2) have \( \text{QuotientGroupRel}(R, A, I)\{xx\cdot zz\cdot yy\} = \)
\( \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)\langle \text{ProjFun2}(R, \text{QuotientGroupRel}(R, A, I), M)\langle x, \text{QuotientGroupRel}(R, A, I)\{zz\}\rangle ,y\rangle \)
moreover
have \( \text{QuotientGroupRel}(R, A, I)\{zz\}\in \text{QuotientBy}(I) \) using QuotientBy_def, ideal, zz unfolding quotient_def
moreover note as(3)
ultimately have \( \text{QuotientGroupRel}(R, A, I)\{xx\cdot zz\cdot yy\} = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \)
then have \( xx\cdot zz\cdot yy\in I \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, xx(1), yy(1), zz, Ring_ZF_1_L4(3), QuotientBy_def, ideal
then have \( \forall zz\in R.\ xx\cdot zz\cdot yy\in I \)
then have D: \( xx:I\vee yy:I \) using assms, equivalent_prime_ideal, xx(1), yy(1)
{
assume \( yy\in I \)
then have \( False \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, yy, as(4), QuotientBy_def, ideal
with D have \( xx\in I \)
moreover
have \( \bigwedge P.\ y \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge x.\ y = \text{QuotientGroupRel}(R, A, I) \{x\} \Longrightarrow x \in R \Longrightarrow P) \Longrightarrow P \) by (rule quotientE )
then have \( y \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge x.\ y = \text{QuotientGroupRel}(R, A, I) \{x\} \Longrightarrow x \in R \Longrightarrow xx\in I) \Longrightarrow xx\in I \) by (rule quotientE )
ultimately have \( xx\in I \) using as(2), QuotientBy_def, ideal
then have \( \text{QuotientGroupRel}(R, A, I)\{xx\} = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, QuotientBy_def, ideal, xx(1)
with xx(2) have \( x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \)
moreover
have \( \bigwedge P.\ x \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ x = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow P) \Longrightarrow P \) by (rule quotientE )
then have \( x \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ x = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)))\)
\( \Longrightarrow x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \) by (rule quotientE )
ultimately have \( x = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \) using as(1), QuotientBy_def, ideal
then show \( thesis \)
qed
In a commutative ring, the quotient by a prime ideal has no zero divisors. This is a specialization of prime_ideal_no_zero_divs using commutativity to convert the prime ring condition directly into the no-zero-divisors property.
theorem (in commutative_ring) comm_prime_ideal_no_zero_divs:
assumes \( I\triangleleft _pR \)
shows \( \text{HasNoZeroDivs}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I), \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)) \)proof have ideal: \( I\triangleleft R \) using assms unfolding primeIdeal_def
{
fix \( xx \) \( yy \)
assume as: \( xx\in \text{QuotientBy}(I) \), \( yy\in \text{QuotientBy}(I) \), \( \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle xx,yy\rangle =\)
\( \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \), \( yy \neq \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \)
{
fix \( xx0 \)
assume xx0: \( xx0\in R \), \( \text{QuotientGroupRel}(R,A,I)\{xx0\} = xx \)
{
fix \( yy0 \)
assume yy0: \( yy0\in R \), \( \text{QuotientGroupRel}(R,A,I)\{yy0\} = yy \)
have \( \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle xx,yy\rangle =\)
\( \text{QuotientGroupRel}(R,A,I)\{xx0\cdot yy0\} \) using EquivClass_1_L10, ideal_equiv_rel, quotientBy_mul_monoid(1), ideal, xx0, yy0
with as(3) have prod_in_I: \( xx0\cdot yy0\in I \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, xx0(1), yy0(1), Ring_ZF_1_L4(3), QuotientBy_def, ideal
{
fix \( zz \)
assume zz: \( zz\in R \)
have \( xx0\cdot zz\cdot yy0 = (xx0\cdot zz)\cdot yy0 \)
moreover
have \( (xx0\cdot zz)\cdot yy0 = yy0\cdot (xx0\cdot zz) \) using commutative, xx0(1), yy0(1), zz, Ring_ZF_1_L4(3) unfolding IsCommutative_def
moreover have \( yy0\cdot (xx0\cdot zz) = (yy0\cdot xx0)\cdot zz \) using Ring_ZF_1_L11(2), yy0(1), xx0(1), zz
moreover have \( (yy0\cdot xx0)\cdot zz = (xx0\cdot yy0)\cdot zz \) using commutative, xx0(1), yy0(1) unfolding IsCommutative_def
ultimately have \( xx0\cdot zz\cdot yy0 = (xx0\cdot yy0)\cdot zz \)
then have \( xx0\cdot zz\cdot yy0\in I \) using ideal_dest_mult(1), ideal, prod_in_I, zz
then have \( \forall zz\in R.\ xx0\cdot zz\cdot yy0\in I \)
then have D: \( xx0\in I \vee yy0\in I \) using assms, equivalent_prime_ideal, xx0(1), yy0(1)
{
assume \( yy0\in I \)
then have \( False \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, yy0, as(4), QuotientBy_def, ideal
with D have \( xx0\in I \)
moreover
have \( \bigwedge P.\ yy \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ yy = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow P) \Longrightarrow P \) by (rule quotientE )
then have \( yy \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ yy = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow xx0\in I)\)
\( \Longrightarrow xx0\in I \) by (rule quotientE )
ultimately have \( xx0\in I \) using as(2), QuotientBy_def, ideal
then have \( \text{QuotientGroupRel}(R,A,I)\{xx0\} =\)
\( \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, QuotientBy_def, ideal, xx0(1)
with xx0(2) have \( xx = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \)
moreover
have \( \bigwedge P.\ xx \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ xx = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow P) \Longrightarrow P \) by (rule quotientE )
then have \( xx \in R // \text{QuotientGroupRel}(R, A, I) \Longrightarrow \)
\( (\bigwedge t.\ xx = \text{QuotientGroupRel}(R, A, I) \{t\} \Longrightarrow t \in R \Longrightarrow xx = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)))\)
\( \Longrightarrow xx = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \) by (rule quotientE )
ultimately have \( xx = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \) using as(1), QuotientBy_def, ideal
then show \( thesis \) unfolding HasNoZeroDivs_def
qed
end
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \), \( 2 \in R \)
lemma (in ring0) Ring_ZF_1_L4:
assumes \( a\in R \), \( b\in R \)
shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \) lemma (in ring0) Ring_ZF_1_L11:
assumes \( a\in R \), \( b\in R \), \( c\in R \)
shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)Definition of IsCommutative:
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma (in ring0) ring_oper_distr:
assumes \( a\in R \), \( b\in R \), \( c\in R \)
shows \( a\cdot (b + c) = a\cdot b + a\cdot c \), \( (b + c)\cdot a = b\cdot a + c\cdot a \) lemma (in ring0) Ring_ZF_1_L4:
assumes \( a\in R \), \( b\in R \)
shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \) theorem (in ring0) ideal_intro:
assumes \( \forall x\in I.\ \forall y\in I.\ x + y\in I \), \( \forall x\in I.\ \forall y\in R.\ x\cdot y \in I \), \( \forall x\in I.\ \forall y\in R.\ y\cdot x \in I \), \( I \subseteq R \), \( I\neq 0 \)
shows \( I\triangleleft R \) lemma (in ring0) Ring_ZF_1_L3:
assumes \( a\in R \)
shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \) corollary (in ring0) generated_ideal_small:
assumes \( X\subseteq I \), \( I \triangleleft R \)
shows \( \langle X\rangle _I \subseteq I \) lemma (in commutative_ring) mult_by_elem:
assumes \( x\in R \)
shows \( \{x\cdot y.\ y\in R\}\triangleleft R \) lemma (in ring0) ideal_dest_mult:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in R \)
shows \( x\cdot y \in I \), \( y\cdot x \in I \)Definition of generatedIdeal:
\( X\subseteq R \Longrightarrow \langle X\rangle _I \equiv \bigcap \{I\in \mathcal{I} .\ X \subseteq I\} \)
Definition of primeRing:
\( \text{IsAring}(R,A,M) \Longrightarrow [R,A,M]\text{ is a prime ring } \equiv \)
\( (\forall x\in R.\ \forall y\in R.\ (\forall z\in R.\ M\langle M\langle x,z\rangle ,y\rangle = \text{ TheNeutralElement}(R,A)) \longrightarrow \)
\( x=\text{ TheNeutralElement}(R,A) \vee y=\text{ TheNeutralElement}(R,A)) \)
lemma (in ring0) Ring_ZF_1_L6:
assumes \( x\in R \)
shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \)Definition of HasNoZeroDivs:
\( \text{HasNoZeroDivs}(R,A,M) \equiv (\forall a\in R.\ \forall b\in R.\ \)
\( M\langle a,b\rangle = \text{ TheNeutralElement}(R,A) \longrightarrow \)
\( a = \text{ TheNeutralElement}(R,A) \vee b = \text{ TheNeutralElement}(R,A)) \)
Definition of primeIdeal:
\( P\triangleleft _pR \equiv P\triangleleft R \wedge P\neq R \wedge (\forall I\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ I\cdot _IJ \subseteq P \longrightarrow (I\subseteq P \vee J\subseteq P)) \)
corollary (in ring0) ideal_equiv_rel:
assumes \( I\triangleleft R \)
shows \( \text{equiv}(R, \text{QuotientGroupRel}(R,A,I)) \) lemma (in ring0) quotientBy_mul_monoid:
assumes \( I\triangleleft R \)
shows \( \text{Congruent2}( \text{QuotientGroupRel}(R, A, I),M) \) and \( \text{IsAmonoid}( \text{QuotientBy}(I), \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)) \) lemma EquivClass_1_L10:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( x\in A \), \( y\in A \)
shows \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \} \)Definition of QuotientBy:
\( I\triangleleft R \Longrightarrow \text{QuotientBy}(I) \equiv R// \text{QuotientGroupRel}(R,A,I) \)
lemma (in group0) Group_ZF_2_4_L5E:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( a\in G \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e \)
shows \( r\{a\} = e \longleftrightarrow a\in H \) lemma (in ring0) ideal_normal_add_subgroup:
assumes \( I\triangleleft R \)
shows \( \text{IsAnormalSubgroup}(R,A,I) \) theorem (in ring0) equivalent_prime_ideal:
assumes \( P\triangleleft _pR \)
shows \( \forall x\in R.\ \forall y\in R.\ (\forall z\in R.\ x\cdot z\cdot y\in P) \longrightarrow x\in P \vee y\in P \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
