begin
This section defines the concept of a ring ideal, and defines some basic concepts and types, finishing with the theorem that shows that the quotient of the additive group by the ideal is actually a full ring.
Ideals
In ring theory ideals are special subsets of a ring that play a similar role as normal subgroups in the group theory.
An ideal is a subgroup of the additive group of the ring, which is closed by left and right multiplication by any ring element.
definition (in ring0)
\( I \triangleleft R \equiv (\forall x\in I.\ \forall y\in R.\ y\cdot x\in I \wedge x\cdot y\in I) \wedge \text{IsAsubgroup}(I,A) \)
To write less during proofs, we will write \( \mathcal{I} \) to denote the set of ideals of the ring \(R\).
abbreviation (in ring0)
\( \mathcal{I} \equiv \{J\in Pow(R).\ J\triangleleft R\} \)
The first examples of ideals are the whole ring and the zero ring:
lemma (in ring0) ring_self_ideal:
shows \( R \triangleleft R \) using group_self_subgroup, Ring_ZF_1_L4(3) unfolding Ideal_defThe singleton containing zero is and ideal.
lemma (in ring0) zero_ideal:
shows \( \{ 0 \} \triangleleft R \) unfolding Ideal_def using Ring_ZF_1_L6, unit_singl_subgrAn ideal is s subset of the the ring.
lemma (in ring0) ideal_dest_subset:
assumes \( I \triangleleft R \)
shows \( I \subseteq R \) using assms, group0_3_L2 unfolding Ideal_defIdeals are closed with respect to the ring addition.
lemma (in ring0) ideal_dest_sum:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in I \)
shows \( x + y \in I \) using assms, group0_3_L6 unfolding Ideal_defIdeals are closed with respect to the ring multiplication.
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 \) using assms unfolding Ideal_defIdeals are closed with respect to taking the opposite in the ring.
lemma (in ring0) ideal_dest_minus:
assumes \( I \triangleleft R \), \( x\in I \)
shows \( ( - x) \in I \) using assms, group0_3_T3A unfolding Ideal_defEvery ideals contains zero.
lemma (in ring0) ideal_dest_zero:
assumes \( I \triangleleft R \)
shows \( 0 \in I \) using assms, group0_3_L5 unfolding Ideal_defThe simplest way to obtain an ideal from others is the intersection, since the intersection of arbitrary collection of ideals is an ideal.
theorem (in ring0) intersection_ideals:
assumes \( \forall J\in \mathcal{J} .\ (J \triangleleft R) \), \( \mathcal{J} \neq 0 \)
shows \( (\bigcap \mathcal{J} ) \triangleleft R \) using assms, ideal_dest_mult, subgroup_inter unfolding Ideal_defIn particular, intersection of two ideals is an ideal.
corollary (in ring0) inter_two_ideals:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( (I\cap J) \triangleleft R \)proof let \( \mathcal{J} = \{I,J\} \)
from assms have \( \forall J\in \mathcal{J} .\ (J \triangleleft R) \) and \( \mathcal{J} \neq 0 \)
then have \( (\bigcap \mathcal{J} ) \triangleleft R \) using intersection_ideals
thus \( thesis \)
qed
From any set, we may construct the minimal ideal containing that set
definition (in ring0)
\( X\subseteq R \Longrightarrow \langle X\rangle _I \equiv \bigcap \{I\in \mathcal{I} .\ X \subseteq I\} \)
The ideal generated by a set is an ideal
corollary (in ring0) generated_ideal_is_ideal:
assumes \( X\subseteq R \)
shows \( \langle X\rangle _I \triangleleft R \)proof let \( \mathcal{J} = \{I\in \mathcal{I} .\ X \subseteq I\} \)
have \( \forall J \in \mathcal{J} .\ (J \triangleleft R) \)
with assms have \( (\bigcap \mathcal{J} ) \triangleleft R \) using ring_self_ideal, intersection_ideals
with assms show \( thesis \) using generatedIdeal_def
qed
The ideal generated by a set is contained in any ideal containing the set.
corollary (in ring0) generated_ideal_small:
assumes \( X\subseteq I \), \( I \triangleleft R \)
shows \( \langle X\rangle _I \subseteq I \)proof from assms have \( I\in \{J\in Pow(R).\ J \triangleleft R \wedge X\subseteq J\} \) using ideal_dest_subset
then have \( \bigcap \{J\in Pow(R).\ J \triangleleft R \wedge X\subseteq J\} \subseteq I \)
moreover
qed
from assms have \( X\subseteq R \) using ideal_dest_subset
ultimately show \( \langle X\rangle _I \subseteq I \) using generatedIdeal_def
The ideal generated by a set contains the set.
corollary (in ring0) generated_ideal_contains_set:
assumes \( X\subseteq R \)
shows \( X\subseteq \langle X\rangle _I \) using assms, ring_self_ideal, generatedIdeal_defTo be able to show properties of an ideal generated by a set, we have the following induction result
lemma (in ring0) induction_generated_ideal:
assumes \( X\neq 0 \), \( X\subseteq R \), \( \forall y\in R.\ \forall z\in R.\ \forall q\in \langle X\rangle _I.\ P(q) \longrightarrow P(y\cdot q\cdot z) \), \( \forall y\in R.\ \forall z\in R.\ P(y) \wedge P(z) \longrightarrow P(y + z) \), \( \forall x\in X.\ P(x) \)
shows \( \forall y\in \langle X\rangle _I.\ P(y) \)proof let \( J = \{m\in \langle X\rangle _I.\ P(m)\} \)
from assms(2,5) have \( X\subseteq J \) using generated_ideal_contains_set
from assms(2) have \( J\subseteq R \) using generated_ideal_is_ideal, ideal_dest_subset
moreover {
}
qed
fix \( y \) \( z \)
assume \( y\in R \), \( z\in J \)
then have \( y\in R \), \( 1 \in R \), \( z\in \langle X\rangle _I \), \( P(z) \) using Ring_ZF_1_L2(2)
with assms(3) have \( P(y\cdot z\cdot 1 ) \) and \( P(1 \cdot z\cdot y) \)
with \( J\subseteq R \), \( y\in R \), \( z\in J \) have \( P(y\cdot z) \) and \( P(z\cdot y) \) using Ring_ZF_1_L4(3), Ring_ZF_1_L3(5,6)
with assms(2), \( z\in \langle X\rangle _I \), \( y\in R \) have \( y\cdot z\in J \), \( z\cdot y\in J \) using ideal_dest_mult, generated_ideal_is_ideal
hence \( \forall x\in J.\ \forall y\in R.\ y \cdot x \in J \wedge x \cdot y \in J \)
moreover have \( \text{IsAsubgroup}(J,A) \)proof
ultimately have \( J\triangleleft R \) unfolding Ideal_def
from assms(1), \( X\subseteq J \), \( J\subseteq R \) have \( J\neq 0 \) and \( J\subseteq R \)
moreover {
}
}
qed
fix \( x \) \( y \)
assume as: \( x\in J \), \( y\in J \)
with assms(2,4) have \( P(x + y) \) using ideal_dest_subset, generated_ideal_is_ideal
with assms(2), \( x\in J \), \( y\in J \) have \( x + y \in J \) using generated_ideal_is_ideal, ideal_dest_sum
then have \( J \text{ is closed under } A \) unfolding IsOpClosed_def
moreover {
fix \( x \)
assume \( x\in J \)
with \( J\subseteq R \) have \( x\in \langle X\rangle _I \), \( x\in R \), \( P(x) \)
with assms(3) have \( P(( - 1 )\cdot x\cdot 1 ) \) using Ring_ZF_1_L2(2), Ring_ZF_1_L3(1)
with assms(2), \( x\in \langle X\rangle _I \), \( x\in R \) have \( ( - x)\in J \) using Ring_ZF_1_L3(1,5,6), Ring_ZF_1_L7(1), Ring_ZF_1_L2(2), generated_ideal_is_ideal, ideal_dest_minus
hence \( \forall x\in J.\ ( - x)\in J \)
ultimately show \( \text{IsAsubgroup}(J,A) \) by (rule group0_3_T3 )
with \( X\subseteq J \) show \( thesis \) using generated_ideal_small
An ideal is very particular with the elements it may contain. If it contains the neutral element of multiplication then it is in fact the whole ring and not a proper subset.
theorem (in ring0) ideal_with_one:
assumes \( I\triangleleft R \), \( 1 \in I \)
shows \( I = R \) using assms, ideal_dest_subset, ideal_dest_mult(2), Ring_ZF_1_L3(5)The only ideal containing an invertible element is the whole ring.
theorem (in ring0) ideal_with_unit:
assumes \( I\triangleleft R \), \( x\in I \), \( \exists y\in R.\ y\cdot x = 1 \vee x\cdot y =1 \)
shows \( I = R \) using assms, ideal_with_one unfolding Ideal_defThe previous result drives us to define what a maximal ideal would be: an ideal such that any bigger ideal is the whole ring:
definition (in ring0)
\( I\triangleleft _mR \equiv I\triangleleft R \wedge I\neq R \wedge (\forall J\in \mathcal{I} .\ I\subseteq J \wedge J\neq R \longrightarrow I=J) \)
Before delving into maximal ideals, lets define some operation on ideals that are useful when formulating some proofs. The product ideal of ideals \(I,J\) is the smallest ideal containing all products of elements from \(I\) and \(J\):
definition (in ring0)
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I\cdot _IJ \equiv \langle M(I\times J)\rangle _I \)
The sum ideal of ideals is the smallest ideal containg both \(I\) and \(J\):
definition (in ring0)
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I+_IJ \equiv \langle I\cup J\rangle _I \)
Sometimes we may need to sum an arbitrary number of ideals, and not just two.
definition (in ring0)
\( \mathcal{J} \subseteq \mathcal{I} \Longrightarrow \oplus _I\mathcal{J} \equiv \langle \bigcup \mathcal{J} \rangle _I \)
Each component of the sum of ideals is contained in the sum.
lemma (in ring0) comp_in_sum_ideals:
assumes \( I\triangleleft R \) and \( J\triangleleft R \)
shows \( I \subseteq I+_IJ \) and \( J \subseteq I+_IJ \) and \( I\cup J \subseteq I+_IJ \)proof from assms have \( I\cup J \subseteq R \) using ideal_dest_subset
with assms show \( I \subseteq I+_IJ \), \( J \subseteq I+_IJ \), \( I\cup J \subseteq I+_IJ \) using generated_ideal_contains_set, sumIdeal_def
qed
Every element in the arbitrary sum of ideals is generated by only a finite subset of those ideals
lemma (in ring0) sum_ideals_finite_sum:
assumes \( \mathcal{J} \subseteq \mathcal{I} \), \( s\in (\oplus _I\mathcal{J} ) \)
shows \( \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ s\in (\oplus _I\mathcal{T} ) \)proof{
}
assume \( \bigcup \mathcal{J} =0 \)
then have \( \mathcal{J} \subseteq \{0\} \)
with assms(2) have \( thesis \) using subset_Finite, nat_into_Finite unfolding FinPow_def
moreover {
}
ultimately show \( thesis \)
qed
let \( P = \lambda t.\ \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ t\in (\oplus _I\mathcal{T} ) \)
assume \( \bigcup \mathcal{J} \neq 0 \)
moreover
}
}
}
from assms(1) have \( \bigcup \mathcal{J} \subseteq R \)
moreover {
fix \( y \) \( z \) \( q \)
assume \( P(q) \), \( y\in R \), \( z\in R \), \( q\in \langle \bigcup \mathcal{J} \rangle _I \)
then obtain \( \mathcal{T} \) where \( \mathcal{T} \in \text{FinPow}(\mathcal{J} ) \) and \( q \in \oplus _I\mathcal{T} \)
from assms(1), \( \mathcal{T} \in \text{FinPow}(\mathcal{J} ) \) have \( \bigcup \mathcal{T} \subseteq R \), \( \mathcal{T} \subseteq \mathcal{I} \) unfolding FinPow_def
with \( q\in \oplus _I\mathcal{T} \), \( y\in R \), \( z\in R \) have \( y\cdot q\cdot z \in \oplus _I\mathcal{T} \) using generated_ideal_is_ideal, sumArbitraryIdeals_def unfolding Ideal_def
with \( \mathcal{T} \in \text{FinPow}(\mathcal{J} ) \) have \( P(y\cdot q \cdot z) \)
hence \( \forall y\in R.\ \forall z\in R.\ \forall q\in \langle \bigcup \mathcal{J} \rangle _I.\ P(q) \longrightarrow P(y\cdot q\cdot z) \)
moreover {
fix \( y \) \( z \)
assume \( P(y) \), \( P(z) \)
then obtain \( T_y \) \( T_z \) where T: \( T_y\in \text{FinPow}(\mathcal{J} ) \), \( y \in \oplus _IT_y \), \( T_z\in \text{FinPow}(\mathcal{J} ) \), \( z \in \oplus _IT_z \)
from T(1,3) have A: \( T_y\cup T_z \in \text{FinPow}(\mathcal{J} ) \) unfolding FinPow_def using Finite_Un
with assms(1) have \( \bigcup T_y \subseteq \bigcup (T_y\cup T_z) \), \( \bigcup T_z \subseteq \bigcup (T_y\cup T_z) \) and sub: \( \bigcup (T_y\cup T_z) \subseteq R \) unfolding FinPow_def
then have \( \bigcup (T_y\cup T_z) \subseteq \langle \bigcup (T_y\cup T_z)\rangle _I \) using generated_ideal_contains_set
hence \( \bigcup T_y \subseteq \langle \bigcup (T_y\cup T_z)\rangle _I \), \( \bigcup T_z \subseteq \langle \bigcup (T_y\cup T_z)\rangle _I \)
with sub have \( \langle \bigcup T_y\rangle _I\subseteq \langle \bigcup (T_y\cup T_z)\rangle _I \), \( \langle \bigcup T_z\rangle _I \subseteq \langle \bigcup (T_y\cup T_z)\rangle _I \) using generated_ideal_small, generated_ideal_is_ideal
moreover
from assms(1), T(1,3) have \( T_y\subseteq \mathcal{I} \), \( T_z\subseteq \mathcal{I} \) unfolding FinPow_def
moreover note T(2,4)
ultimately have \( y \in \langle \bigcup (T_y\cup T_z)\rangle _I \), \( z \in \langle \bigcup (T_y\cup T_z)\rangle _I \) using sumArbitraryIdeals_def, sumArbitraryIdeals_def
with \( \bigcup (T_y\cup T_z) \subseteq R \) have \( y + z \in \langle \bigcup (T_y\cup T_z)\rangle _I \) using generated_ideal_is_ideal, ideal_dest_sum
moreover
from \( T_y\subseteq \mathcal{I} \), \( T_z\subseteq \mathcal{I} \) have \( T_y\cup T_z \subseteq \mathcal{I} \)
then have \( (\oplus _I(T_y\cup T_z)) = \langle \bigcup (T_y\cup T_z)\rangle _I \) using sumArbitraryIdeals_def
ultimately have \( y + z \in (\oplus _I(T_y\cup T_z)) \)
with A have \( P(y + z) \)
hence \( \forall y\in R.\ \forall z\in R.\ P(y) \wedge P(z) \longrightarrow P(y + z) \)
moreover {
fix \( t \)
assume \( t\in \bigcup \mathcal{J} \)
then obtain \( J \) where \( t\in J \), \( J\in \mathcal{J} \)
then have \( \{J\}\in \text{FinPow}(\mathcal{J} ) \) unfolding FinPow_def using eqpoll_imp_Finite_iff, nat_into_Finite
moreover
from assms(1), \( J\in \mathcal{J} \) have \( (\oplus _I\{J\}) = \langle J\rangle _I \) using sumArbitraryIdeals_def
with assms(1), \( t\in J \), \( J\in \mathcal{J} \) have \( t\in (\oplus _I\{J\}) \) using generated_ideal_contains_set
ultimately have \( P(t) \)
hence \( \forall t\in \bigcup \mathcal{J} .\ P(t) \)
ultimately have \( \forall t\in \langle \bigcup \mathcal{J} \rangle _I.\ P(t) \) by (rule induction_generated_ideal )
with assms have \( thesis \) using sumArbitraryIdeals_def
By definition of product of ideals and of an ideal itself, it follows that the product of ideals is an ideal contained in the intersection
theorem (in ring0) product_in_intersection:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( I\cdot _IJ \subseteq I\cap J \) and \( (I\cdot _IJ)\triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \)proof have \( M(I\times J) \subseteq I\cap J \)proof
fix \( x \)
assume \( x\in M(I\times J) \)
then obtain \( y \) where \( y\in I\times J \), \( \langle y,x\rangle \in M \) unfolding image_def
then obtain \( y_i \) \( y_j \) where y: \( y_i\in I \), \( y_j\in J \), \( \langle \langle y_i,y_j\rangle ,x\rangle \in M \)
from assms have \( I\subseteq R \), \( J\subseteq R \) using ideal_dest_subset
with ringAssum, assms, y show \( x\in I\cap J \) unfolding Ideal_def, IsAring_def, IsAmonoid_def, IsAssociative_def using apply_equality
qed
with assms show \( I\cdot _IJ \subseteq I\cap J \) using productIdeal_def, generated_ideal_small, inter_two_ideals
from assms, \( M(I\times J) \subseteq I\cap J \) have \( M(I\times J) \subseteq R \) using ideal_dest_subset
with assms show \( (I\cdot _IJ) \triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \) using productIdeal_def, generated_ideal_is_ideal, generated_ideal_contains_set
qed
We will show now that the sum of ideals is no more that the sum of the ideal elements.
lemma (in ring0) sum_elements:
assumes \( I \triangleleft R \), \( J \triangleleft R \), \( x\in I \), \( y\in J \)
shows \( x + y \in I+_IJ \)proof from assms(1,2) have \( I\cup J \subseteq R \) using ideal_dest_subset
with assms(3,4) have \( x \in \langle I\cup J\rangle _I \), \( y \in \langle I\cup J\rangle _I \) using generated_ideal_contains_set
with assms(1,2), \( I\cup J \subseteq R \) show \( thesis \) using generated_ideal_is_ideal, ideal_dest_subset, ideal_dest_sum, sumIdeal_def
qed
For two ideals the set containing all sums of their elements is also an ideal.
lemma (in ring0) sum_elements_is_ideal:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (A(I\times J)) \triangleleft R \)proof from assms have ij: \( I\times J \subseteq R\times R \) using ideal_dest_subset
have Aim: \( A(I\times J) \subseteq R \) using group_oper_fun, func1_1_L6(2)
moreover {
}
qed
fix \( x \) \( y \)
assume \( x\in R \), \( y \in A(I\times J) \)
from ij, \( y\in A(I\times J) \) obtain \( y_i \) \( y_j \) where y: \( y=y_i + y_j \), \( y_i\in I \), \( y_j\in J \) using group_oper_fun, func_imagedef
from \( x\in R \), y, ij have \( x\cdot y = (x\cdot y_i) + (x\cdot y_j) \) and \( y\cdot x = (y_i\cdot x) + (y_j\cdot x) \) using ring_oper_distr, group_op_closed
moreover
from assms, \( x\in R \), y(2,3) have \( x\cdot y_i \in I \), \( y_i\cdot x \in I \), \( x\cdot y_j \in J \), \( y_j\cdot x \in J \) using ideal_dest_mult
ultimately have \( x\cdot y\in A(I\times J) \), \( y\cdot x\in A(I\times J) \) using ij, group_oper_fun, func_imagedef
hence \( \forall x\in A(I\times J).\ \forall y\in R.\ y \cdot x \in A(I\times J) \wedge x \cdot y \in A(I\times J) \)
moreover have \( \text{IsAsubgroup}(A(I\times J),A) \)proof
ultimately show \( (A(I \times J)) \triangleleft R \) unfolding Ideal_def
from assms, ij have \( 0 + 0 \in A (I \times J) \) using group_oper_fun, ideal_dest_zero, func_imagedef
with Aim have \( A(I \times J) \neq 0 \) and \( A(I \times J) \subseteq R \)
moreover {
}
}
qed
fix \( x \) \( y \)
assume xy: \( x \in A(I \times J) \), \( y \in A(I \times J) \)
with ij obtain \( x_i \) \( x_j \) \( y_i \) \( y_j \) where \( x_i\in I \), \( x_j\in J \), \( x=x_i + x_j \), \( y_i\in I \), \( y_j\in J \), \( y=y_i + y_j \) using group_oper_fun, func_imagedef
from \( x\in A(I \times J) \), \( A(I \times J)\subseteq R \) have \( x\in R \)
from assms, \( x_i\in I \), \( x_j\in J \), \( y_i\in I \), \( y_j\in J \) have \( x_i\in R \), \( x_j\in R \), \( y_i\in R \), \( y_j\in R \) using ideal_dest_subset
from ij, \( x\in R \), \( y_i\in R \), \( y_j\in R \), \( y=y_i + y_j \) have \( x + y = (x + y_i) + y_j \) using Ring_ZF_1_L10(1)
with \( x=x_i + x_j \), \( x_i\in R \), \( x_j\in R \), \( y_i\in R \), \( y_j\in R \) have \( x + y = (x_i + y_i) + (x_j + y_j) \) using Ring_ZF_2_L5(4)
moreover
from assms, \( x_i\in I \), \( x_j\in J \), \( y_i\in I \), \( y_j\in J \) have \( x_i + y_i \in I \) and \( x_j + y_j \in J \) using ideal_dest_sum
ultimately have \( x + y \in A(I\times J) \) using ij, group_oper_fun, func_imagedef
then have \( A(I \times J) \text{ is closed under } A \) unfolding IsOpClosed_def
moreover {
fix \( x \)
assume \( x \in A(I \times J) \)
with ij obtain \( x_i \) \( x_j \) where \( x_i\in I \), \( x_j\in J \), \( x=x_i + x_j \) using group_oper_fun, func_imagedef
with assms have \( ( - x) = ( - x_i) - x_j \) using Ring_ZF_1_L9(2), ideal_dest_subset
moreover
from assms, \( x_i\in I \), \( x_j\in J \) have \( ( - x_i)\in I \) and \( ( - x_j)\in J \) using ideal_dest_minus
ultimately have \( ( - x) \in A(I\times J) \) using group_oper_fun, ij, func_imagedef
hence \( \forall x\in A(I \times J).\ ( - x) \in A(I \times J) \)
ultimately show \( thesis \) using group0_3_T3
The set of all sums of elements of two ideals is their sum ideal i.e. the ideal generated by their union.
corollary (in ring0) sum_ideals_is_sum_elements:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (A(I \times J)) = I+_IJ \)proof from assms have ij: \( I\subseteq R \), \( J\subseteq R \) using ideal_dest_subset
then have ij_prd: \( I\times J \subseteq R\times R \)
with assms show \( A(I \times J) \subseteq I +_I J \) using group_oper_fun, sum_elements, func_imagedef
{
fix \( x \)
assume \( x\in I \)
with ij(1) have \( x=x + 0 \) using Ring_ZF_1_L3(3)
with assms(2), ij_prd, \( x\in I \) have \( x\in A (I \times J) \) using group0_3_L5, group_oper_fun, func_imagedef unfolding Ideal_def
hence \( I \subseteq A(I \times J) \)
moreover {
}
qed
fix \( x \)
assume x: \( x\in J \)
with ij(2) have \( x= 0 + x \) using Ring_ZF_1_L3(4)
with assms(1), ij_prd, \( x\in J \) have \( x \in A(I \times J) \) using group0_3_L5, group_oper_fun, func_imagedef unfolding Ideal_def
hence \( J \subseteq A(I \times J) \)
ultimately have \( I\cup J \subseteq A(I \times J) \)
with assms show \( I+_IJ \subseteq A(I \times J) \) using generated_ideal_small, sum_elements_is_ideal, sumIdeal_def
The sum ideal of two ideals is indeed an ideal.
corollary (in ring0) sum_ideals_is_ideal:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (I+_IJ) \triangleleft R \) using assms, sum_ideals_is_sum_elements, sum_elements_is_ideal, ideal_dest_subsetThe operation of taking the sum of ideals is commutative.
corollary (in ring0) sum_ideals_commute:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( (I +_I J) = (J +_I I) \)proof have \( I \cup J = J \cup I \)
with assms show \( thesis \) using sumIdeal_def
qed
Now that we know what the product of ideals is, we are able to define what a prime ideal is:
definition (in ring0)
\( 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)) \)
Any maximal ideal is a prime ideal.
theorem (in ring0) maximal_is_prime:
assumes \( Q\triangleleft _mR \)
shows \( Q\triangleleft _pR \)proof have \( Q\in \mathcal{I} \) using assms, ideal_dest_subset unfolding maximalIdeal_def
{
fix \( I \) \( J \)
assume \( I\in \mathcal{I} \), \( J\in \mathcal{I} \), \( I\cdot _IJ \subseteq Q \)
{
assume K: \( \neg (I\subseteq Q) \), \( \neg (J\subseteq Q) \)
from \( \neg (I\subseteq Q) \) obtain \( x \) where \( x\in I-Q \)
with \( I\in \mathcal{I} \) have \( x\in R \) using ideal_dest_subset
from \( I\in \mathcal{I} \), \( J\in \mathcal{I} \) have sub: \( I\times J \subseteq R\times R \)
let \( K = \langle Q\cup \{x\}\rangle _I \)
from \( Q\in \mathcal{I} \), \( x\in R \) have \( Q\cup \{x\} \subseteq R \)
then have \( Q\subseteq K \) and \( x\in K \) using generated_ideal_contains_set
with \( x\in I-Q \) have \( Q\subseteq K \), \( K\neq Q \)
from \( Q\cup \{x\} \subseteq R \) have \( K\in \mathcal{I} \) using ideal_dest_subset, generated_ideal_is_ideal
with assms, \( Q\subseteq K \), \( K\neq Q \) have \( K=R \) unfolding maximalIdeal_def
let \( P = Q+_II \)
from \( Q\in \mathcal{I} \), \( I\in \mathcal{I} \), \( x\in I-Q \) have \( Q\cup \{x\} \subseteq Q+_II \) using comp_in_sum_ideals(3)
with \( Q\in \mathcal{I} \), \( I\in \mathcal{I} \) have \( K \subseteq Q+_II \), \( Q+_II \subseteq R \) using sum_ideals_is_ideal, generated_ideal_small, ideal_dest_subset
with \( K=R \) have \( 1 \in Q+_II \) using Ring_ZF_1_L2(2)
with \( I\in \mathcal{I} \), \( Q\in \mathcal{I} \) have \( 1 \in A(Q\times I) \) using sum_ideals_is_sum_elements
moreover
{
from \( I\in \mathcal{I} \), \( Q\in \mathcal{I} \) have \( Q\times I \subseteq R\times R \)
ultimately obtain \( x_m \) \( x_i \) where \( x_m\in Q \), \( x_i\in I \), \( 1 =x_m + x_i \) using func_imagedef, group_oper_fun
fix \( y \)
assume \( y\in J \)
with \( x_m\in Q \), \( x_i\in I \), \( Q\in \mathcal{I} \), \( I\in \mathcal{I} \), \( J\in \mathcal{I} \) have \( y\in R \), \( x_m\in R \), \( x_i\in R \)
with \( y\in J \), \( J\in \mathcal{I} \), \( 1 =x_m + x_i \) have \( (x_m\cdot y) + (x_i\cdot y) = y \) using Ring_ZF_1_L3(6), ring_oper_distr(2)
from \( Q\in \mathcal{I} \), \( x_m\in Q \), \( y\in R \) have \( x_m\cdot y\in Q \) using ideal_dest_mult(1)
from sub, \( y\in J \), \( x_i\in I \), \( I\in \mathcal{I} \), \( J\in \mathcal{I} \), \( I\cdot _IJ\subseteq Q \) have \( x_i\cdot y\in Q \) using func_imagedef, monoid_oper_fun, product_in_intersection(3)
with \( Q\in \mathcal{I} \), \( (x_m\cdot y) + (x_i\cdot y) = y \), \( x_m\cdot y\in Q \) have \( y\in Q \) using ideal_dest_sum
hence \( J \subseteq Q \)
with K have \( False \)
hence \( (I\subseteq Q)\vee (J\subseteq Q) \)
hence \( \forall I\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ I \cdot _I J \subseteq Q \longrightarrow (I \subseteq Q \vee J \subseteq Q) \)
with assms show \( thesis \) unfolding maximalIdeal_def, primeIdeal_def
qed
In case of non-commutative rings, the zero divisor concept is too constrictive. For that we define the following concept of a prime ring. Note that in case that our ring is commutative, this is equivalent to having no zero divisors (there is no of that proof yet).
definition
\( \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)) \)
Prime rings appear when the zero ideal is prime.
lemma (in ring0) prime_ring_zero_prime_ideal:
assumes \( [R,A,M]\text{ is a prime ring } \), \( R\neq \{ 0 \} \)
shows \( \{ 0 \} \triangleleft _pR \)proof{
}
}
}
fix \( I \) \( J \)
assume ij: \( I\in \mathcal{I} \), \( J\in \mathcal{I} \), \( I\cdot _IJ \subseteq \{ 0 \} \)
from ij(1,2) have \( I\times J \subseteq R\times R \)
{
assume \( \neg (I\subseteq \{ 0 \}) \), \( \neg (J\subseteq \{ 0 \}) \)
then obtain \( x_i \) \( x_j \) where \( x_i\neq 0 \), \( x_j\neq 0 \), \( x_i\in I \), \( x_j\in J \)
from ij(1,2), \( x_i\in I \), \( x_j\in J \) have \( x_i\in R \), \( x_j\in R \)
{
fix \( u \)
assume \( u\in R \)
with \( I\in \mathcal{I} \), \( x_i\in I \), \( x_j\in J \), \( I\times J \subseteq R\times R \) have \( x_i\cdot u\cdot x_j \in M(I\times J) \) using ideal_dest_mult(1), func_imagedef, monoid_oper_fun
with ij have \( x_i\cdot u\cdot x_j = 0 \) using product_in_intersection(3)
hence \( \forall u\in R.\ x_i\cdot u\cdot x_j = 0 \)
with ringAssum, assms(1), \( x_i\in R \), \( x_j\in R \), \( x_i\neq 0 \), \( x_j\neq 0 \) have \( False \) using primeRing_def
hence \( I\subseteq \{ 0 \} \vee J\subseteq \{ 0 \} \)
hence \( \forall I\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ I \cdot _I J \subseteq \{ 0 \} \longrightarrow (I \subseteq \{ 0 \} \vee J \subseteq \{ 0 \}) \)
with assms(2) show \( thesis \) using zero_ideal unfolding primeIdeal_def
qed
If the trivial ideal \(\{ 0\}\) is a prime ideal then the ring is a prime ring.
lemma (in ring0) zero_prime_ideal_prime_ring:
assumes \( \{ 0 \}\triangleleft _pR \)
shows \( [R,A,M]\text{ is a prime ring } \)proof{
}
fix \( x \) \( y \) \( z \)
assume \( x\in R \), \( y\in R \), \( \forall z\in R.\ x\cdot z\cdot y = 0 \)
let \( X = \langle \{x\}\rangle _I \)
let \( Y = \langle \{y\}\rangle _I \)
from \( x\in R \), \( y\in R \) have \( X\times Y \subseteq R\times R \) using generated_ideal_is_ideal, ideal_dest_subset
let \( P = \lambda q.\ (\forall z\in Y.\ q\cdot z = 0 ) \)
let \( Q = \lambda q.\ (\forall z\in R.\ x\cdot z\cdot q = 0 ) \)
have \( \forall y\in Y.\ Q(y) \)proof
from \( y\in R \) have \( \{y\}\neq 0 \) and \( \{y\}\subseteq R \)
moreover {
}
}
qed
fix \( s \) \( t \) \( q \)
assume yzq: \( s\in R \), \( t\in R \), \( q \in \langle \{y\}\rangle _I \), \( \forall k\in R.\ x\cdot k\cdot q = 0 \)
from \( y\in R \), yzq(3) have \( q\in R \) using generated_ideal_is_ideal, ideal_dest_subset
{
fix \( u \)
assume \( u\in R \)
from yzq(1,2), \( x\in R \), \( q\in R \), \( u\in R \) have \( x\cdot u\cdot (s\cdot q\cdot t) = (x\cdot (u\cdot s)\cdot q)\cdot t \) using Ring_ZF_1_L11(2), Ring_ZF_1_L4(3)
with \( u\in R \), yzq(1,2,4) have \( x\cdot u\cdot (s\cdot q\cdot t) = 0 \) using Ring_ZF_1_L4(3), Ring_ZF_1_L6(1)
hence \( \forall z_a\in R.\ x\cdot z_a\cdot (s\cdot q\cdot t) = 0 \)
hence \( \forall t\in R.\ \forall z\in R.\ \forall q\in \langle \{y\}\rangle _I.\ \)
\( (\forall z\in R.\ x\cdot z\cdot q = 0 ) \longrightarrow (\forall z_a\in R.\ x\cdot z_a\cdot (t\cdot q\cdot z) = 0 ) \)
moreover from \( x\in R \) have \( \forall y\in R.\ \forall z\in R.\ \)
\( (\forall z\in R.\ x\cdot z\cdot y = 0 ) \wedge (\forall z_a\in R.\ x\cdot z_a\cdot z = 0 ) \longrightarrow \)
\( (\forall z_a\in R.\ x\cdot z_a\cdot (y + z) = 0 ) \) using ring_oper_distr(1), Ring_ZF_1_L4(3), Ring_ZF_1_L3(3), Ring_ZF_1_L2(1)
moreover from \( \forall z\in R.\ x\cdot z\cdot y = 0 \) have \( \forall x_a\in \{y\}.\ \forall z\in R.\ x\cdot z\cdot x_a = 0 \)
ultimately show \( thesis \) by (rule induction_generated_ideal )
from \( x\in R \), \( \forall y\in Y.\ Q(y) \) have \( \forall y\in Y.\ x\cdot y = 0 \) using Ring_ZF_1_L2(2), Ring_ZF_1_L3(5)
from \( y\in R \) have \( Y\triangleleft R \), \( Y\subseteq R \) using generated_ideal_is_ideal, ideal_dest_subset
have \( \forall y\in X.\ P(y) \)proof
from \( x\in R \) have \( \{x\}\neq 0 \), \( \{x\}\subseteq R \)
moreover {
}
qed
fix \( q_1 \) \( q_2 \) \( q_3 \)
assume q: \( q_1\in R \), \( q_2\in R \), \( q_3 \in \langle \{x\}\rangle _I \), \( \forall k\in Y.\ q_3\cdot k = 0 \)
from \( x\in R \), \( q_3 \in \langle \{x\}\rangle _I \) have \( q_3\in R \) using generated_ideal_is_ideal, ideal_dest_subset
with \( Y\triangleleft R \), \( Y\subseteq R \), q(1,2,4) have \( \forall z_a\in \langle \{y\}\rangle _I.\ q_1\cdot q_3\cdot q_2 \cdot z_a = 0 \) using ideal_dest_mult(2), Ring_ZF_1_L4(3), Ring_ZF_1_L11(2), Ring_ZF_1_L6(2)
hence \( \forall y_a\in R.\ \forall z\in R.\ \forall q\in \langle \{x\}\rangle _I.\ \)
\( (\forall z\in \langle \{y\}\rangle _I.\ q\cdot z = 0 ) \longrightarrow (\forall z_a\in \langle \{y\}\rangle _I.\ y_a\cdot q\cdot z\cdot z_a = 0 ) \)
moreover from \( Y\subseteq R \) have \( \forall y_a\in R.\ \forall z\in R.\ \)
\( (\forall z\in \langle \{y\}\rangle _I.\ y_a\cdot z = 0 ) \wedge (\forall z_a\in \langle \{y\}\rangle _I.\ z\cdot z_a = 0 ) \longrightarrow \)
\( (\forall z_a\in \langle \{y\}\rangle _I.\ (y_a + z)\cdot z_a = 0 ) \) using ring_oper_distr(2), Ring_ZF_1_L3(3), Ring_ZF_1_L2(1)
moreover from \( \forall y\in Y.\ x\cdot y = 0 \) have \( \forall x\in \{x\}.\ \forall z\in \langle \{y\}\rangle _I.\ x\cdot z = 0 \)
ultimately show \( thesis \) by (rule induction_generated_ideal )
from \( X\times Y \subseteq R\times R \), \( \forall y\in X.\ P(y) \) have \( M(X\times Y) \subseteq \{ 0 \} \) using monoid_oper_fun, func_imagedef
with \( x\in R \), \( y\in R \) have \( X\cdot _IY \subseteq \{ 0 \} \) using generated_ideal_small, zero_ideal, productIdeal_def, generated_ideal_is_ideal
with assms, \( x\in R \), \( y\in R \) have \( X \subseteq \{ 0 \} \vee Y \subseteq \{ 0 \} \) using generated_ideal_is_ideal, ideal_dest_subset unfolding primeIdeal_def
with \( x\in R \), \( y\in R \) have \( x= 0 \vee y= 0 \) using generated_ideal_contains_set
hence \( \forall x\in R.\ \forall y\in R.\ (\forall z\in R.\ x\cdot z\cdot y = 0 ) \longrightarrow x= 0 \vee y= 0 \)
with ringAssum show \( thesis \) using primeRing_def
qed
We can actually use this definition of a prime ring as a condition to check for prime ideals.
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 \)proof{
}
}
fix \( x \) \( y \)
assume \( x\in R \), \( y\in R \), \( \forall z\in R.\ x\cdot z\cdot y\in P \), \( y\notin P \)
let \( X = \langle \{x\}\rangle _I \)
let \( Y = \langle \{y\}\rangle _I \)
from \( y\in R \) have \( \{y\}\neq 0 \) and \( \{y\}\subseteq R \)
moreover
have \( \forall y_a\in R.\ \)
\( \forall z\in R.\ \forall q\in \langle \{y\}\rangle _I.\ (\forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot q \in P) \longrightarrow \)
\( (\forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot (y_a\cdot q\cdot z) \in P) \)proof
moreover {
}
fix \( y_a \) \( z \) \( q \) \( t \) \( u \)
assume \( y_a\in R \), \( z\in R \), \( q\in Y \), \( \forall t\in X.\ \forall u\in R.\ t\cdot u\cdot q\in P \), \( t\in X \), \( u\in R \)
from \( x\in R \), \( y\in R \), \( q\in Y \), \( t\in X \) have \( q\in R \), \( t\in R \) using generated_ideal_is_ideal, ideal_dest_subset
from \( y_a\in R \), \( u\in R \) have \( u\cdot y_a\in R \) using Ring_ZF_1_L4(3)
with assms, \( z\in R \), \( \forall t\in X.\ \forall u\in R.\ t\cdot u\cdot q\in P \), \( t\in X \) have \( (t\cdot (u\cdot y_a)\cdot q)\cdot z \in P \) using ideal_dest_mult(1) unfolding primeIdeal_def
with \( y_a\in R \), \( z\in R \), \( u\in R \), \( q\in R \), \( t\in R \) have \( t\cdot u\cdot (y_a\cdot q\cdot z) \in P \) using Ring_ZF_1_L4(3), Ring_ZF_1_L11(2)
thus \( thesis \)
qed
have \( \forall y\in R.\ \forall z\in R.\ \)
\( (\forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot y \in P) \wedge (\forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot z \in P) \longrightarrow \)
\( (\forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot (y + z) \in P) \)proof
moreover {
}
fix \( y_a \) \( z \) \( t \) \( u \)
assume ass: \( y_a\in R \), \( z\in R \), \( t\in X \), \( u\in R \), \( \forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot y_a\in P \), \( \forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot z\in P \)
from \( x\in R \), \( t\in X \) have \( t\in R \) using ideal_dest_subset, generated_ideal_is_ideal
from assms, ass(3,4,5,6) have \( (t\cdot u\cdot y_a) + (t\cdot u\cdot z) \in P \) using ideal_dest_sum unfolding primeIdeal_def
with \( t\in R \), \( y_a\in R \), \( z\in R \), \( u\in R \) have \( t\cdot u\cdot (y_a + z) \in P \) using Ring_ZF_1_L4(3), ring_oper_distr(1)
thus \( thesis \)
qed
have \( \forall y_a\in \langle \{x\}\rangle _I.\ \forall u\in R.\ y_a\cdot u\cdot y \in P \)proof
from \( x\in R \) have \( \{x\}\neq 0 \) and \( \{x\}\subseteq R \)
moreover
qed
have \( \forall y_a\in R.\ \forall z\in R.\ \forall q\in X.\ \)
\( (\forall u\in R.\ q\cdot u\cdot y \in P) \longrightarrow (\forall u\in R.\ y_a\cdot q\cdot z\cdot u\cdot y \in P) \)proof
moreover {
}
fix \( y_a \) \( z \) \( q \) \( u \)
assume ass: \( y_a\in R \), \( z\in R \), \( q\in X \), \( \forall u\in R.\ q\cdot u\cdot y \in P \), \( u \in R \)
from \( x\in R \), \( q\in X \) have q: \( q\in R \) using generated_ideal_is_ideal, ideal_dest_subset
from assms, ass(1,2,4,5) have \( y_a\cdot (q\cdot (z\cdot u)\cdot y) \in P \) using Ring_ZF_1_L4(3), ideal_dest_mult(2) unfolding primeIdeal_def
with \( y\in R \), \( y_a\in R \), \( z\in R \), \( u \in R \), \( q\in R \) have \( y_a\cdot q\cdot z\cdot u\cdot y \in P \) using Ring_ZF_1_L4(3), Ring_ZF_1_L11(2)
thus \( thesis \)
qed
have \( \forall y_a\in R.\ \forall z\in R.\ \)
\( (\forall u\in R.\ y_a\cdot u\cdot y \in P) \wedge (\forall u\in R.\ z\cdot u\cdot y \in P) \longrightarrow (\forall u\in R.\ (y_a + z)\cdot u\cdot y \in P) \)proof
moreover {
}
fix \( y_a \) \( z \) \( u \)
assume \( y_a\in R \), \( z\in R \), \( u\in R \), \( \forall u\in R.\ y_a\cdot u\cdot y \in P \), \( \forall u\in R.\ z\cdot u\cdot y \in P \)
with assms, \( y\in R \) have \( ((y_a + z)\cdot u)\cdot y\in P \) using ideal_dest_sum, ring_oper_distr(2), Ring_ZF_1_L4(3) unfolding primeIdeal_def
thus \( thesis \)
qed
from \( \forall z\in R.\ x\cdot z\cdot y\in P \) have \( \forall x\in \{x\}.\ \forall u\in R.\ x\cdot u\cdot y \in P \)
ultimately show \( thesis \) by (rule induction_generated_ideal )
hence \( \forall x_a\in \{y\}.\ \forall t\in \langle \{x\}\rangle _I.\ \forall u\in R.\ t\cdot u\cdot x_a \in P \)
ultimately have R: \( \forall q\in Y.\ \forall t\in X.\ \forall u\in R.\ t\cdot u\cdot q \in P \) by (rule induction_generated_ideal )
from \( x\in R \), \( y\in R \) have subprd: \( X\times Y \subseteq R\times R \) using ideal_dest_subset, generated_ideal_is_ideal
{
fix \( t \)
assume \( t \in M(X\times Y) \)
with subprd obtain \( t_x \) \( t_y \) where \( t_x\in X \), \( t_y\in Y \) and t: \( t= t_x\cdot t_y \) using func_imagedef, monoid_oper_fun
with R, \( t_x\in X \), \( t_y\in Y \) have \( t_x\cdot 1 \cdot t_y \in P \) using Ring_ZF_1_L2(2)
moreover
from \( x\in R \), \( t_x\in X \) have \( t_x\in R \) using generated_ideal_is_ideal, ideal_dest_subset
ultimately have \( t\in P \) using Ring_ZF_1_L3(5), t
hence \( M(X\times Y) \subseteq P \)
with assms, \( x\in R \), \( y\in R \) have \( X \subseteq P \vee Y \subseteq P \) unfolding primeIdeal_def using generated_ideal_small, productIdeal_def, generated_ideal_is_ideal, ideal_dest_subset
with \( x\in R \), \( y\in R \), \( y\notin P \) have \( x\in P \) using generated_ideal_contains_set
thus \( thesis \)
qed
The next theorem provides a sufficient condition for a proper ideal \(P\) to be a prime ideal: if for all \(x,y\in R\) it holds that for all \(z\in R\) \(x z y \in P\) only when \(x\in P\) or \(y\in P\) then \(P\) is a prime ideal.
theorem (in ring0) equivalent_prime_ideal_2:
assumes \( \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 \), \( P\triangleleft R \), \( P\neq R \)
shows \( P\triangleleft _pR \)proof{
}
}
fix \( I \) \( J \) \( x \) \( x_a \)
assume \( I\triangleleft R \), \( I\subseteq R \), \( J\triangleleft R \), \( J\subseteq R \), \( I\cdot _IJ \subseteq P \), \( x\in J \), \( x\notin P \), \( x_a\in I \)
from \( I\subseteq R \), \( J\subseteq R \) have \( I\times J \subseteq R\times R \)
{
fix \( z \)
assume \( z\in R \)
with \( I\triangleleft R \), \( x\in J \), \( x_a\in I \), \( I\times J \subseteq R\times R \) have \( (x_a\cdot z\cdot x)\in M(I\times J) \) using ideal_dest_mult(1), func_imagedef, monoid_oper_fun
with \( I\triangleleft R \), \( J\triangleleft R \), \( I\cdot _IJ \subseteq P \) have \( x_a\cdot z\cdot x \in P \) using generated_ideal_contains_set, func1_1_L6(2), monoid_oper_fun, productIdeal_def
with assms(1), \( I\subseteq R \), \( J\subseteq R \), \( x\in J \), \( x\notin P \), \( x_a\in I \) have \( x_a\in P \)
with assms(2,3) show \( thesis \) unfolding primeIdeal_def
qed
Ring quotient
Similar to groups, rings can be quotiented by normal additive subgroups; but to keep the structure of the multiplicative monoid we need extra structure in the normal subgroup. This extra structure is given by the ideal.
Any ideal is a normal subgroup.
lemma (in ring0) ideal_normal_add_subgroup:
assumes \( I\triangleleft R \)
shows \( \text{IsAnormalSubgroup}(R,A,I) \) using ringAssum, assms, Group_ZF_2_4_L6(1) unfolding IsAring_def, Ideal_defEach ring \(R\) is a group with respect to its addition operation. By the lemma ideal_normal_add_subgroup above an ideal \(I\subseteq R\) is a normal subgroup of that group. Therefore we can define the quotient of the ring \(R\) by the ideal \(I\) using the notion of quotient of a group by its normal subgroup, see section Normal subgroups and quotient groups in Group_ZF_2 theory.
definition (in ring0)
\( I\triangleleft R \Longrightarrow \text{QuotientBy}(I) \equiv R// \text{QuotientGroupRel}(R,A,I) \)
Any ideal gives rise to an equivalence relation
corollary (in ring0) ideal_equiv_rel:
assumes \( I\triangleleft R \)
shows \( \text{equiv}(R, \text{QuotientGroupRel}(R,A,I)) \) using assms, Group_ZF_2_4_L3 unfolding Ideal_defAny quotient by an ideal is an abelian group.
lemma (in ring0) quotientBy_add_group:
assumes \( I\triangleleft R \)
shows \( \text{IsAgroup}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \) and \( \text{QuotientGroupOp}(R, A, I) \text{ is commutative on } \text{QuotientBy}(I) \) using assms, ringAssum, ideal_normal_add_subgroup, Group_ZF_2_4_T1, Group_ZF_2_4_L6(2), QuotientBy_def, QuotientBy_def, Ideal_def unfolding IsAring_defSince every ideal is a normal subgroup of the additive group of the ring it is quite obvious that that addition is congruent with respect to the quotient group relation. The next lemma shows something a little bit less obvious: that the multiplicative ring operation is also congruent with the quotient relation and gives rise to a monoid in the quotient.
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)) \)proof let \( r = \text{QuotientGroupRel}(R,A,I) \)
{
fix \( x \) \( y \) \( s \) \( t \)
assume \( \langle x,y\rangle \in r \) and \( \langle s,t\rangle \in r \)
then have xyst: \( x\in R \), \( y\in R \), \( s\in R \), \( t\in R \), \( x - y \in I \), \( s - t \in I \) unfolding QuotientGroupRel_def
from \( x\in R \), \( y\in R \), \( s\in R \) have \( (x\cdot s) - (y\cdot t) = ((x\cdot s) + (( - (y\cdot s)) + (y\cdot s))) - (y\cdot t) \) using Ring_ZF_1_L3(1,3,7), Ring_ZF_1_L4(3,4)
with \( x\in R \), \( y\in R \), \( s\in R \), \( t\in R \) have \( (x\cdot s) - (y\cdot t) = ((x\cdot s) - (y\cdot s)) + ((y\cdot s) - (y\cdot t)) \) using Ring_ZF_1_L3(1), Ring_ZF_1_L4(1,2,3), Ring_ZF_1_L10(1)
with \( x\in R \), \( y\in R \), \( s\in R \), \( t\in R \) have \( (x\cdot s) - (y\cdot t) = ((x - y)\cdot s) + (y\cdot (s - t)) \) using Ring_ZF_1_L8
with assms, xyst have \( \langle M\langle x,s\rangle ,M\langle y,t\rangle \rangle \in r \) using ideal_dest_sum, ideal_dest_mult(1,2), Ring_ZF_1_L4(3) unfolding QuotientGroupRel_def
then show \( \text{Congruent2}(r,M) \) unfolding Congruent2_def
with assms show \( \text{IsAmonoid}( \text{QuotientBy}(I), \text{ProjFun2}(R,r, M)) \) using Group_ZF_2_4_L3, Group_ZF_2_2_T1, QuotientBy_def unfolding Ideal_def
qed
Each ideal defines an equivalence relation on the ring with which both addition and multiplication are congruent. The next couple of definitions set up notation for the operations that result from projecting the ring addition and multiplication on the quotient space. We will write \(x+_I y \) to denote the result of the quotient operation (with respect to an ideal I) on classes \(x\) and \(y\)
definition (in ring0)
\( x\{ + I\}y \equiv \text{QuotientGroupOp}(R, A, I)\langle x,y\rangle \)
Similarly \(x \cdot_I y\) is the value of the projection of the ring's multiplication on the quotient space defined by the an ideal \(I\), which as we know is a normal subgroup of the ring with addition.
definition (in ring0)
\( x\{\cdot I\}y \equiv \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle x,y\rangle \)
The value of the projection of taking the negative in the ring on the quotient space defined by an ideal \(I\) will be denoted \( \{ - I\} \).
definition (in ring0)
\( \{ - I\}y \equiv \text{GroupInv}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I))(y) \)
Subtraction in the quotient space is defined by the \( + I \) and \( - I \) operations in the obvious way.
definition (in ring0)
\( x\{ - I\}y \equiv x\{ + I\}(\{ - I\}y) \)
The class of the zero of the ring with respect to the equivalence relation defined by an ideal \(I\) will be denoted \(0_I\).
definition (in ring0)
\( 0 _I \equiv \text{QuotientGroupRel}(R,A,I)\{ 0 \} \)
Similarly the class of the neutral element of multiplication in the ring with respect to the equivalence relation defined by an ideal \(I\) will be denoted \(1_I\).
definition (in ring0)
\( 1 _I \equiv \text{QuotientGroupRel}(R,A,I)\{1 \} \)
The class of the sum of two units of the ring will be denoted \(2_I\).
definition (in ring0)
\( 2 _I \equiv \text{QuotientGroupRel}(R,A,I)\{ 2 \} \)
The value of the projection of the ring multiplication onto the the quotient space defined by an ideal \(I\) on a pair of the same classes \(\langle x,x\rangle\) is denoted \(x^{2I}\).
definition (in ring0)
\( x^{2^I} \equiv \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle x,x\rangle \)
The class of the additive neutral element of the ring (i.e. \(0\)) with respect to the equivalence relation defined by an ideal is the neutral of the projected addition.
lemma (in ring0) neutral_quotient:
assumes \( I\triangleleft R \)
shows \( \text{QuotientGroupRel}(R,A,I)\{ 0 \} = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I)) \) using ringAssum, assms, Group_ZF_2_4_L5B, ideal_normal_add_subgroup, QuotientBy_def unfolding IsAring_defSimilarly, the class of the multiplicative neutral element of the ring (i.e. \(1\)) with respect to the equivalence relation defined by an ideal is the neutral of the projected multiplication.
lemma (in ring0) one_quotient:
assumes \( I\triangleleft R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( r\{1 \} = \text{ TheNeutralElement}( \text{QuotientBy}(I), \text{ProjFun2}(R,r,M)) \) using ringAssum, assms, Group_ZF_2_2_L1, ideal_equiv_rel, quotientBy_mul_monoid, QuotientBy_def unfolding IsAring_defThe class of \(2\) (i.e. \(1+1\)) is the same as the value of the addition projected on the quotient space on the pair of classes of \(1\).
lemma (in ring0) two_quotient:
assumes \( I\triangleleft R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( r\{ 2 \} = \text{QuotientGroupOp}(R,A,I)\langle r\{1 \},r\{1 \}\rangle \) using ringAssum, assms, EquivClass_1_L10, ideal_equiv_rel, Ring_ZF_1_L2(2), Ring_ZF_1_L2(2), Group_ZF_2_4_L5A, ideal_normal_add_subgroup unfolding IsAring_def, QuotientGroupOp_defThe class of a square of an element of the ring is the same as the result of the projected multiplication on the pair of classes of the element.
lemma (in ring0) sqrt_quotient:
assumes \( I\triangleleft R \), \( x\in R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( r\{x^2\} = \text{ProjFun2}(R,r, M)\langle r\{x\},r\{x\}\rangle \) using assms, EquivClass_1_L10, ideal_equiv_rel, quotientBy_mul_monoid(1)The projection of the ring addition is distributive with respect to the projection of the ring multiplication.
lemma (in ring0) quotientBy_distributive:
assumes \( I\triangleleft R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( \text{IsDistributive}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I), \text{ProjFun2}(R,r,M)) \) using ringAssum, assms, QuotientBy_def, ring_oper_distr(1), Ring_ZF_1_L4(1,3), quotientBy_mul_monoid(1), EquivClass_1_L10, ideal_equiv_rel, Group_ZF_2_4_L5A, ideal_normal_add_subgroup, ring_oper_distr(2) unfolding quotient_def, QuotientGroupOp_def, IsAring_def, IsDistributive_defThe quotient group is a ring with the quotient multiplication.
theorem (in ring0) quotientBy_is_ring:
assumes \( I\triangleleft R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( \text{IsAring}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I), \text{ProjFun2}(R,r, M)) \) using assms, quotientBy_distributive, quotientBy_mul_monoid(2), quotientBy_add_group unfolding IsAring_defAn important property satisfied by many important rings is being Noetherian: every ideal is finitely generated.
definition (in ring0)
\( I\triangleleft R \Longrightarrow I \text{ is finitely generated } \equiv \exists S\in \text{FinPow}(R).\ I = \langle S\rangle _I \)
For Noetherian rings the arbitrary sum can be reduced to the sum of a finite subset of the initial set of ideals
theorem (in ring0) sum_ideals_noetherian:
assumes \( \forall I\in \mathcal{I} .\ (I\text{ is finitely generated }) \), \( \mathcal{J} \subseteq \mathcal{I} \)
shows \( \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ (\oplus _I\mathcal{J} ) = (\oplus _I\mathcal{T} ) \)proof from assms(2) have \( \bigcup \mathcal{J} \subseteq R \) using ideal_dest_subset
then have \( \langle \bigcup \mathcal{J} \rangle _I \triangleleft R \) using generated_ideal_is_ideal
with assms(2) have \( (\oplus _I\mathcal{J} ) \triangleleft R \) using sumArbitraryIdeals_def
with assms(1) have \( (\oplus _I\mathcal{J} ) \text{ is finitely generated } \) using ideal_dest_subset
with \( (\oplus _I\mathcal{J} )\triangleleft R \) obtain \( S \) where \( S\in \text{FinPow}(R) \), \( (\oplus _I\mathcal{J} ) = \langle S\rangle _I \) using isFinGen_def
let \( N = \lambda s\in S.\ \{J\in \text{FinPow}(\mathcal{J} ).\ s\in (\oplus _IJ)\} \)
from \( S\in \text{FinPow}(R) \) have \( Finite(S) \) unfolding FinPow_def
then have \( (\forall t\in S.\ N(t) \neq 0) \longrightarrow \)
\( (\exists f.\ f \in (\prod t\in S.\ N(t)) \wedge (\forall t\in S.\ f(t) \in N(t))) \) using eqpoll_iff, finite_choice, AxiomCardinalChoiceGen_def unfolding Finite_def
moreover {
}
ultimately obtain \( f \) where f: \( f \in (\prod t\in S.\ N(t)) \), \( \forall t\in S.\ f(t) \in N(t) \)
{
fix \( t \)
assume \( t\in S \)
then have \( N(t) = \{J\in \text{FinPow}(\mathcal{J} ).\ t\in (\oplus _IJ)\} \) using lamE
moreover
from \( S\in \text{FinPow}(R) \), \( (\oplus _I\mathcal{J} ) = \langle S\rangle _I \), \( t\in S \) have \( t\in (\oplus _I\mathcal{J} ) \) using generated_ideal_contains_set unfolding FinPow_def
with assms(2) have \( \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ t\in (\oplus _I\mathcal{T} ) \) using sum_ideals_finite_sum
ultimately have \( N(t)\neq 0 \) using assms(2), sum_ideals_finite_sum
fix \( y \)
assume \( y \in f(S) \)
with image_iff obtain \( x \) where \( x\in S \) and \( \langle x,y\rangle \in f \)
with f(1) have \( y\in N(x) \) unfolding Pi_def
with \( x\in S \) have \( Finite(y) \) using lamE unfolding FinPow_def
moreover
{
from f(1) have f_Fun: \( f:S\rightarrow (\bigcup \{N(t).\ t\in S\}) \) unfolding Pi_def, Sigma_def
with \( Finite(S) \) have \( Finite(f(S)) \) using Finite1_L6A, Finite_Fin_iff, Fin_into_Finite
ultimately have \( Finite(\bigcup (f(S))) \) using Finite_Union
with f_Fun, f(2) have B: \( (\bigcup (f(S))) \in \text{FinPow}(\mathcal{J} ) \) using func_imagedef, lamE unfolding FinPow_def
then have \( (\bigcup (f(S))) \subseteq \mathcal{J} \) unfolding FinPow_def
with assms(2) have \( (\bigcup (f(S))) \subseteq \mathcal{I} \)
hence sub: \( \bigcup (\bigcup (f(S))) \subseteq R \)
fix \( t \)
assume \( t\in S \)
with f(2) have \( f(t) \in \text{FinPow}(\mathcal{J} ) \), \( t \in (\oplus _I(f(t))) \) using lamE
from assms(2), \( f(t) \in \text{FinPow}(\mathcal{J} ) \) have \( f(t) \subseteq \mathcal{I} \) unfolding FinPow_def
from f_Fun, \( t\in S \) have \( \bigcup (ft) \subseteq \bigcup (\bigcup (fS)) \) using func_imagedef
with sub have \( \bigcup (f(t)) \subseteq \langle \bigcup (\bigcup (f(S)))\rangle _I \) using generated_ideal_contains_set
with sub have \( \langle \bigcup (ft)\rangle _I \subseteq \langle \bigcup (\bigcup (fS))\rangle _I \) using generated_ideal_is_ideal, generated_ideal_small
with \( f(t) \subseteq \mathcal{I} \), \( t \in (\oplus _I(f(t))) \), \( (\bigcup (f(S))) \subseteq \mathcal{I} \) have \( t \in (\oplus _I(\bigcup (f(S)))) \) using sumArbitraryIdeals_def
hence \( S \subseteq \oplus _I(\bigcup (f(S))) \)
with sub, \( (\bigcup (f(S))) \subseteq \mathcal{I} \), \( (\oplus _I\mathcal{J} ) = \langle S\rangle _I \) have \( (\oplus _I\mathcal{J} ) \subseteq \oplus _I(\bigcup (f(S))) \) using generated_ideal_small, generated_ideal_is_ideal, sumArbitraryIdeals_def
moreover
qed
from \( \bigcup \mathcal{J} \subseteq R \), \( (\bigcup (f(S))) \subseteq \mathcal{J} \) have \( \bigcup (\bigcup (f(S))) \subseteq \langle \bigcup \mathcal{J} \rangle _I \) using generated_ideal_contains_set
with assms(2), \( (\bigcup (f(S))) \subseteq \mathcal{I} \), \( \langle \bigcup \mathcal{J} \rangle _I \triangleleft R \) have \( (\oplus _I(\bigcup (f(S)))) \subseteq (\oplus _I\mathcal{J} ) \) using generated_ideal_small, sumArbitraryIdeals_def, sumArbitraryIdeals_def
ultimately have \( (\oplus _I\mathcal{J} ) = \oplus _I(\bigcup (f(S))) \)
with B show \( thesis \)
end
lemma (in group0) group_self_subgroup: shows \( \text{IsAsubgroup}(G,P) \)
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 \)Definition of Ideal:
\( I \triangleleft R \equiv (\forall x\in I.\ \forall y\in R.\ y\cdot x\in I \wedge x\cdot y\in I) \wedge \text{IsAsubgroup}(I,A) \)
lemma (in ring0) Ring_ZF_1_L6:
assumes \( x\in R \)
shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \) corollary (in group0) unit_singl_subgr: shows \( \text{IsAsubgroup}(\{1 \},P) \)
lemma (in group0) group0_3_L2:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( H \subseteq G \) lemma (in group0) group0_3_L6:
assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)
shows \( a\cdot b \in H \) theorem (in group0) group0_3_T3A:
assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)
shows \( h^{-1}\in H \) lemma (in group0) group0_3_L5:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( 1 \in H \) 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 \) lemma (in group0) subgroup_inter:
assumes \( \ \lt H>\neq 0 \) and \( \forall H\in \ \lt H>.\ \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAsubgroup}(\bigcap \ \lt H>,P) \) theorem (in ring0) intersection_ideals:
assumes \( \forall J\in \mathcal{J} .\ (J \triangleleft R) \), \( \mathcal{J} \neq 0 \)
shows \( (\bigcap \mathcal{J} ) \triangleleft R \) lemma (in ring0) ring_self_ideal: shows \( R \triangleleft R \)
Definition of generatedIdeal:
\( X\subseteq R \Longrightarrow \langle X\rangle _I \equiv \bigcap \{I\in \mathcal{I} .\ X \subseteq I\} \)
lemma (in ring0) ideal_dest_subset:
assumes \( I \triangleleft R \)
shows \( I \subseteq R \) corollary (in ring0) generated_ideal_contains_set:
assumes \( X\subseteq R \)
shows \( X\subseteq \langle X\rangle _I \) corollary (in ring0) generated_ideal_is_ideal:
assumes \( X\subseteq R \)
shows \( \langle X\rangle _I \triangleleft R \) lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
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 \) lemma (in ring0) ideal_dest_sum:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in I \)
shows \( x + y \in I \)Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
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 \) 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 \) lemma (in ring0) Ring_ZF_1_L7:
assumes \( a\in R \), \( b\in R \)
shows \( ( - a)\cdot b = - (a\cdot b) \), \( a\cdot ( - b) = - (a\cdot b) \), \( ( - a)\cdot b = a\cdot ( - b) \) lemma (in ring0) ideal_dest_minus:
assumes \( I \triangleleft R \), \( x\in I \)
shows \( ( - x) \in I \) theorem (in group0) group0_3_T3:
assumes \( H\neq 0 \) and \( H\subseteq G \) and \( H \text{ is closed under } P \) and \( \forall x\in H.\ x^{-1} \in H \)
shows \( \text{IsAsubgroup}(H,P) \) corollary (in ring0) generated_ideal_small:
assumes \( X\subseteq I \), \( I \triangleleft R \)
shows \( \langle X\rangle _I \subseteq I \) 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 \) 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 \) theorem (in ring0) ideal_with_one:
assumes \( I\triangleleft R \), \( 1 \in I \)
shows \( I = R \)Definition of sumIdeal:
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I+_IJ \equiv \langle I\cup J\rangle _I \)
Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
Definition of sumArbitraryIdeals:
\( \mathcal{J} \subseteq \mathcal{I} \Longrightarrow \oplus _I\mathcal{J} \equiv \langle \bigcup \mathcal{J} \rangle _I \)
lemma (in ring0) induction_generated_ideal:
assumes \( X\neq 0 \), \( X\subseteq R \), \( \forall y\in R.\ \forall z\in R.\ \forall q\in \langle X\rangle _I.\ P(q) \longrightarrow P(y\cdot q\cdot z) \), \( \forall y\in R.\ \forall z\in R.\ P(y) \wedge P(z) \longrightarrow P(y + z) \), \( \forall x\in X.\ P(x) \)
shows \( \forall y\in \langle X\rangle _I.\ P(y) \)Definition of IsAring:
\( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \)
\( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
Definition of productIdeal:
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I\cdot _IJ \equiv \langle M(I\times J)\rangle _I \)
corollary (in ring0) inter_two_ideals:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( (I\cap J) \triangleleft R \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma func1_1_L6:
assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) 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 group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in ring0) ideal_dest_zero:
assumes \( I \triangleleft R \)
shows \( 0 \in I \) lemma (in ring0) Ring_ZF_1_L10:
assumes \( a\in R \), \( b\in R \), \( c\in R \)
shows \( a + (b + c) = a + b + c \), \( a - (b + c) = a - b - c \), \( a - (b - c) = a - b + c \) lemma (in ring0) Ring_ZF_2_L5:
assumes \( a\in R \), \( b\in R \), \( c\in R \), \( d\in R \)
shows \( a - b - c - d = a - d - b - c \), \( a + b + c - d = a - d + b + c \), \( a + b - c - d = a - c + (b - d) \), \( a + b + c + d = a + c + (b + d) \) lemma (in ring0) Ring_ZF_1_L9:
assumes \( a\in R \), \( b\in R \)
shows \( ( - b) - a = ( - a) - b \), \( ( - (a + b)) = ( - a) - b \), \( ( - (a - b)) = (( - a) + b) \), \( a - ( - b) = a + b \) lemma (in ring0) sum_elements:
assumes \( I \triangleleft R \), \( J \triangleleft R \), \( x\in I \), \( y\in J \)
shows \( x + y \in I+_IJ \) 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 \) 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 \) lemma (in ring0) sum_elements_is_ideal:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (A(I\times J)) \triangleleft R \) corollary (in ring0) sum_ideals_is_sum_elements:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (A(I \times J)) = I+_IJ \)Definition of maximalIdeal:
\( I\triangleleft _mR \equiv I\triangleleft R \wedge I\neq R \wedge (\forall J\in \mathcal{I} .\ I\subseteq J \wedge J\neq R \longrightarrow I=J) \)
lemma (in ring0) comp_in_sum_ideals:
assumes \( I\triangleleft R \) and \( J\triangleleft R \)
shows \( I \subseteq I+_IJ \) and \( J \subseteq I+_IJ \) and \( I\cup J \subseteq I+_IJ \) corollary (in ring0) sum_ideals_is_ideal:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (I+_IJ) \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 \) 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) ideal_dest_mult:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in R \)
shows \( x\cdot y \in I \), \( y\cdot x \in I \) lemma (in monoid0) monoid_oper_fun: shows \( f:G\times G\rightarrow G \)
theorem (in ring0) product_in_intersection:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( I\cdot _IJ \subseteq I\cap J \) and \( (I\cdot _IJ)\triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \)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)) \)
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) zero_ideal: shows \( \{ 0 \} \triangleleft R \)
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) \) lemma (in ring0) Ring_ZF_1_L6:
assumes \( x\in R \)
shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \) 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_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
lemma (in ring0) Ring_ZF_1_L6:
assumes \( x\in R \)
shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \) lemma Group_ZF_2_4_L6:
assumes \( \text{IsAgroup}(G,P) \) and \( P \text{ is commutative on } G \) and \( \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \), \( \text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H)) \) lemma (in group0) Group_ZF_2_4_L3:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \) lemma (in ring0) ideal_normal_add_subgroup:
assumes \( I\triangleleft R \)
shows \( \text{IsAnormalSubgroup}(R,A,I) \) theorem Group_ZF_2_4_T1:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{IsAgroup}(G// \text{QuotientGroupRel}(G,P,H), \text{QuotientGroupOp}(G,P,H)) \) lemma Group_ZF_2_4_L6:
assumes \( \text{IsAgroup}(G,P) \) and \( P \text{ is commutative on } G \) and \( \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \), \( \text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H)) \)Definition of QuotientBy:
\( I\triangleleft R \Longrightarrow \text{QuotientBy}(I) \equiv R// \text{QuotientGroupRel}(R,A,I) \)
Definition of QuotientGroupRel:
\( \text{QuotientGroupRel}(G,P,H) \equiv \)
\( \{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\} \)
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 \) 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_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_L8:
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) 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 Congruent2:
\( \text{Congruent2}(r,f) \equiv \)
\( (\forall x_1 x_2 y_1 y_2.\ \langle x_1,x_2\rangle \in r \wedge \langle y_1,y_2\rangle \in r \longrightarrow \)
\( \langle f\langle x_1,y_1\rangle , f\langle x_2,y_2\rangle \rangle \in r) \)
theorem (in monoid0) Group_ZF_2_2_T1:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,f) \) and \( F = \text{ProjFun2}(G,r,f) \)
shows \( \text{IsAmonoid}(G//r,F) \) lemma Group_ZF_2_4_L5B:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( e = \text{ TheNeutralElement}(G,P) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) \) lemma Group_ZF_2_2_L1:
assumes \( \text{IsAmonoid}(G,f) \) and \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,f) \) and \( F = \text{ProjFun2}(G,r,f) \) and \( e = \text{ TheNeutralElement}(G,f) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r,F) \) 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 \} \) lemma Group_ZF_2_4_L5A:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{Congruent2}( \text{QuotientGroupRel}(G,P,H),P) \)Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
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 (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 \)Definition of IsDistributive:
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
lemma (in ring0) quotientBy_distributive:
assumes \( I\triangleleft R \)
defines \( r \equiv \text{QuotientGroupRel}(R,A,I) \)
shows \( \text{IsDistributive}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R,A,I), \text{ProjFun2}(R,r,M)) \) 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 (in ring0) quotientBy_add_group:
assumes \( I\triangleleft R \)
shows \( \text{IsAgroup}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I)) \) and \( \text{QuotientGroupOp}(R, A, I) \text{ is commutative on } \text{QuotientBy}(I) \)Definition of isFinGen:
\( I\triangleleft R \Longrightarrow I \text{ is finitely generated } \equiv \exists S\in \text{FinPow}(R).\ I = \langle S\rangle _I \)
theorem finite_choice:
assumes \( n\in nat \)
shows \( \text{ the axiom of } n \text{ choice holds } \)Definition of AxiomCardinalChoiceGen:
\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
lemma (in ring0) sum_ideals_finite_sum:
assumes \( \mathcal{J} \subseteq \mathcal{I} \), \( s\in (\oplus _I\mathcal{J} ) \)
shows \( \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ s\in (\oplus _I\mathcal{T} ) \) lemma Finite1_L6A:
assumes \( f:X\rightarrow Y \) and \( N \in Fin(X) \)
shows \( f(N) \in Fin(Y) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8