theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_6
begin
This section studies the ideals of quotient rings, and defines ring homomorphisms.
Ring homomorphisms
Morphisms in general are structure preserving functions between algebraic structures. In this section we study ring homomorphisms.
A ring homomorphism is a function between rings which has the morphism property with respect to both addition and multiplication operation, and maps one (the neutral element of multiplication) in the first ring to one in the second ring.
definition
\( \text{IsRingHomomor}(f,R,A,M,S,U,V) \equiv f:R\rightarrow S \wedge \text{IsMorphism}(R,A,U,f) \wedge \text{IsMorphism}(R,M,V,f) \) \( \wedge f(\text{ TheNeutralElement}(R,M)) = \text{ TheNeutralElement}(S,V) \)
The next locale defines notation which we will use in this theory. We assume that we have two rings, one (which we will call the origin ring) defined by the triple \((R,A,M)\) and the second one (which we will call the target ring) by the triple \((S,U,V)\), and a homomorphism \(f:R\rightarrow S\).
locale ring_homo
assumes origin: \( \text{IsAring}(R,A,M) \) and target: \( \text{IsAring}(S,U,V) \) and homomorphism: \( \text{IsRingHomomor}(f,R,A,M,S,U,V) \)
defines \( x + _Ry \equiv A\langle x,y\rangle \)
defines \( ( - _Rx) \equiv \text{GroupInv}(R,A)(x) \)
defines \( x - _Ry \equiv x + _R( - _Ry) \)
defines \( x\cdot _Ry \equiv M\langle x,y\rangle \)
defines \( 0 _R \equiv \text{ TheNeutralElement}(R,A) \)
defines \( 1 _R \equiv \text{ TheNeutralElement}(R,M) \)
defines \( 2 _R \equiv 1 _R + _R1 _R \)
defines \( x^{2^R} \equiv x\cdot _Rx \)
defines \( x + _Sb \equiv U\langle x,b\rangle \)
defines \( ( - _Sx) \equiv \text{GroupInv}(S,U)(x) \)
defines \( x - _Sb \equiv x + _S( - _Sb) \)
defines \( x\cdot _Sb \equiv V\langle x,b\rangle \)
defines \( 0 _S \equiv \text{ TheNeutralElement}(S,U) \)
defines \( 1 _S \equiv \text{ TheNeutralElement}(S,V) \)
defines \( 2 _S \equiv 1 _S + _S1 _S \)
defines \( x^{2^S} \equiv x\cdot _Sx \)
defines \( \sum s \equiv \text{Fold}(A, 0 _R,s) \)
defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)
defines \( \prod s \equiv \text{Fold}(M,1 _R,s) \)
defines \( x^{n} \equiv \prod \{\langle k,x\rangle .\ k\in n\} \)
We will write \( I\triangleleft R_o \) to denote that \(I\) is an ideal of the ring \(R\). Note that in this notation the \( R_o \) part by itself has no meaning, only the whole \( \triangleleft R_o \) serves as postfix operator.
abbreviation (in ring_homo)
\( I\triangleleft R_o \equiv ring0.\ \text{Ideal}(R,A,M,I) \)
\( I\triangleleft R_t \) means that \(I\) is an ideal of \(S\).
abbreviation (in ring_homo)
\( I\triangleleft R_t \equiv ring0.\ \text{Ideal}(S,U,V,I) \)
\( I\triangleleft _pR_o \) means that \(I\) is a prime ideal of \(R\).
abbreviation (in ring_homo)
\( I\triangleleft _pR_o \equiv ring0.\ \text{primeIdeal}(R,A,M,I) \)
We will write \( I\triangleleft _pR_t \) to denote that \(I\) is a prime ideal of the ring \(S\).
abbreviation (in ring_homo)
\( I\triangleleft _pR_t \equiv ring0.\ \text{primeIdeal}(S,U,V,I) \)
ker denotes the kernel of \(f\) (which is assumed to be a homomorphism between \(R\) and \(S\).
abbreviation (in ring_homo)
\( ker \equiv f^{-1}\{ 0 _S\} \)
The theorems proven in the ring0 context are valid in the ring_homo context when applied to the ring \(R\).
sublocale ring_homo < origin_ring: ring0
using origin unfolding ring0_def
The group homomorphism locale applies to the additive part of a ring homomorphism: \((R,A)\) is the origin group and \((S,U)\) is the target group.
sublocale ring_homo < add_group_homo: group_homo
using origin, target, homomorphism unfolding IsAring_def, ringa_def, ringminus_def, ringzero_def, ringas_def, ringminuss_def, ringzeros_def, group_homo_def, IsRingHomomor_def, IsMorphism_def, Homomor_def
The theorems proven in the ring0 context are valid in the ring_homo context when applied to the ring \(S\).
sublocale ring_homo < target_ring: ring0
using target unfolding ring0_def
A ring homomorphism is a homomorphism both with respect to addition and multiplication.
lemma ringHomHom:
assumes \( \text{IsRingHomomor}(f,R,A,M,S,U,V) \)
shows \( \text{Homomor}(f,R,A,S,U) \) and \( \text{Homomor}(f,R,M,S,V) \) using assms unfolding IsRingHomomor_def, Homomor_defSince in the ring_homo locale \(f\) is a ring homomorphism it implies that \(f\) is a function from \(R\) to \(S\).
lemma (in ring_homo) f_is_fun:
shows \( f:R\rightarrow S \) using homomorphism unfolding IsRingHomomor_defIn the ring_homo context \(A\) is the addition in the first (source) ring \(M\) is the multiplication there and \(U,V\) are the addition and multiplication resp. in the second (target) ring. The next lemma states the all these are binary operations, a trivial, but frequently used fact.
lemma (in ring_homo) AMUV_are_ops:
shows \( A:R\times R\rightarrow R \), \( M:R\times R\rightarrow R \), \( U:S\times S\rightarrow S \), \( V:S\times S\rightarrow S \) using origin, target unfolding IsAring_def, IsAgroup_def, IsAmonoid_def, IsAssociative_defThe kernel is a subset of \(R\) on which the value of \(f\) is zero (of the target ring)
lemma (in ring_homo) kernel_def_alt:
shows \( ker = \{r\in R.\ f(r) = 0 _S\} \) using f_is_fun, func1_1_L14the homomorphism \(f\) maps each element of the kernel to zero of the target ring.
lemma (in ring_homo) image_kernel:
assumes \( x\in ker \)
shows \( f(x) = 0 _S \) using assms, func1_1_L15, f_is_funAs a ring homomorphism \(f\) preserves multiplication.
lemma (in ring_homo) homomor_dest_mult:
assumes \( x\in R \), \( y\in R \)
shows \( f(x\cdot _Ry) = (f(x))\cdot _S(f(y)) \) using assms, origin, target, homomorphism unfolding IsRingHomomor_def, IsMorphism_defAs a ring homomorphism \(f\) preserves addition.
lemma (in ring_homo) homomor_dest_add:
assumes \( x\in R \), \( y\in R \)
shows \( f(x + _Ry) = (f(x)) + _S(f(y)) \) using homomor_eq, origin, target, homomorphism, assms unfolding IsAring_def, IsRingHomomor_def, IsMorphism_defFor \(x\in R\) the value of \(f\) is in \(S\).
lemma (in ring_homo) homomor_val:
assumes \( x\in R \)
shows \( f(x) \in S \) using homomorphism, assms, apply_funtype unfolding IsRingHomomor_defA ring homomorphism preserves taking negative of an element.
lemma (in ring_homo) homomor_dest_minus:
assumes \( x\in R \)
shows \( f( - _Rx) = - _S(f(x)) \) using assms, add_group_homo.f_invA ring homomorphism preserves substraction.
lemma (in ring_homo) homomor_dest_subs:
assumes \( x\in R \), \( y\in R \)
shows \( f(x - _Ry) = (f(x)) - _S(f(y)) \) using assms, homomor_dest_add, homomor_dest_minus using Ring_ZF_1_L3(1)A ring homomorphism maps zero to zero.
lemma (in ring_homo) homomor_dest_zero:
shows \( f( 0 _R) = 0 _S \) using add_group_homo.f_neutralThe kernel of a homomorphism is never empty.
lemma (in ring_homo) kernel_non_empty:
shows \( 0 _R \in ker \) and \( ker\neq 0 \) using homomor_dest_zero, Ring_ZF_1_L2(1), func1_1_L15, f_is_funThe image of the kernel by \(f\) is the singleton \(\{ 0_R\}\).
corollary (in ring_homo) image_kernel_2:
shows \( f(ker) = \{ 0 _S\} \)proof have \( f:R\rightarrow S \), \( ker\subseteq R \), \( ker\neq 0 \), \( \forall x\in ker.\ f(x) = 0 _S \) using f_is_fun, kernel_def_alt, kernel_non_empty
then show \( f(ker) = \{ 0 _S\} \) using image_constant_singleton
qed
The inverse image of an ideal (in the target ring) is a normal subgroup of the addition group and an ideal in the origin ring. The kernel of the homomorphism is a subset of the inverse of image of every ideal.
lemma (in ring_homo) preimage_ideal:
assumes \( J\triangleleft R_t \)
shows \( \text{IsAnormalSubgroup}(R,A,f^{-1}(J)) \), \( (f^{-1}(J))\triangleleft R_o \), \( ker \subseteq f^{-1}(J) \)proof from origin, target, homomorphism, assms show \( \text{IsAnormalSubgroup}(R,A,f^{-1}(J)) \) using add_group_homo.preimage_normal_subgroup, ideal_normal_add_subgroup unfolding IsAring_def
then have \( \text{IsAsubgroup}(f^{-1}(J),A) \) unfolding IsAnormalSubgroup_def
moreover {
}
ultimately show \( (f^{-1}(J))\triangleleft R_o \) using Ideal_def
fix \( x \) \( y \)
assume \( x \in f^{-1}(J) \), \( y\in R \)
from homomorphism have \( f:R\rightarrow S \) unfolding IsRingHomomor_def
with \( x \in f^{-1}(J) \) have \( x\in R \) and \( f(x) \in J \) using func1_1_L15 unfolding IsRingHomomor_def
with assms, \( y\in R \), \( f:R\rightarrow S \) have \( V\langle f(x),f(y)\rangle \in J \) and \( V\langle f(y),f(x)\rangle \in J \) using apply_funtype, ideal_dest_mult
with \( x\in R \), \( y\in R \) have \( f(M\langle x,y\rangle ) \in J \) and \( f(M\langle y,x\rangle ) \in J \) using homomor_dest_mult
with \( x\in R \), \( y\in R \), \( f:R\rightarrow S \) have \( M\langle x,y\rangle \in f^{-1}(J) \) and \( M\langle y,x\rangle \in f^{-1}(J) \) using Ring_ZF_1_L4(3), func1_1_L15
from assms show \( ker \subseteq f^{-1}(J) \) using ideal_dest_zero
qed
Kernel of the homomorphism in an ideal.
lemma (in ring_homo) kernel_ideal:
shows \( ker \triangleleft R_o \) using zero_ideal, preimage_ideal(2)The inverse image of a prime ideal by a homomorphism is not the whole ring. Proof by contradiction.
lemma (in ring_homo) vimage_prime_ideal_not_all:
assumes \( J\triangleleft _pR_t \)
shows \( f^{-1}(J) \neq R \)proof{
}
assume \( R = f^{-1}(J) \)
then have \( R = \{x\in R.\ f(x)\in J\} \) using f_is_fun, func1_1_L15
then have \( 1 _R \in \{x\in R.\ f(x)\in J\} \) using Ring_ZF_1_L2(2)
with origin_ring.ringAssum, target_ring.ringAssum, homomorphism, assms have \( False \) using ideal_with_one unfolding primeIdeal_def, IsRingHomomor_def
thus \( f^{-1}(J) \neq R \)
qed
Even more, if the target ring of the homomorphism is commutative and the ideal is prime then its preimage is also. Note that this is not true in general.
lemma (in ring_homo) preimage_prime_ideal_comm:
assumes \( J\triangleleft _pR_t \), \( V \text{ is commutative on } S \)
shows \( (f^{-1}(J))\triangleleft _pR_o \)proof have \( \forall x\in R.\ \forall y\in R.\ (\forall z\in R.\ x\cdot _Rz\cdot _Ry \in f^{-1}(J)) \longrightarrow x\in f^{-1}(J) \vee y\in f^{-1}( J) \)proof
{
}
}
fix \( x \) \( y \)
assume \( x\in R \), \( y\in R \) and as: \( \forall z\in R.\ x\cdot _Rz\cdot _Ry \in f^{-1}(J) \) and \( y \notin f^{-1}(J) \)
{
fix \( s \)
assume \( s\in S \)
with assms(2), \( x\in R \), \( y\in R \) have \( (f(x))\cdot _Ss\cdot _S(f(y)) = s\cdot _S((f(x))\cdot _S(f(y))) \) using f_is_fun, apply_funtype, Ring_ZF_1_L11(2) unfolding IsCommutative_def
with \( x\in R \), \( y\in R \) have \( (fx)\cdot _Ss\cdot _S(fy) = s\cdot _S(f(x\cdot _Ry)) \) using homomor_dest_mult
with assms(1), \( s\in S \), \( x\in R \), as have \( (f(x))\cdot _Ss\cdot _S(f(y)) \in J \) using Ring_ZF_1_L2(2), Ring_ZF_1_L3(5), func1_1_L15, f_is_fun, ideal_dest_mult(2) unfolding primeIdeal_def
then have \( \forall z\in S.\ (fx) \cdot _S z \cdot _S (fy) \in J \)
with assms(1), \( x\in R \), \( y\in R \) have \( f(x)\in J \vee f(y)\in J \) using equivalent_prime_ideal, f_is_fun, apply_funtype
with \( x\in R \), \( y\in R \), \( y \notin f^{-1}(J) \) have \( x\in f^{-1}(J) \) using func1_1_L15, f_is_fun
thus \( thesis \)
qed
moreover
qed
from assms have \( (f^{-1}J)\triangleleft R_o \) using preimage_ideal unfolding primeIdeal_def
moreover from assms(1) have \( f^{-1}(J) \neq R \) using vimage_prime_ideal_not_all
ultimately show \( (f^{-1}(J))\triangleleft _pR_o \) by (rule equivalent_prime_ideal_2 )
We can replace the assumption that the target ring of the homomorphism is commutative with the assumption that homomorphism is surjective in preimage_prime_ideal_comm above and we can show the same assertion that the preimage of a prime ideal prime.
lemma (in ring_homo) preimage_prime_ideal_surj:
assumes \( J\triangleleft _pR_t \), \( f \in \text{surj}(R,S) \)
shows \( (f^{-1}(J))\triangleleft _pR_o \)proof have \( \forall x\in R.\ \forall y\in R.\ (\forall z\in R.\ x\cdot _Rz\cdot _Ry \in f^{-1}(J)) \longrightarrow x\in f^{-1}(J) \vee y\in f^{-1}(J) \)proof
{
}
}
fix \( x \) \( y \)
assume \( x\in R \), \( y\in R \) and as: \( \forall z\in R.\ x\cdot _Rz\cdot _Ry \in f^{-1}(J) \) and \( y \notin f^{-1}(J) \)
{
fix \( s \)
assume s: \( s\in S \)
with assms(2) obtain \( t \) where \( s=f(t) \), \( t\in R \) unfolding surj_def
with \( x\in R \), \( y\in R \), as have \( (fx)\cdot _Ss\cdot _S(fy)\in J \) using homomor_dest_mult, Ring_ZF_1_L4(3), func1_1_L15, f_is_fun
then have \( \forall z\in S.\ (f(x)) \cdot _S z \cdot _S (f(y)) \in J \)
with target_ring.equivalent_prime_ideal, assms(1), \( x\in R \), \( y\in R \) have \( f(x)\in J\vee f(y)\in J \) using f_is_fun, apply_funtype
with \( x\in R \), \( y\in R \), \( y \notin f^{-1}(J) \) have \( x\in f^{-1}(J) \) using func1_1_L15, f_is_fun
thus \( thesis \)
qed
moreover
qed
from assms have \( (f^{-1}(J))\triangleleft R_o \) using preimage_ideal unfolding primeIdeal_def
moreover from assms(1) have \( f^{-1}(J) \neq R \) using vimage_prime_ideal_not_all
ultimately show \( (f^{-1}(J))\triangleleft _pR_o \) by (rule equivalent_prime_ideal_2 )
Quotient ring with quotient map
The notion of a quotient ring (a.k.a factor ring, difference ring or residue class) is analogous to the notion of quotient group from the group theory.
The next locale ring2 extends the ring0 locale (defined in the Ring_ZF theory) with the assumption that some fixed set \(I\) is an ideal. It also defines some notation related to quotient rings, in particular we define the function (projection) \(f_I\) that maps each element \(r\) of the ring \(R\) to its class \(r_I(\{ r\}\) where \(r_I\) is the quotient group relation defined by \(I\) as a (normal) subgroup of \(R\) with addition.
locale ring2 = ring0 +
assumes idealAssum: \( I\triangleleft R \)
defines \( R_I \equiv \text{QuotientBy}(I) \)
defines \( r_I \equiv \text{QuotientGroupRel}(R,A,I) \)
defines \( f_I \equiv \lambda r\in R.\ r_I\{r\} \)
defines \( A_I \equiv \text{QuotientGroupOp}(R, A, I) \)
defines \( M_I \equiv \text{ProjFun2}(R, qrel, M) \)
The expression \( J\triangleleft R_I \) will mean that \(J\) is an ideal of the quotient ring \(R_I\) (with the quotient addition and multiplication).
abbreviation (in ring2)
\( J\triangleleft R_I \equiv ring0.\ \text{Ideal}(R_I,A_I,M_I,J) \)
In the ring2 The expression \( J\triangleleft _pR_I \) means that \(J\) is a prime ideal of the quotient ring \(R_I\).
abbreviation (in ring2)
\( J\triangleleft _pR_I \equiv ring0.\ \text{primeIdeal}(R_I,A_I,M_I,J) \)
Theorems proven in the ring0 context can be applied to the quotient ring in the ring2 context.
sublocale ring2 < quotient_ring: ring0
using quotientBy_is_ring, idealAssum, neutral_quotient, one_quotient, two_quotient unfolding ring0_def, ideal_radd_def, ideal_rmin_def, ideal_rsub_def, ideal_rmult_def, ideal_rzero_def, ideal_rone_def, ideal_rtwo_def, ideal_rsqr_def
The quotient map is a homomorphism of rings. This is probably one of the most sophisticated facts in IsarMathlib that Isabelle's simp method proves from 10 facts and 5 definitions.
theorem (in ring2) quotient_fun_homomor:
shows \( \text{IsRingHomomor}(f_I,R,A,M,R_I,A_I,M_I) \) using ringAssum, idealAssum, ideal_normal_add_subgroup, add_group.quotient_map, Ring_ZF_1_L4(3), EquivClass_1_L10, Ring_ZF_1_L2(2), Group_ZF_2_2_L1, ideal_equiv_rel, quotientBy_mul_monoid(1), QuotientBy_def unfolding IsAring_def, Homomor_def, IsMorphism_def, IsRingHomomor_defThe quotient map is surjective
lemma (in ring2) quot_fun:
shows \( f_I\in \text{surj}(R,R_I) \) using lam_funtype, idealAssum, QuotientBy_def unfolding quotient_def, surj_defThe theorems proven in the ring_homo context are valid in the ring_homo context when applied to the quotient ring as the second (target) ring and the quotient map as the ring homomorphism.
sublocale ring2 < quot_homomorphism: ring_homo
using ringAssum, quotient_ring.ringAssum, quotient_fun_homomor unfolding ring_homo_def
The ideal we divide by is the kernel of the quotient map.
lemma (in ring2) quotient_kernel:
shows \( quot\_homomorphism.\ kernel = I \)proof from idealAssum show \( quot\_homomorphism.\ kernel \subseteq I \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, neutral_quotient, QuotientBy_def, image_kernel, func1_1_L15 unfolding ideal_rzero_def, QuotientBy_def
{
fix \( t \)
assume \( t\in I \)
then have \( t\in R \) using ideal_dest_subset, idealAssum
with idealAssum, \( t\in I \) have \( t \in f_I^{-1}\{ 0 _I\} \) using Group_ZF_2_4_L5E, ideal_normal_add_subgroup, neutral_quotient, QuotientBy_def, func1_1_L15, surj_is_fun unfolding ideal_rzero_def
thus \( I \subseteq quot\_homomorphism.\ kernel \)
qed
If an ideal \(I\) is a subset of the kernel of the homomorphism then the image of the ideal generated by \(I\cup J\), where \(J\) is another ideal, is the same as the image of \(J\). Note that \( J+_II \) notation means the ideal generated by the union of ideals \(J\) and \(J\), see the definitions of sumIdeal and generatedIdeal in the Ring_ZF_2 theory, and also corollary sum_ideals_is_sum_elements for an alternative definition.
theorem (in ring_homo) kernel_empty_image:
assumes \( J\triangleleft R \), \( I \subseteq ker \), \( I\triangleleft R \)
shows \( f(J+_II) = f(J) \), \( f(I+_IJ) = f(J) \)proof from assms(1,3) have \( J+_II \subseteq R \) using sum_ideals_is_ideal, ideal_dest_subset
show \( f(J+_II) = f(J) \)proof
{
}
}
fix \( t \)
assume \( t\in f(J+_II) \)
with \( J+_II \subseteq R \) obtain \( q \) where q: \( q \in J+_II \), \( t=f(q) \) using func_imagedef, f_is_fun
with assms(1,3), \( q \in J+_II \) have \( q\in A(J\times I) \), \( J\times I \subseteq R\times R \) using sum_ideals_is_sum_elements, assms(1,3), ideal_dest_subset
from origin_ring.add_group.groupAssum, \( J\times I \subseteq R\times R \) have \( A(J\times I) = \{A(p).\ p\in J\times I\} \) unfolding IsAgroup_def, IsAmonoid_def, IsAssociative_def using func_imagedef
with \( q\in A(J\times I) \) obtain \( q_j \) \( q_i \) where \( q_j\in J \), \( q_i\in I \), \( q=q_j + _Rq_i \)
with assms have \( f(q) = (f(q_j)) + _S 0 _S \) using homomor_dest_add, ideal_dest_subset, image_kernel
moreover
from assms(1), \( q_j\in J \) have \( f(q_j) \in S \) using ideal_dest_subset, f_is_fun, apply_funtype
ultimately have \( f(q) = f(q_j) \) using Ring_ZF_1_L3(3)
with assms, \( t=f(q) \), \( q_j\in J \) have \( t \in f(J) \) using func_imagedef, f_is_fun, ideal_dest_subset
thus \( f(J+_II) \subseteq f(J) \)
{
fix \( t \)
assume \( t\in f(J) \)
with assms(1) obtain \( q \) where q: \( q\in J \), \( t=f(q) \) using func_imagedef, f_is_fun, ideal_dest_subset
from \( q\in J \) have \( q\in J\cup I \)
moreover
from assms(1,3) have \( J\cup I \subseteq R \) using ideal_dest_subset
ultimately have \( q\in \langle J\cup I\rangle _I \) using generated_ideal_contains_set
with assms(1,3), \( J+_II \subseteq R \), \( t=f(q) \) have \( t\in f(J+_II) \) using sumIdeal_def, f_is_fun, func_imagedef
thus \( f(J) \subseteq f(J+_II) \)
qed
with assms(1,3) show \( f (I+_IJ) = f(J) \) using sum_ideals_commute
qed
Quotient ideals
If we have an ideal \(J\) in a ring \(R\), and another ideal \(I\) contained in J, then we can form the quotient ideal J/I whose elements are of the form \(a + I\) where \(a\) is an element of \(J\).
The preimage of an ideal is an ideal, so it applies to the quotient map; but the preimage ideal contains the quotient ideal.
lemma (in ring2) ideal_quot_preimage:
assumes \( J\triangleleft R_I \)
shows \( (f_I^{-1}(J)) \triangleleft R \), \( I \subseteq f_I^{-1}(J) \)proof from assms, quot_homomorphism.preimage_ideal show \( (f_I^{-1}(J)) \triangleleft R \)
{
fix \( x \)
assume x: \( x\in I \)
with idealAssum have \( x\in R \) using ideal_dest_subset
from assms, \( x\in I \) have \( f_I(x) \in J \) using quotient_kernel, image_kernel, ideal_dest_zero
with \( x\in R \) have \( x\in f_I^{-1}(J) \) using f_is_fun, func1_1_L15
thus \( I \subseteq f_I^{-1}(J) \)
qed
Since the map is surjective, the image is also an ideal
lemma (in ring_homo) image_ideal_surj:
assumes \( J\triangleleft R_o \), \( f\in \text{surj}(R,S) \)
shows \( (f(J)) \triangleleft R_t \)proof from assms, homomorphism, target_ring.ringAssum, origin_ring.ringAssum have \( \text{IsAsubgroup}(f(J),U) \) using add_group_homo.image_is_subgroup, f_is_fun, ideal_dest_subset unfolding IsAring_def, Ideal_def
moreover {
}
qed
fix \( x \) \( y \)
assume \( x\in f(J) \), \( y\in S \)
from assms(1), \( x\in f(J) \) obtain \( j \) where \( x=f(j) \), \( j\in J \) using func_imagedef, f_is_fun, ideal_dest_subset
from assms, \( y\in S \), \( j\in J \) have \( j\in R \) and \( y\in f(R) \) using ideal_dest_subset, surj_range_image_domain
with assms(1) obtain \( s \) where \( y=f(s) \), \( s\in R \) using func_imagedef, ideal_dest_subset, f_is_fun
with assms(1), \( j\in R \), \( x=f(j) \), \( x\in f(J) \) have \( V\langle x,y\rangle = f(M\langle j,s\rangle ) \) and \( V\langle y,x\rangle = f(M\langle s,j\rangle ) \) using homomor_dest_mult, ideal_dest_subset
with assms(1), \( j\in J \), \( s\in R \) have \( (x\cdot _Sy)\in f(J) \) and \( (y\cdot _Sx)\in fJ \) using ideal_dest_mult, func_imagedef, f_is_fun, ideal_dest_subset
then have \( \forall x\in f(J).\ \forall y\in S.\ (y\cdot _Sx) \in f(J) \wedge (x\cdot _Sy) \in f(J) \)
ultimately show \( thesis \) unfolding Ideal_def
If the homomorphism is a surjection and given two ideals in the target ring the inverse image of their product ideal is the sum ideal of the product ideal of their inverse images and the kernel of the homomorphism.
corollary (in ring_homo) prime_ideal_quot:
assumes \( J\triangleleft R_t \), \( K\triangleleft R_t \), \( f\in \text{surj}(R,S) \)
shows \( f^{-1}(target\_ring.\ \text{productIdeal}(J, K)) = \) \( origin\_ring.\ \text{sumIdeal}(origin\_ring.\ \text{productIdeal}((f^{-1}(J)),(f^{-1}(K))), ker) \)proof let \( P = origin\_ring.\ \text{sumIdeal}(origin\_ring.\ \text{productIdeal}((f^{-1}(J)),(f^{-1}(K))), f^{-1}\{ 0 _S\}) \)
let \( Q = target\_ring.\ \text{productIdeal}(J, K) \)
from assms(1,2) have ideals: \( (f^{-1}(J)) \triangleleft R_o \), \( (f^{-1}(K)) \triangleleft R_o \) using preimage_ideal
then have idealJK: \( ((f^{-1}(J))\cdot _I(f^{-1}(K))) \triangleleft R_o \) using product_in_intersection(2)
then have \( P \triangleleft R_o \) and \( P\subseteq R \) using kernel_ideal, sum_ideals_is_ideal, ideal_dest_subset
with assms(3) have \( (f(P)) \triangleleft R_t \) using image_ideal_surj
let \( X = ((f^{-1}(J)) \cdot _I (f^{-1}(K)))\cup (f^{-1}\{ 0 _S\}) \)
from assms(3), idealJK have \( X \subseteq R \) using func1_1_L6A, surj_is_fun, ideal_dest_subset
with idealJK have \( X \subseteq P \) using kernel_ideal, sumIdeal_def, generated_ideal_contains_set
{
fix \( t \)
assume \( t\in V (J\times K) \)
moreover
from assms have \( J\times K \subseteq S\times S \) using ideal_dest_subset
ultimately obtain \( j \) \( k \) where \( j\in J \), \( k\in K \), \( t=V\langle j,k\rangle \) using func_imagedef, AMUV_are_ops(4)
from assms(1), \( j\in J \) have \( j\in S \) using ideal_dest_subset
with assms(3) obtain \( j_0 \) where \( j_0\in R \), \( f(j_0) = j \) unfolding surj_def
with assms(2,3), \( k\in K \) obtain \( k_0 \) where \( k_0\in R \), \( f(k_0) = k \) using ideal_dest_subset unfolding surj_def
with \( t=V\langle j,k\rangle \), \( f(j_0) = j \), \( j_0\in R \) have \( t=f(M\langle j_0,k_0\rangle ) \) using homomor_dest_mult
from assms(3) have \( (f^{-1}(J))\times (f^{-1}(K)) \subseteq R\times R \) using func1_1_L6A, f_is_fun
moreover
from assms(3), \( j_0\in R \), \( f(j_0) = j \), \( j\in J \), \( k\in K \), \( k_0\in R \), \( f(k_0) = k \) have \( \langle j_0,k_0\rangle \in (f^{-1}J)\times (f^{-1}K) \) using func1_1_L15 unfolding surj_def
ultimately have \( M\langle j_0,k_0\rangle \in M((f^{-1}(J))\times (f^{-1}(K))) \) using AMUV_are_ops, func_imagedef
with ideals, \( X \subseteq P \) have \( M\langle j_0,k_0\rangle \in P \) using product_in_intersection(3)
with \( P\subseteq R \), \( t=f(M\langle j_0,k_0\rangle ) \) have \( t\in (f(P)) \) using f_is_fun, func1_1_L15D
then have \( V(J \times K) \subseteq f(P) \)
with assms(1,2), \( (f(P)) \triangleleft R_t \) have \( Q\subseteq f(P) \) using generated_ideal_small, productIdeal_def
then have R: \( f^{-1}(Q) \subseteq f^{-1}(fP) \) unfolding vimage_def
from \( X \subseteq P \), \( P \triangleleft R_o \), \( P\subseteq R \) have P_ideal: \( P \in \{N\in \mathcal{I} .\ f^{-1}\{ 0 _S\} \subseteq N\} \)
{
fix \( t \)
assume \( t\in f^{-1}(f(P)) \)
then have \( f(t) \in f(P) \) and \( t\in R \) using func1_1_L15, f_is_fun
with P_ideal obtain \( s \) where \( f(t) = f(s) \), \( s\in P \) using func_imagedef, f_is_fun
from P_ideal, \( s\in P \) have \( s\in R \)
from \( t\in R \), \( s\in R \), \( f(t) = f(s) \) have \( f(t - _Rs) = 0 _S \) using f_is_fun, apply_funtype, Ring_ZF_1_L3(7), homomor_dest_subs
with \( t\in R \), \( s\in R \), \( X\subseteq P \) have \( t - _Rs \in P \) using Ring_ZF_1_L4(2), func1_1_L15, f_is_fun
with P_ideal, \( s\in P \) have \( s + _R(t - _Rs) \in P \) using ideal_dest_sum
with \( t\in R \), \( s\in R \) have \( t\in P \) using Ring_ZF_2_L1A(5)
with R show \( f^{-1}(Q) \subseteq P \)
{
fix \( t \)
assume as: \( t \in M((f^{-1}(J))\times (f^{-1}(K))) \)
have \( (f^{-1}(J))\times (f^{-1}(K)) \subseteq R\times R \) using func1_1_L15, f_is_fun
with as obtain \( t_j \) \( t_k \) where jk: \( t=t_j\cdot _Rt_k \), \( t_j\in f^{-1}(J) \), \( t_k\in f^{-1}(K) \) using AMUV_are_ops(2), func_imagedef, IsAssociative_def
from as have \( t\in R \) using AMUV_are_ops(2), func1_1_L6(2)
from jk(2,3) have \( t_j\in R \), \( f(t_j)\in J \) and \( t_k\in R \), \( f(t_k)\in K \) using func1_1_L15, f_is_fun
from jk(1), \( t_j\in R \), \( t_k\in R \) have ft: \( f(t) = ((f(t_j))\cdot _S(f(t_k))) \) using homomor_dest_mult
from \( f(t_j)\in J \), \( f(t_k) \in K \) have \( \langle f(t_j),f(t_k)\rangle \in J\times K \)
moreover
from assms have \( V:S\times S\rightarrow S \) and \( J\times K \subseteq S\times S \) using AMUV_are_ops(4), ideal_dest_subset
ultimately have \( V\langle f(t_j), f(t_k)\rangle \in V(J\times K) \) using func_imagedef
with assms, ft, \( t\in R \) have \( t \in f^{-1}(Q) \) using product_in_intersection(3), func1_1_L15, f_is_fun
then have \( M(f^{-1}(J)\times f^{-1}(K))\subseteq f^{-1}(Q) \)
moreover
qed
from assms(1,2) have id: \( (f^{-1}(Q)) \triangleleft R_o \) using preimage_ideal, product_in_intersection(2)
ultimately have \( (f ^{-1} J) \cdot _I (f ^{-1} K)\subseteq f^{-1}(Q) \) using ideals, generated_ideal_small, productIdeal_def
with assms(1,2) have \( X \subseteq f^{-1}(Q) \) using product_in_intersection(2), ideal_dest_zero
with idealJK, id show \( ((f^{-1}(J))\cdot _I(f^{-1}(K)))+_I(f^{-1}\{ 0 _S\}) \subseteq f^{-1}(Q) \) using generated_ideal_small, kernel_ideal, sumIdeal_def
If the homomorphism is surjective then the product ideal of ideals \(J,K\) in the target ring is the image of the product ideal (in the source ring) of the inverse images of \(J,K\).
corollary (in ring_homo) prime_ideal_quot_2:
assumes \( J\triangleleft R_t \), \( K\triangleleft R_t \), \( f\in \text{surj}(R,S) \)
shows \( target\_ring.\ \text{productIdeal}(J, K) = \) \( f(origin\_ring.\ \text{productIdeal}((f^{-1}(J)), (f^{-1}(K)))) \)proof from assms have \( f(f^{-1}(target\_ring.\ \text{productIdeal}(J, K)))\)
\( = f(((f^{-1}(J)) \cdot _I (f^{-1}(K))) +_I (ker)) \) using prime_ideal_quot
with assms show \( thesis \) using product_in_intersection(2), ideal_dest_subset, surj_image_vimage, product_in_intersection(2), preimage_ideal, kernel_empty_image(1), zero_ideal
qed
If the homomorphism is surjective and an ideal in the source ring contains the kernel, then the image of that ideal is a prime ideal in the target ring.
lemma (in ring_homo) preimage_ideal_prime:
assumes \( J\triangleleft _pR_o \), \( ker \subseteq J \), \( f\in \text{surj}(R,S) \)
shows \( (f(J))\triangleleft _pR_t \)proof from assms(1) have \( J \subseteq R \), \( J \neq R \) unfolding primeIdeal_def using ideal_dest_subset
from assms(1,3) have \( (f(J))\triangleleft R_t \) using image_ideal_surj unfolding primeIdeal_def
moreover {
}
}
ultimately show \( thesis \) unfolding primeIdeal_def
qed
assume \( f(J) = S \)
from \( J \subseteq R \), \( J \neq R \) obtain \( t \) where \( t\in R-J \)
with assms(3) have \( f(t)\in S \) using apply_funtype, f_is_fun
with assms(3), \( J \subseteq R \), \( f(J) = S \) obtain \( j \) where j: \( j\in J \), \( f(t)= f(j) \) using func_imagedef, f_is_fun
from \( j\in J \), \( J \subseteq R \) have \( j\in R \)
with assms(3), \( f(t)= f(j) \), \( t\in R-J \) have \( t - _Rj\in f^{-1}\{ 0 _S\} \) using apply_type, Ring_ZF_1_L3(7), f_is_fun, homomor_dest_subs, Ring_ZF_1_L4(2), func1_1_L15
with assms(1,2), j(1) have \( j + _R(t - _Rj) \in J \) unfolding primeIdeal_def using ideal_dest_sum
with \( j\in R \), \( t\in R-J \) have \( False \) using Ring_ZF_2_L1A(5)
then have \( f(J) \neq S \)
moreover {
fix \( I \) \( K \)
assume as: \( I\in target\_ring.\ ideals \), \( K\in target\_ring.\ ideals \), \( target\_ring.\ \text{productIdeal}(I, K) \subseteq f(J) \)
let \( A = (f^{-1}(I)) \cdot _I (f^{-1}(K)) \)
from as(1,2) have \( A \subseteq f^{-1}(f(A)) \) using product_in_intersection(2), preimage_ideal(2), ideal_dest_subset, func1_1_L9, f_is_fun
with assms(3), as have \( A \subseteq f^{-1}(f(J)) \) using prime_ideal_quot_2, vimage_mono
moreover
}
from assms(1) have \( J \subseteq f^{-1}(f(J)) \) using func1_1_L9, f_is_fun, ideal_dest_subset unfolding primeIdeal_def
moreover {
fix \( t \)
assume \( t \in f^{-1}(f(J)) \)
then have \( f(t)\in f(J) \), \( t\in R \) using func1_1_L15, f_is_fun
from assms(1), \( f(t)\in f(J) \) obtain \( s \) where \( f(t)=f(s) \), \( s\in J \) using func_imagedef, f_is_fun, ideal_dest_subset unfolding primeIdeal_def
from assms(1), \( s\in J \) have \( s\in R \) unfolding primeIdeal_def using ideal_dest_subset
with assms(2), \( f(t)=f(s) \), \( t\in R \) have \( t - _Rs \in J \) using Ring_ZF_1_L3(7), apply_funtype, f_is_fun, homomor_dest_subs, Ring_ZF_1_L4(2), func1_1_L15
with assms(1), \( s\in J \) have \( s + _R(t - _Rs)\in J \) using ideal_dest_sum unfolding primeIdeal_def
with \( s\in R \), \( t\in R \) have \( t\in J \) using Ring_ZF_2_L1A(5)
then have \( f^{-1}(fJ) \subseteq J \)
ultimately have \( A \subseteq J \)
with assms(1), as(1,2) have \( (f^{-1}(I)) \subseteq J \vee (f^{-1}(K)) \subseteq J \) using preimage_ideal, ideal_dest_subset unfolding primeIdeal_def
then have \( f(f^{-1}(I)) \subseteq fJ \vee f(f^{-1}(K)) \subseteq f(J) \)
with assms(3), as(1,2) have \( I \subseteq f(J) \vee K \subseteq f(J) \) using surj_image_vimage
The ideals of the quotient ring are in bijection with the ideals of the original ring that contain the ideal by which we made the quotient.
theorem (in ring_homo) ideal_quot_bijection:
assumes \( f\in \text{surj}(R,S) \)
defines \( idealFun \equiv \lambda J\in target\_ring.\ ideals.\ f^{-1}(J) \)
shows \( idealFun \in \text{bij}(target\_ring.\ ideals,\{K\in \mathcal{I} .\ ker \subseteq K\}) \)proof let \( \mathcal{I} _t = target\_ring.\ ideals \)
have \( idealFun : \mathcal{I} _t \rightarrow \{f^{-1}(J).\ J\in \mathcal{I} _t\} \) unfolding idealFun_def using lam_funtype
moreover {
}
{
fix \( t \)
assume \( t \in \{f^{-1}(J).\ J\in \mathcal{I} _t\} \)
then obtain \( K \) where \( K \in \mathcal{I} _t \), \( f^{-1}(K) = t \)
then have \( K\triangleleft R_t \)
then have \( (f^{-1}(K))\triangleleft R \), \( ker \subseteq f^{-1}(K) \) using preimage_ideal(2,3)
with \( f^{-1}(K) = t \) have \( ker \subseteq t \), \( t\triangleleft R \)
with \( f^{-1}(K) = t \) have \( t\in \{K\in \mathcal{I} .\ ker \subseteq K\} \) using func1_1_L3, f_is_fun
then have \( \{f^{-1}(J).\ J\in \mathcal{I} _t\} \subseteq \{K\in \mathcal{I} .\ ker \subseteq K\} \)
ultimately have I: \( idealFun : \mathcal{I} _t \rightarrow \{K\in \mathcal{I} .\ ker \subseteq K\} \) using func1_1_L1B
fix \( w \) \( x \)
assume as: \( w\triangleleft R_t \), \( x\triangleleft R_t \), \( w\subseteq S \), \( x\subseteq S \), \( idealFun(w) = idealFun(x) \)
then have \( f(f^{-1}(w)) = f(f^{-1}(x)) \) unfolding idealFun_def
with assms(1), as have \( w = x \) using surj_image_vimage
with I have \( idealFun \in \text{inj}(\mathcal{I} _t,\{K\in \mathcal{I} .\ ker \subseteq K\}) \) unfolding inj_def
moreover {
}
qed
fix \( y \)
assume \( y\triangleleft R \), \( y\subseteq R \), \( ker \subseteq y \)
from \( y\subseteq R \) have \( y \subseteq f^{-1}(fy) \) using func1_1_L9, f_is_fun
moreover {
}
ultimately have \( f^{-1}(f(y)) = y \)
fix \( t \)
assume \( t\in f^{-1}(f(y)) \)
then have \( f(t) \in f(y) \), \( t\in R \) using func1_1_L15, f_is_fun
from \( f(t) \in f(y) \), \( y\subseteq R \) obtain \( s \) where \( s\in y \), \( f(t) = f(s) \) using func_imagedef, f_is_fun
from \( s\in y \), \( y\subseteq R \) have \( s\in R \)
with \( t\in R \), \( f(t) = f(s) \), \( ker \subseteq y \) have \( t - _Rs \in y \) using Ring_ZF_1_L3(7), homomor_dest_subs, Ring_ZF_1_L4(2), func1_1_L15, f_is_fun
with \( s\in y \), \( y\triangleleft R \), \( s\in R \), \( t\in R \) have \( t\in y \) using ideal_dest_sum, Ring_ZF_2_L1A(5)
moreover
have \( f(y) \subseteq S \) using func1_1_L6(2), f_is_fun unfolding surj_def
moreover from assms(1), \( y\triangleleft R \) have \( (f(y))\triangleleft R_t \) using image_ideal_surj
ultimately have \( \exists x\in \mathcal{I} _t.\ idealFun(x) = y \) unfolding idealFun_def
with I have \( idealFun \in \text{surj}(\mathcal{I} _t,\{K\in \mathcal{I} .\ ker \subseteq K\}) \) unfolding surj_def
ultimately show \( thesis \) unfolding bij_def
Assume the homomorphism \(f\) is surjective and consider the function that maps an ideal \(J\) in the target ring to its inverse image \(f^{-1}(J)\) (in the source ring). Then the value of the converse of that function on any ideal containing the kernel of \(f\) is the image of that ideal under the homomorphism \(f\).
theorem (in ring_homo) quot_converse:
defines \( F \equiv \lambda J\in target\_ring.\ ideals.\ f^{-1}(J) \)
assumes \( J\triangleleft R \), \( ker\subseteq J \), \( f\in \text{surj}(R,S) \)
shows \( converse(F)(J) = f(J) \)proof let \( g = \lambda J\in \{K\in \mathcal{I} .\ ker\subseteq K\}.\ f(J) \)
let \( \mathcal{I} _t = target\_ring.\ ideals \)
let \( C_F = converse(F) \)
from assms(1,4) have \( C_F \in \text{bij}(\{K\in \mathcal{I} .\ ker\subseteq K\}, \mathcal{I} _t) \) using bij_converse_bij, ideal_quot_bijection
then have I: \( C_F:\{K\in \mathcal{I} .\ ker\subseteq K\} \rightarrow \mathcal{I} _t \) unfolding bij_def, inj_def
moreover
from assms(2,3) have J: \( J \in \{K\in \mathcal{I} .\ ker\subseteq K\} \) using ideal_dest_subset
ultimately have ideal: \( C_F(J) \in \mathcal{I} _t \) using apply_funtype
with assms(1,4), ideal have \( g(F(C_F(J))) = C_F(J) \) using preimage_ideal, ideal_dest_subset, surj_image_vimage
moreover
qed
from assms(1) have \( F: \mathcal{I} _t \rightarrow \{f^{-1}(J).\ J\in \mathcal{I} _t\} \) using lam_funtype
with I, J have \( F(C_F(J)) = J \) using right_inverse_lemma
ultimately have \( g(J) = C_F(J) \)
with J show \( thesis \)
Since the map is surjective, this bijection restricts to prime ideals on both sides.
corollary (in ring_homo) prime_ideal_quot_3:
assumes \( K\triangleleft R_t \), \( f \in \text{surj}(R,S) \)
shows \( K\triangleleft _pR_t \longleftrightarrow ((f^{-1}(K))\triangleleft _pR) \)proof{
}
{
}
qed
assume \( K\triangleleft _pR_t \)
with assms(2) show \( (f^{-1}(K))\triangleleft _pR \) using preimage_prime_ideal_surj, ideal_dest_subset unfolding primeIdeal_def
assume \( (f^{-1}(K))\triangleleft _pR \)
with assms(1,2) have \( K\triangleleft R_t \) and \( K\neq S \) using func1_1_L4 unfolding primeIdeal_def, surj_def
moreover {
}
ultimately show \( K\triangleleft _pR_t \) unfolding primeIdeal_def
fix \( J \) \( P \)
assume jp: \( J\in target\_ring.\ ideals \), \( P\in target\_ring.\ ideals \), \( target\_ring.\ \text{productIdeal}(J, P) \subseteq K \)
from jp(3) have \( f^{-1}(target\_ring.\ \text{productIdeal}(J, P)) \subseteq f^{-1}(K) \)
with assms(2), jp(1,2) have A: \( ((f^{-1}(J)) \cdot _I (f^{-1}(P))) +_I (ker) \subseteq f^{-1}(K) \) using prime_ideal_quot
from jp(1,2) have \( (f^{-1}(J))\cdot _I(f^{-1}(P)) \cup ker \subseteq ((f^{-1}(J))\cdot _I(f^{-1}(P))) +_I (ker) \) using preimage_ideal, product_in_intersection(2), kernel_ideal, comp_in_sum_ideals(3)
with A have \( ((f ^{-1} J) \cdot _I (f ^{-1} P)) \subseteq f^{-1}(K) \)
with \( (f^{-1}(K))\triangleleft _pR \), jp(1,2) have \( f^{-1}(J) \subseteq f^{-1}(K) \vee f^{-1}(P) \subseteq f^{-1}(K) \) using preimage_ideal, ideal_dest_subset unfolding primeIdeal_def
then have \( f(f^{-1}(J)) \subseteq f(f^{-1}(K)) \vee f(f^{-1}(P)) \subseteq f(f^{-1}(K)) \)
with assms, jp(1,2) have \( J \subseteq K \vee P \subseteq K \) using surj_image_vimage, ideal_dest_subset
If the homomorphism is surjective then the function that maps ideals in the target ring to their inverse images (in the source ring) is a bijection between prime ideals in the target ring and the prime ideals containing the kernel in the source ring.
corollary (in ring_homo) bij_prime_ideals:
defines \( F \equiv \lambda J\in target\_ring.\ ideals.\ f^{-1}(J) \)
assumes \( f \in \text{surj}(R,S) \)
shows \( \text{restrict}(F,\{J\in Pow(S).\ J\triangleleft _pR_t\}) \in \) \( \text{bij}(\{J\in Pow(S).\ J\triangleleft _pR_t\}, \{J\in Pow(R).\ ker\subseteq J \wedge (J\triangleleft _pR)\}) \)proof let \( \mathcal{I} _t = target\_ring.\ ideals \)
from assms have I: \( F:\mathcal{I} _t \rightarrow \{K\in \mathcal{I} .\ ker \subseteq K\} \) using ideal_quot_bijection, bij_is_fun
have II: \( \{J\in Pow(S).\ J\triangleleft _pR_t\} \subseteq \mathcal{I} _t \) unfolding primeIdeal_def
have III: \( \{J\in Pow(S).\ J\triangleleft _pR_t\} \subseteq \mathcal{I} _t \) unfolding primeIdeal_def
with assms have \( \text{restrict}(F,\{J\in Pow(S).\ J\triangleleft _pR_t\}) \in \)
\( \text{bij}(\{J\in Pow(S).\ J\triangleleft _pR_t\}, F\{J\in Pow(S).\ J\triangleleft _pR_t\}) \) using restrict_bij, ideal_quot_bijection unfolding bij_def
moreover
qed
have \( \{t\in Pow(R).\ ker\subseteq t \wedge (t\triangleleft _pR)\} = F\{J\in Pow(S).\ J\triangleleft _pR_t\} \)proof
ultimately show \( thesis \)
{
}
}
fix \( t \)
assume \( t \in F\{J\in Pow(S).\ J\triangleleft _pR_t\} \)
with I, III obtain \( q \) where \( q\in Pow(S) \), \( q\triangleleft _pR_t \), \( t=F(q) \) using func_imagedef
from \( q\in Pow(S) \), \( q\triangleleft _pR_t \) have \( q\in \mathcal{I} _t \) unfolding primeIdeal_def
with I have \( F(q) \in \{K\in \mathcal{I} .\ ker \subseteq K\} \) using apply_funtype
with assms, \( q\triangleleft _pR_t \), \( t=F(q) \), \( q\in \mathcal{I} _t \), \( t=F(q) \) have \( t\triangleleft R \), \( t\triangleleft _pR \), \( ker\subseteq t \) using prime_ideal_quot_3
then show \( F\{J\in Pow(S).\ J\triangleleft _pR_t\} \subseteq \{t\in Pow(R).\ ker\subseteq t \wedge (t\triangleleft _pR)\} \) using ideal_dest_subset
{
fix \( t \)
assume \( t\in \{t\in Pow(R).\ ker\subseteq t \wedge (t\triangleleft _pR)\} \)
then have \( t\in Pow(R) \), \( ker\subseteq t \), \( t\triangleleft _pR \)
then have tSet: \( t \in \{t\in \mathcal{I} .\ ker \subseteq t\} \) unfolding primeIdeal_def
with assms have cont: \( converse(F)(t) \in \mathcal{I} _t \) using ideal_quot_bijection, bij_converse_bij, apply_funtype, bij_is_fun
moreover
from assms, tSet have \( F(converse(F)(t)) = t \) using ideal_quot_bijection, right_inverse_bij
ultimately have \( f^{-1}(converse(F)(t)) = t \) using assms(1)
with assms, II, tSet, \( t\triangleleft _pR \), cont have \( t \in F\{J\in Pow(S).\ J\triangleleft _pR_t\} \) using prime_ideal_quot_3, ideal_dest_subset, bij_val_image_vimage, ideal_quot_bijection unfolding primeIdeal_def
thus \( \{t\in Pow(R).\ ker\subseteq t \wedge (t\triangleleft _pR)\} \subseteq F\{J\in Pow(S).\ J\triangleleft _pR_t\} \)
qed
Subrings
A subring of a ring \((R,A,M)\) is a subset \(S\) which forms a ring under the operations restricted from \((R,A,M)\).
We define \( \text{IsAsubring}(S,A,M) \) to mean that \(S\) is a subring of a ring with addition \(A\) and multiplication \(M\).
definition (in ring0)
\( S \subseteq R \Longrightarrow \text{IsAsubring}(S) \equiv \text{IsAring}(S, \text{restrict}(A,S\times S), \text{restrict}(M,S\times S)) \)
Every ring is a subring of itself.
lemma (in ring0) ring_self_subring:
shows \( \text{IsAsubring}(R) \)proof have restA: \( \text{restrict}(A,R\times R) = A \) using group_oper_fun, restrict_domain
have restM: \( \text{restrict}(M,R\times R) = M \) using monoid_oper_fun, restrict_domain
have \( R\subseteq R \Longrightarrow \text{IsAsubring}(R) \longleftrightarrow \text{IsAring}(R, \text{restrict}(A,R\times R), \text{restrict}(M,R\times R)) \) using IsAsubring_def
then show \( thesis \) using restA, restM, ringAssum
qed
The image of a ring under a ring homomorphism is a subring of the target ring.
lemma (in ring_homo) image_is_subring:
shows \( target\_ring.\ \text{IsAsubring}(f(R)) \)proof let \( T = f(R) \)
have R: \( T \subseteq S \Longrightarrow target\_ring.\ \text{IsAsubring}(T) \equiv \text{IsAring}(T, \text{restrict}(U,T\times T), \text{restrict}(V,T\times T)) \) using IsAsubring_def
have fR_sub_S: \( T \subseteq S \) using func1_1_L6(2), f_is_fun
have groupS: \( \text{IsAgroup}(S,U) \) using target, IsAring_def
have groupR: \( \text{IsAgroup}(R,A) \) using origin, IsAring_def
have T_add_group: \( \text{IsAsubgroup}(T,U) \) using ringHomHom(1), homomorphism, add_group_homo.image_is_group, R, groupS, groupR
have T_mul_closed: \( T \text{ is closed under } V \)proof
{
}
fix \( x \) \( y \)
assume xT: \( x\in T \) and yT: \( y\in T \)
from xT obtain \( g \) where aR: \( g\in R \) and xeq: \( x = f(g) \) using func_imagedef, f_is_fun
from yT obtain \( b \) where bR: \( b\in R \) and yeq: \( y = f(b) \) using func_imagedef, f_is_fun
have \( V\langle x,y\rangle = f(M\langle g,b\rangle ) \) using homomor_dest_mult, aR, bR, xeq, yeq
with aR, bR have \( V\langle x,y\rangle \in T \) using Ring_ZF_1_L4(3), func_imagedef, f_is_fun
then show \( thesis \) unfolding IsOpClosed_def
qed
have one_in_T: \( \text{ TheNeutralElement}(S,V) \in T \)proof
have oneR: \( 1 _R \in R \) using Ring_ZF_1_L2(2)
have hf: \( f(1 _R) \in T \) using func1_1_L15D, f_is_fun, oneR, subset_refl
have feq: \( f(1 _R) = \text{ TheNeutralElement}(S,V) \) using homomorphism unfolding IsRingHomomor_def
show \( thesis \) using hf, feq
qed
have T_add_closed: \( T \text{ is closed under } U \)proof
}
from T_add_group have rU_fun: \( \text{restrict}(U,T\times T):T\times T\rightarrow T \) unfolding IsAsubgroup_def, IsAgroup_def, IsAmonoid_def, IsAssociative_def
{
fix \( x \) \( y \)
assume xT: \( x\in T \) and yT: \( y\in T \)
from xT, yT, rU_fun have \( \text{restrict}(U,T\times T)\langle x,y\rangle \in T \) using apply_funtype
with xT, yT have \( U\langle x,y\rangle \in T \) using restrict_if
then show \( thesis \) unfolding IsOpClosed_def
qed
have T_mul_monoid: \( \text{IsAmonoid}(T, \text{restrict}(V,T\times T)) \) using group0_1_T1, T_mul_closed, fR_sub_S, one_in_T
have T_add_comm: \( \text{restrict}(U,T\times T) \text{ is commutative on } T \)proof
from target_ring.ringAssum have \( U \text{ is commutative on } S \) unfolding IsAring_def
with fR_sub_S, AMUV_are_ops(3) show \( thesis \) using func_ZF_4_L1
qed
have T_distrib: \( \text{IsDistributive}(T, \text{restrict}(U,T\times T), \text{restrict}(V,T\times T)) \)proof
from target_ring.ringAssum have \( \text{IsDistributive}(S,U,V) \) unfolding IsAring_def
with fR_sub_S, T_add_closed, T_mul_closed show \( thesis \) using func_ZF_7_L2
qed
from T_add_group, T_add_comm, T_mul_monoid, T_distrib show \( thesis \) using IsAsubring_def, fR_sub_S unfolding IsAring_def, IsAsubgroup_def
qed
The converse of a bijective ring homomorphism is also a ring homomorphism.
lemma (in ring_homo) bij_ring_homo_converse:
assumes bij: \( f \in \text{bij}(R,S) \)
shows \( \text{IsRingHomomor}(converse(f), S, U, V, R, A, M) \)proof have cf_fun: \( converse(f) : S \rightarrow R \) using bij_converse_bij, bij, bij_is_fun
have cf_add: \( \text{IsMorphism}(S, U, A, converse(f)) \)proof
have \( \text{IsAgroup}(R,A) \) using origin unfolding IsAring_def
with bij have \( \text{Homomor}(converse(f),S,U,R,A) \) using add_group_homo.bijective_hom_inverse
then show \( thesis \) unfolding Homomor_def
qed
have cf_mult: \( \text{IsMorphism}(S, V, M, converse(f)) \)proof
{
}
fix \( s_1 \) \( s_2 \)
assume s1: \( s_1 \in S \) and s2: \( s_2 \in S \)
from s1, bij obtain \( r_1 \) where r1: \( r_1 \in R \), \( f(r_1) = s_1 \) unfolding bij_def, surj_def
from s2, bij obtain \( r_2 \) where r2: \( r_2 \in R \), \( f(r_2) = s_2 \) unfolding bij_def, surj_def
have \( converse(f)(V\langle s_1,s_2\rangle ) = converse(f)(f(M\langle r_1,r_2\rangle )) \) using homomor_dest_mult, r1, r2
moreover
have \( M\langle r_1,r_2\rangle \in R \) using Ring_ZF_1_L4(3), r1(1), r2(1)
moreover have \( \bigwedge f A B x.\ f \in \text{inj}(A, B) \Longrightarrow x \in A \Longrightarrow converse(f) (fx) = x \) using left_inverse_eq
then have \( \bigwedge x.\ f\in \text{inj}(R,S) \Longrightarrow x\in R \Longrightarrow converse(f)(fx) = x \)
ultimately have step: \( converse(f)(V\langle s_1,s_2\rangle ) = M\langle r_1,r_2\rangle \) using bij, bij_is_inj
from bij have \( f:\text{inj}(R,S) \) using bij_is_inj
with r1, r2 have \( converse(f)(s_1) = r_1 \), \( converse(f)(s_2) = r_2 \) using left_inverse_eq
with step have \( converse(f)(V\langle s_1,s_2\rangle ) = M\langle converse(f)(s_1),converse(f)(s_2)\rangle \)
then show \( thesis \) unfolding IsMorphism_def
qed
have cf_one: \( converse(f)(\text{ TheNeutralElement}(S,V)) = \text{ TheNeutralElement}(R,M) \)proof
from homomorphism have one_eq: \( f(\text{ TheNeutralElement}(R,M)) = \text{ TheNeutralElement}(S,V) \) unfolding IsRingHomomor_def
have \( \bigwedge f A B x.\ f \in \text{inj}(A, B) \Longrightarrow x \in A \Longrightarrow converse(f) (fx) = x \) using left_inverse_eq
then have \( \bigwedge x.\ f\in \text{inj}(R,S) \Longrightarrow x\in R \Longrightarrow converse(f)(fx) = x \)
then have \( converse(f)(f(\text{ TheNeutralElement}(R,M))) = \text{ TheNeutralElement}(R,M) \) using left_inverse_eq, bij_is_inj, bij, Ring_ZF_1_L2(2)
with one_eq show \( thesis \)
qed
from cf_fun, cf_add, cf_mult, cf_one show \( thesis \) unfolding IsRingHomomor_def
qed
First isomorphism theorem
The first isomorphism theorem for rings: any ring homomorphism \(f: R \to S\) induces a ring isomorphism \(R/\ker(f) \cong f(R)\). The isomorphism sends each coset \([r]_{\ker(f)}\) to \(f(r)\).
If \(f: R \to S\) is a surjective ring homomorphism, then there exists a ring isomorphism \(\phi: R/\ker(f) \to S\).
theorem (in ring_homo) first_isomorphism_theorem:
assumes surj: \( f \in \text{surj}(R,S) \)
shows \( \exists \phi .\ \text{IsRingHomomor}(\phi , origin\_ring.\ \text{QuotientBy}(ker),\) \( \text{QuotientGroupOp}(R,A,ker),\) \( \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,ker),M),\) \( S, U, V) \wedge \phi \in \text{bij}(origin\_ring.\ \text{QuotientBy}(ker), S) \)proof let \( K = ker \)
let \( r = \text{QuotientGroupRel}(R,A,K) \)
let \( Q = origin\_ring.\ \text{QuotientBy}(K) \)
let \( A_Q = \text{QuotientGroupOp}(R,A,K) \)
let \( M_Q = \text{ProjFun2}(R,r,M) \)
let \( \phi = \{\langle r\{g\}, f(g)\rangle .\ g\in R\} \)
have K_ideal: \( K\triangleleft R_o \) using kernel_ideal
have equiv_r: \( \text{equiv}(R,r) \) using K_ideal, ideal_equiv_rel
have add_congr: \( \text{Congruent2}(r,A) \) using K_ideal, ideal_normal_add_subgroup, Group_ZF_2_4_L5A, origin_ring.ringAssum unfolding IsAring_def
have mul_congr: \( \text{Congruent2}(r,M) \) using K_ideal, quotientBy_mul_monoid(1)
have phi_fun: \( \phi : Q \rightarrow S \)proof
}
have qQ: \( \bigwedge g.\ g\in R \Longrightarrow r\{g\} \in Q \) using equiv_r, K_ideal, QuotientBy_def, quotientI
have I: \( \phi \in Pow(Q \times S) \) using qQ, homomor_val
have II: \( Q \subseteq domain(\phi ) \)proof
{
fix \( q \)
assume \( q \in Q \)
then obtain \( g \) where \( g\in R \), \( q = r\{g\} \) using K_ideal, QuotientBy_def unfolding quotient_def
then show \( q \in domain(\phi ) \) unfolding domain_def
qed
fix \( x \) \( y \) \( t \)
assume \( \langle x,y\rangle \in \phi \), \( \langle x,t\rangle \in \phi \)
then obtain \( g \) \( b \) where Hy: \( \langle x,y\rangle = \langle r\{g\},f(g)\rangle \) and aR: \( g\in R \) and Ht: \( \langle x,t\rangle = \langle r\{b\},f(b)\rangle \) and bR: \( b\in R \)
from Hy, Ht have rEq: \( r\{g\} = r\{b\} \) and yEq: \( y = f(g) \) and tEq: \( t = f(b) \)
from equiv_r, bR, rEq have ab_r: \( \langle g,b\rangle \in r \) using same_image_equiv
from ab_r have \( g - _Rb \in K \) unfolding QuotientGroupRel_def
then have \( f(g - _Rb) = 0 _S \) using func1_1_L15, f_is_fun, Ring_ZF_1_L4(2), aR, bR
with aR, bR have \( f(g) - _S(fb) = 0 _S \) using homomor_dest_subs
with homomor_val, aR, bR have \( f(g) = f(b) \) using Ring_ZF_1_L9A
then have \( y = t \) using yEq, tEq
then have III: \( \forall x y t.\ \langle x,y\rangle \in \phi \longrightarrow \langle x,t\rangle \in \phi \longrightarrow y = t \)
from I, II, III show \( thesis \) unfolding Pi_def, function_def
qed
have phi_val: \( \bigwedge g.\ g\in R \Longrightarrow \phi (r\{g\}) = f(g) \)proof
fix \( g \)
assume \( g\in R \)
then have \( \langle r\{g\}, f(g)\rangle \in \phi \)
with phi_fun show \( \phi (r\{g\}) = f(g) \) using apply_equality
qed
have phi_add: \( \text{IsMorphism}(Q,A_Q,U,\phi ) \)proof
{
}
fix \( x \) \( y \)
assume xQ: \( x\in Q \) and yQ: \( y\in Q \)
from xQ obtain \( g \) where aR: \( g\in R \) and xeq: \( x = r\{g\} \) using K_ideal, QuotientBy_def unfolding quotient_def
from yQ obtain \( b \) where bR: \( b\in R \) and yeq: \( y = r\{b\} \) using K_ideal, QuotientBy_def unfolding quotient_def
have \( A_Q\langle x,y\rangle = r\{A\langle g,b\rangle \} \) unfolding QuotientGroupOp_def using EquivClass_1_L10, equiv_r, add_congr, aR, bR, xeq, yeq
then have \( \phi (A_Q\langle x,y\rangle ) = f(A\langle g,b\rangle ) \) using phi_val, Ring_ZF_1_L4(1), aR, bR
also
have \( \ldots = U\langle f(g),f(b)\rangle \) using homomor_dest_add, aR, bR
also have \( \ldots = U\langle \phi (x),\phi (y)\rangle \) using aR, phi_val, bR, xeq, yeq
finally have \( \phi (A_Q\langle x,y\rangle ) = U\langle \phi (x),\phi (y)\rangle \)
then show \( thesis \) unfolding IsMorphism_def
qed
have phi_mult: \( \text{IsMorphism}(Q,M_Q,V,\phi ) \)proof
{
}
fix \( x \) \( y \)
assume xQ: \( x\in Q \) and yQ: \( y\in Q \)
from xQ obtain \( g \) where aR: \( g\in R \) and xeq: \( x = r\{g\} \) using K_ideal, QuotientBy_def unfolding quotient_def
from yQ obtain \( b \) where bR: \( b\in R \) and yeq: \( y = r\{b\} \) using K_ideal, QuotientBy_def unfolding quotient_def
have \( M_Q\langle x,y\rangle = r\{M\langle g,b\rangle \} \) using EquivClass_1_L10, equiv_r, mul_congr, aR, bR, xeq, yeq
then have \( \phi (M_Q\langle x,y\rangle ) = f(M\langle g,b\rangle ) \) using phi_val, Ring_ZF_1_L4(3), aR, bR
also
have \( \ldots = V\langle f(g),f(b)\rangle \) using homomor_dest_mult, aR, bR
also have \( \ldots = V\langle \phi (x),\phi (y)\rangle \) using phi_val, aR, bR, xeq, yeq
finally have \( \phi (M_Q\langle x,y\rangle ) = V\langle \phi (x),\phi (y)\rangle \)
then show \( \text{IsMorphism}(Q,M_Q,V,\phi ) \) unfolding IsMorphism_def
qed
have phi_one: \( \phi (\text{ TheNeutralElement}(Q,M_Q)) = \text{ TheNeutralElement}(S,V) \)proof
have \( \text{ TheNeutralElement}(Q,M_Q) = r\{1 _R\} \) using K_ideal, one_quotient
with origin_ring.Ring_ZF_1_L2(2) have \( \phi (\text{ TheNeutralElement}(Q,M_Q)) = f(1 _R) \) using phi_val
also
qed
have \( \ldots = \text{ TheNeutralElement}(S,V) \) using homomorphism unfolding IsRingHomomor_def
finally show \( thesis \)
have phi_inj: \( \phi \in \text{inj}(Q,S) \)proof
{
}
fix \( x \) \( y \)
assume xQ: \( x\in Q \) and yQ: \( y\in Q \) and eq: \( \phi (x) = \phi (y) \)
from xQ obtain \( g \) where aR: \( g\in R \) and xeq: \( x = r\{g\} \) using K_ideal, QuotientBy_def unfolding quotient_def
from yQ obtain \( b \) where bR: \( b\in R \) and yeq: \( y = r\{b\} \) using K_ideal, QuotientBy_def unfolding quotient_def
from eq, xeq, yeq, aR, bR have fab: \( f(g) = f(b) \) using phi_val
moreover
have \( fg\in S \) using homomor_val, aR
ultimately have \( f(g) - _S(fb) = 0 _S \) using Ring_ZF_1_L3(7)
with aR, bR have \( f(g - _Rb) = 0 _S \) using homomor_dest_subs
then have \( g - _Rb \in K \) using func1_1_L15, f_is_fun, Ring_ZF_1_L4(2), aR, bR
then have \( \langle g,b\rangle \in r \) using aR, bR unfolding QuotientGroupRel_def
then have \( x = y \) using xeq, yeq, equiv_class_eq, equiv_r
with phi_fun show \( thesis \) unfolding inj_def
qed
have phi_surj: \( \phi \in \text{surj}(Q,S) \)proof
{
}
fix \( s \)
assume \( s\in S \)
with surj obtain \( g \) where aR: \( g\in R \) and fs: \( f(g) = s \) unfolding surj_def
from quotientI have \( r\{g\} \in Q \) using equiv_r, aR, K_ideal, QuotientBy_def
with aR, fs, phi_val have \( \exists q\in Q.\ \phi (q) = s \)
with phi_fun show \( thesis \) unfolding surj_def
qed
from phi_inj, phi_surj, phi_fun have \( \phi \in \text{bij}(Q,S) \) unfolding bij_def
moreover
qed
have \( \text{IsRingHomomor}(\phi ,Q,A_Q,M_Q,S,U,V) \) using phi_fun, phi_add, phi_mult, phi_one unfolding IsRingHomomor_def, Homomor_def
ultimately show \( thesis \)
end
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 IsRingHomomor:
\( \text{IsRingHomomor}(f,R,A,M,S,U,V) \equiv f:R\rightarrow S \wedge \text{IsMorphism}(R,A,U,f) \wedge \text{IsMorphism}(R,M,V,f) \)
\( \wedge f(\text{ TheNeutralElement}(R,M)) = \text{ TheNeutralElement}(S,V) \)
Definition of IsMorphism:
\( \text{IsMorphism}(G,P,F,f) \equiv \forall g_1\in G.\ \forall g_2\in G.\ f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle \)
Definition of Homomor:
\( \text{Homomor}(f,G,P,H,F) \equiv f:G\rightarrow H \wedge \text{IsMorphism}(G,P,F,f) \)
Definition of IsAgroup:
\( \text{IsAgroup}(G,f) \equiv \)
\( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
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 ))) \)
lemma (in ring_homo) f_is_fun: shows \( f:R\rightarrow S \)
lemma func1_1_L14:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(\{y\}) = \{x\in X.\ f(x) = y\} \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma homomor_eq:
assumes \( \text{Homomor}(f,G,P,H,F) \), \( g_1\in G \), \( g_2\in G \)
shows \( f(P\langle g_1,g_2\rangle ) = F\langle f(g_1),f(g_2)\rangle \) lemma (in ring_homo) homomor_dest_add:
assumes \( x\in R \), \( y\in R \)
shows \( f(x + _Ry) = (f(x)) + _S(f(y)) \) lemma (in ring_homo) homomor_dest_minus:
assumes \( x\in R \)
shows \( f( - _Rx) = - _S(f(x)) \) 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 ring_homo) homomor_dest_zero: shows \( f( 0 _R) = 0 _S \)
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \), \( 2 \in R \)
lemma (in ring_homo) kernel_def_alt: shows \( ker = \{r\in R.\ f(r) = 0 _S\} \)
lemma (in ring_homo) kernel_non_empty: shows \( 0 _R \in ker \) and \( ker\neq 0 \)
lemma image_constant_singleton:
assumes \( f:X\rightarrow Y \), \( A\subseteq X \), \( A\neq \emptyset \), \( \forall x\in A.\ f(x) = c \)
shows \( f(A) = \{c\} \) lemma (in ring0) ideal_normal_add_subgroup:
assumes \( I\triangleleft R \)
shows \( \text{IsAnormalSubgroup}(R,A,I) \)Definition of IsAnormalSubgroup:
\( \text{IsAnormalSubgroup}(G,P,N) \equiv \text{IsAsubgroup}(N,P) \wedge \)
\( (\forall n\in N.\ \forall g\in G.\ P\langle P\langle g,n \rangle , \text{GroupInv}(G,P)(g) \rangle \in N) \)
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 ring_homo) homomor_dest_mult:
assumes \( x\in R \), \( y\in R \)
shows \( f(x\cdot _Ry) = (f(x))\cdot _S(f(y)) \) 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) ideal_dest_zero:
assumes \( I \triangleleft R \)
shows \( 0 \in I \) lemma (in ring0) zero_ideal: shows \( \{ 0 \} \triangleleft R \)
lemma (in ring_homo) preimage_ideal:
assumes \( J\triangleleft R_t \)
shows \( \text{IsAnormalSubgroup}(R,A,f^{-1}(J)) \), \( (f^{-1}(J))\triangleleft R_o \), \( ker \subseteq f^{-1}(J) \) lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \), \( 2 \in R \)
theorem (in ring0) ideal_with_one:
assumes \( I\triangleleft R \), \( 1 \in I \)
shows \( I = R \)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)) \)
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_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_mult:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in R \)
shows \( x\cdot y \in I \), \( y\cdot x \in 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 \) lemma (in ring_homo) preimage_ideal:
assumes \( J\triangleleft R_t \)
shows \( \text{IsAnormalSubgroup}(R,A,f^{-1}(J)) \), \( (f^{-1}(J))\triangleleft R_o \), \( ker \subseteq f^{-1}(J) \) lemma (in ring_homo) vimage_prime_ideal_not_all:
assumes \( J\triangleleft _pR_t \)
shows \( f^{-1}(J) \neq R \) 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 \) 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)) \) 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)) \) 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)) \) 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 \)Definition of ideal_radd:
\( x\{ + I\}y \equiv \text{QuotientGroupOp}(R, A, I)\langle x,y\rangle \)
Definition of ideal_rmin:
\( \{ - I\}y \equiv \text{GroupInv}( \text{QuotientBy}(I), \text{QuotientGroupOp}(R, A, I))(y) \)
Definition of ideal_rsub:
\( x\{ - I\}y \equiv x\{ + I\}(\{ - I\}y) \)
Definition of ideal_rmult:
\( x\{\cdot I\}y \equiv \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle x,y\rangle \)
Definition of ideal_rzero:
\( 0 _I \equiv \text{QuotientGroupRel}(R,A,I)\{ 0 \} \)
Definition of ideal_rone:
\( 1 _I \equiv \text{QuotientGroupRel}(R,A,I)\{1 \} \)
Definition of ideal_rtwo:
\( 2 _I \equiv \text{QuotientGroupRel}(R,A,I)\{ 2 \} \)
Definition of ideal_rsqr:
\( x^{2^I} \equiv \text{ProjFun2}(R, \text{QuotientGroupRel}(R,A,I), M)\langle x,x\rangle \)
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_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)) \)Definition of QuotientBy:
\( I\triangleleft R \Longrightarrow \text{QuotientBy}(I) \equiv R// \text{QuotientGroupRel}(R,A,I) \)
theorem (in ring2) quotient_fun_homomor: shows \( \text{IsRingHomomor}(f_I,R,A,M,R_I,A_I,M_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 ring_homo) image_kernel:
assumes \( x\in ker \)
shows \( f(x) = 0 _S \) lemma (in ring0) ideal_dest_subset:
assumes \( I \triangleleft R \)
shows \( I \subseteq R \) corollary (in ring0) sum_ideals_is_ideal:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (I+_IJ) \triangleleft R \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) corollary (in ring0) sum_ideals_is_sum_elements:
assumes \( I \triangleleft R \), \( J \triangleleft R \)
shows \( (A(I \times J)) = 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 \) corollary (in ring0) generated_ideal_contains_set:
assumes \( X\subseteq R \)
shows \( X\subseteq \langle X\rangle _I \)Definition of sumIdeal:
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I+_IJ \equiv \langle I\cup J\rangle _I \)
corollary (in ring0) sum_ideals_commute:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( (I +_I J) = (J +_I I) \) lemma (in ring2) quotient_kernel: shows \( quot\_homomorphism.\ kernel = I \)
lemma surj_range_image_domain:
assumes \( f \in \text{surj}(A,B) \)
shows \( f(A) = B \) 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 \) lemma (in ring_homo) kernel_ideal: shows \( ker \triangleleft R_o \)
lemma (in ring_homo) image_ideal_surj:
assumes \( J\triangleleft R_o \), \( f\in \text{surj}(R,S) \)
shows \( (f(J)) \triangleleft R_t \) lemma func1_1_L6A:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A)\subseteq X \) lemma (in ring_homo) AMUV_are_ops: shows \( A:R\times R\rightarrow R \), \( M:R\times R\rightarrow R \), \( U:S\times S\rightarrow S \), \( V:S\times S\rightarrow S \)
lemma (in ring_homo) AMUV_are_ops: shows \( A:R\times R\rightarrow R \), \( M:R\times R\rightarrow R \), \( U:S\times S\rightarrow S \), \( V:S\times S\rightarrow S \)
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 \) lemma func1_1_L15D:
assumes \( f:X\rightarrow Y \), \( x\in A \), \( A\subseteq X \)
shows \( f(x) \in f(A) \) corollary (in ring0) generated_ideal_small:
assumes \( X\subseteq I \), \( I \triangleleft R \)
shows \( \langle X\rangle _I \subseteq I \)Definition of productIdeal:
\( I\triangleleft R \Longrightarrow J\triangleleft R \Longrightarrow I\cdot _IJ \equiv \langle M(I\times J)\rangle _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 \) lemma (in ring_homo) homomor_dest_subs:
assumes \( x\in R \), \( y\in R \)
shows \( f(x - _Ry) = (f(x)) - _S(f(y)) \) 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) ideal_dest_sum:
assumes \( I \triangleleft R \), \( x\in I \), \( y\in I \)
shows \( x + y \in I \) lemma (in ring0) Ring_ZF_2_L1A:
assumes \( a\in R \), \( b\in R \)
shows \( a - b + b = a \), \( a + b - a = b \), \( ( - a) + b + a = b \), \( ( - a) + (b + a) = b \), \( a + (b - a) = b \) lemma (in ring_homo) AMUV_are_ops: shows \( A:R\times R\rightarrow R \), \( M:R\times R\rightarrow R \), \( U:S\times S\rightarrow S \), \( V:S\times S\rightarrow S \)
lemma func1_1_L6:
assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \) corollary (in ring_homo) prime_ideal_quot:
assumes \( J\triangleleft R_t \), \( K\triangleleft R_t \), \( f\in \text{surj}(R,S) \)
shows \( f^{-1}(target\_ring.\ \text{productIdeal}(J, K)) = \) \( origin\_ring.\ \text{sumIdeal}(origin\_ring.\ \text{productIdeal}((f^{-1}(J)),(f^{-1}(K))), ker) \) lemma surj_image_vimage:
assumes \( f \in \text{surj}(X,Y) \) and \( A\subseteq Y \)
shows \( f(f^{-1}(A)) = A \) theorem (in ring_homo) kernel_empty_image:
assumes \( J\triangleleft R \), \( I \subseteq ker \), \( I\triangleleft R \)
shows \( f(J+_II) = f(J) \), \( f(I+_IJ) = f(J) \) lemma func1_1_L9:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( A \subseteq f^{-1}(f(A)) \) corollary (in ring_homo) prime_ideal_quot_2:
assumes \( J\triangleleft R_t \), \( K\triangleleft R_t \), \( f\in \text{surj}(R,S) \)
shows \( target\_ring.\ \text{productIdeal}(J, K) = \) \( f(origin\_ring.\ \text{productIdeal}((f^{-1}(J)), (f^{-1}(K)))) \) lemma (in ring_homo) preimage_ideal:
assumes \( J\triangleleft R_t \)
shows \( \text{IsAnormalSubgroup}(R,A,f^{-1}(J)) \), \( (f^{-1}(J))\triangleleft R_o \), \( ker \subseteq f^{-1}(J) \) lemma func1_1_L3:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(D) \subseteq X \) lemma func1_1_L1B:
assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)
shows \( f:X\rightarrow Z \) theorem (in ring_homo) ideal_quot_bijection:
assumes \( f\in \text{surj}(R,S) \)
defines \( idealFun \equiv \lambda J\in target\_ring.\ ideals.\ f^{-1}(J) \)
shows \( idealFun \in \text{bij}(target\_ring.\ ideals,\{K\in \mathcal{I} .\ ker \subseteq K\}) \) lemma (in ring_homo) preimage_prime_ideal_surj:
assumes \( J\triangleleft _pR_t \), \( f \in \text{surj}(R,S) \)
shows \( (f^{-1}(J))\triangleleft _pR_o \) lemma func1_1_L4:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(Y) = X \) 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 ring_homo) prime_ideal_quot_3:
assumes \( K\triangleleft R_t \), \( f \in \text{surj}(R,S) \)
shows \( K\triangleleft _pR_t \longleftrightarrow ((f^{-1}(K))\triangleleft _pR) \) lemma bij_val_image_vimage:
assumes \( f \in \text{bij}(X,Y) \), \( A\subseteq X \), \( y\in Y \)
shows \( y\in f(A) \longleftrightarrow converse(f)(y) \in A \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma restrict_domain:
assumes \( f:X\rightarrow Y \)
shows \( \text{restrict}(f,X) = f \) lemma (in monoid0) monoid_oper_fun: shows \( f:G\times G\rightarrow G \)
Definition of IsAsubring:
\( S \subseteq R \Longrightarrow \text{IsAsubring}(S) \equiv \text{IsAring}(S, \text{restrict}(A,S\times S), \text{restrict}(M,S\times S)) \)
lemma ringHomHom:
assumes \( \text{IsRingHomomor}(f,R,A,M,S,U,V) \)
shows \( \text{Homomor}(f,R,A,S,U) \) and \( \text{Homomor}(f,R,M,S,V) \)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 \)
Definition of IsAsubgroup:
\( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H,\text{restrict}(P,H\times H)) \)
theorem (in monoid0) group0_1_T1:
assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \) lemma func_ZF_4_L1:
assumes \( f:X\times X\rightarrow Y \) and \( A\subseteq X \) and \( f \text{ is commutative on } X \)
shows \( \text{restrict}(f,A\times A) \text{ is commutative on } A \) lemma func_ZF_7_L2:
assumes \( \text{IsDistributive}(X,A,M) \) and \( Y\subseteq X \) and \( Y \text{ is closed under } A \), \( Y \text{ is closed under } M \) and \( A_r = \text{restrict}(A,Y\times Y) \), \( M_r = \text{restrict}(M,Y\times Y) \)
shows \( \text{IsDistributive}(Y,A_r,M_r) \) 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) \) lemma (in ring_homo) homomor_val:
assumes \( x\in R \)
shows \( f(x) \in S \) lemma same_image_equiv:
assumes \( \text{equiv}(A,r) \), \( y\in A \), \( r\{x\} = r\{y\} \)
shows \( \langle x,y\rangle \in r \)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_L9A:
assumes \( a\in R \), \( b\in R \) and \( a - b = 0 \)
shows \( a=b \)Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),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 \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
