IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5

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{ringHomomor}(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{ringHomomor}(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\} \)

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 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{ringHomomor}(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 ringHomomor_def, Homomor_def

Since 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 ringHomomor_def

In 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_def

The 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_L14

the 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_fun

As 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 ringHomomor_def, IsMorphism_def

As 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, ringHomomor_def, IsMorphism_def

For \(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 ringHomomor_def

A 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 origin, target, homomorphism, assms, ringHomHom, image_inv unfolding IsAring_def

A 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 origin, target, homomorphism, ringHomHom(1), image_neutral unfolding IsAring_def

The 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_fun

The 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 ringHomHom(1), preimage_normal_subgroup, ideal_normal_add_subgroup unfolding IsAring_def

then have \( \text{IsAsubgroup}(f^{-1}(J),A) \) unfolding IsAnormalSubgroup_def

moreover {

fix \( x \) \( y \)

assume \( x \in f^{-1}(J) \), \( y\in R \)

from homomorphism have \( f:R\rightarrow S \) unfolding ringHomomor_def

with \( x \in f^{-1}(J) \) have \( x\in R \) and \( f(x) \in J \) using func1_1_L15 unfolding ringHomomor_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

} ultimately show \( (f^{-1}(J))\triangleleft R_o \) using Ideal_def

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, ringHomomor_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

}

hence \( \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

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 )

qed

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

}

hence \( \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

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 )

qed

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{ringHomomor}(f_I,R,A,M,R_I,A_I,M_I) \) using ringAssum, idealAssum, ideal_normal_add_subgroup, 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, ringHomomor_def

The 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_def

The 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 ringHomHom(1), image_subgroup, f_is_fun unfolding IsAring_def, Ideal_def

moreover {

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

}

hence \( \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

qed

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

}

hence \( 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

}

hence \( M(f^{-1}(J)\times f^{-1}(K))\subseteq f^{-1}(Q) \)

moreover

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

qed

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 {

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)

}

hence \( 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)

}

hence \( 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

hence \( 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

} ultimately show \( thesis \) unfolding primeIdeal_def

qed

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

}

hence \( \{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 {

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 {

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)

} ultimately have \( f^{-1}(f(y)) = y \)

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

qed

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

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 \)

qed

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

{

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 {

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

} ultimately show \( K\triangleleft _pR_t \) unfolding primeIdeal_def

} qed

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

have \( \{t\in Pow(R).\ ker\subseteq t \wedge (t\triangleleft _pR)\} = F\{J\in Pow(S).\ J\triangleleft _pR_t\} \)proof

{

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

ultimately show \( thesis \)

qed

end

Definition of ringHomomor: \( \text{ringHomomor}(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 Homomor: \( \text{Homomor}(f,G,P,H,F) \equiv f:G\rightarrow H \wedge \text{IsMorphism}(G,P,F,f) \)

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 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\} \)

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 \)

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 ringHomHom:

assumes \( \text{ringHomomor}(f,R,A,M,S,U,V) \)

shows \( \text{Homomor}(f,R,A,S,U) \) and \( \text{Homomor}(f,R,M,S,V) \)

lemma image_inv:

assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( g\in G \)

shows \( f( \text{GroupInv}(G,P)(g)) = \text{GroupInv}(H,F)(f(g)) \)

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 ringHomHom:

assumes \( \text{ringHomomor}(f,R,A,M,S,U,V) \)

shows \( \text{Homomor}(f,R,A,S,U) \) and \( \text{Homomor}(f,R,M,S,V) \)

lemma image_neutral:

assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \)

shows \( f(\text{ TheNeutralElement}(G,P)) = \text{ TheNeutralElement}(H,F) \)

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 \)

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\} \)

theorem preimage_normal_subgroup:

assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( \text{IsAnormalSubgroup}(H,F,K) \)

shows \( \text{IsAnormalSubgroup}(G,P,f^{-1}(K)) \)

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 \)

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 \)

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 (in group0) quotient_map:

assumes \( \text{IsAnormalSubgroup}(G,P,H) \)

defines \( r \equiv \text{QuotientGroupRel}(G,P,H) \) and \( q \equiv \lambda x\in G.\ \text{QuotientGroupRel}(G,P,H)\{x\} \)

shows \( \text{Homomor}(q,G,P,G//r, \text{QuotientGroupOp}(G,P,H)) \)

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{ringHomomor}(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 \)

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 \)

theorem image_subgroup:

assumes \( \text{IsAgroup}(G,P) \), \( \text{IsAgroup}(H,F) \), \( \text{Homomor}(f,G,P,H,F) \), \( f:G\rightarrow H \), \( \text{IsAsubgroup}(K,P) \)

shows \( \text{IsAsubgroup}(fK,F) \)

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 \)

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 \)

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)))) \)