Theory Ring_ZF_3
section ‹Rings - Ideals of quotient rings›
theory Ring_ZF_3 imports Ring_ZF_2 Group_ZF_5
begin
text‹This section studies the ideals of quotient rings,
and defines ring homomorphisms.›
subsection‹Ring homomorphisms›
text‹Morphisms in general are structure preserving functions between algebraic
structures. In this section we study ring homomorphisms.›
text‹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
"ringHomomor(f,R,A,M,S,U,V) ≡ f:R→S ∧ IsMorphism(R,A,U,f) ∧ IsMorphism(R,M,V,f)
∧ f`(TheNeutralElement(R,M)) = TheNeutralElement(S,V)"
text‹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 =
fixes R A M S U V f
assumes origin: "IsAring(R,A,M)"
and target: "IsAring(S,U,V)"
and homomorphism: "ringHomomor(f,R,A,M,S,U,V)"
fixes ringa (infixl "\<ra>⇩R" 90)
defines ringa_def [simp]: "x\<ra>⇩Ry ≡ A`⟨x,y⟩"
fixes ringminus ("\<rm>⇩R _" 89)
defines ringminus_def [simp]: "(\<rm>⇩Rx) ≡ GroupInv(R,A)`(x)"
fixes ringsub (infixl "\<rs>⇩R" 90)
defines ringsub_def [simp]: "x\<rs>⇩Ry ≡ x\<ra>⇩R(\<rm>⇩Ry)"
fixes ringm (infixl "⋅⇩R" 95)
defines ringm_def [simp]: "x⋅⇩Ry ≡ M`⟨x,y⟩"
fixes ringzero ("𝟬⇩R")
defines ringzero_def [simp]: "𝟬⇩R ≡ TheNeutralElement(R,A)"
fixes ringone ("𝟭⇩R")
defines ringone_def [simp]: "𝟭⇩R ≡ TheNeutralElement(R,M)"
fixes ringtwo ("𝟮⇩R")
defines ringtwo_def [simp]: "𝟮⇩R ≡ 𝟭⇩R\<ra>⇩R𝟭⇩R"
fixes ringsq ("_⇧2⇧R" [96] 97)
defines ringsq_def [simp]: "x⇧2⇧R ≡ x⋅⇩Rx"
fixes ringas (infixl "\<ra>⇩S" 90)
defines ringas_def [simp]: "x\<ra>⇩Sb ≡ U`⟨x,b⟩"
fixes ringminuss ("\<rm>⇩S _" 89)
defines ringminuss_def [simp]: "(\<rm>⇩Sx) ≡ GroupInv(S,U)`(x)"
fixes ringsubs (infixl "\<rs>⇩S" 90)
defines ringsubs_def [simp]: "x\<rs>⇩Sb ≡ x\<ra>⇩S(\<rm>⇩Sb)"
fixes ringms (infixl "⋅⇩S" 95)
defines ringms_def [simp]: "x⋅⇩Sb ≡ V`⟨ x,b⟩"
fixes ringzeros ("𝟬⇩S")
defines ringzeros_def [simp]: "𝟬⇩S ≡ TheNeutralElement(S,U)"
fixes ringones ("𝟭⇩S")
defines ringones_def [simp]: "𝟭⇩S ≡ TheNeutralElement(S,V)"
fixes ringtwos ("𝟮⇩S")
defines ringtwos_def [simp]: "𝟮⇩S ≡ 𝟭⇩S\<ra>⇩S𝟭⇩S"
fixes ringsqs ("_⇧2⇧S" [96] 97)
defines ringsqs_def [simp]: "x⇧2⇧S ≡ x⋅⇩Sx"
text‹We will write ‹I◃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 ‹◃R⇩o› serves as postfix operator. ›
abbreviation (in ring_homo) ideal_origin ("_◃R⇩o")
where "I◃R⇩o ≡ ring0.Ideal(R,A,M,I)"
text‹‹I◃R⇩t› means that $I$ is an ideal of $S$.›
abbreviation (in ring_homo) ideal_target ("_◃R⇩t")
where "I◃R⇩t ≡ ring0.Ideal(S,U,V,I)"
text‹ ‹I◃⇩pR⇩o› means that $I$ is a prime ideal of $R$.›
abbreviation (in ring_homo) prime_ideal_origin ("_◃⇩pR⇩o")
where "I◃⇩pR⇩o ≡ ring0.primeIdeal(R,A,M,I)"
text‹We will write ‹I◃⇩pR⇩t› to denote that $I$ is a prime ideal of the ring $S$. ›
abbreviation (in ring_homo) prime_ideal_target ("_◃⇩pR⇩t")
where "I◃⇩pR⇩t ≡ ring0.primeIdeal(S,U,V,I)"
text‹ ‹ker› denotes the kernel of $f$ (which is assumed to be a homomorphism
between $R$ and $S$.›
abbreviation (in ring_homo) kernel ("ker" 90) where
"ker ≡ f-``{𝟬⇩S}"
text‹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 by auto
text‹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 S U V ringas ringminuss
ringsubs ringms ringzeros ringones ringtwos ringsqs
using target unfolding ring0_def by auto
text‹A ring homomorphism is a homomorphism both with respect to
addition and multiplication.›
lemma ringHomHom: assumes "ringHomomor(f,R,A,M,S,U,V)"
shows "Homomor(f,R,A,S,U)" and "Homomor(f,R,M,S,V)"
using assms unfolding ringHomomor_def Homomor_def
by simp_all
text‹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→S"
using homomorphism unfolding ringHomomor_def by simp
text‹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×R→R" "M:R×R→R" "U:S×S→S" "V:S×S→S"
using origin target
unfolding IsAring_def IsAgroup_def IsAmonoid_def IsAssociative_def
by auto
text‹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∈R. f`(r) = 𝟬⇩S}"
using f_is_fun func1_1_L14 by simp
text‹ the homomorphism $f$ maps each element of the kernel
to zero of the target ring. ›
lemma (in ring_homo) image_kernel:
assumes "x∈ker"
shows "f`(x) = 𝟬⇩S"
using assms func1_1_L15 f_is_fun by simp
text‹ As a ring homomorphism $f$ preserves multiplication.›
lemma (in ring_homo) homomor_dest_mult:
assumes "x∈R" "y∈R"
shows "f`(x⋅⇩Ry) = (f`(x))⋅⇩S(f`(y))"
using assms origin target homomorphism
unfolding ringHomomor_def IsMorphism_def by simp
text‹ As a ring homomorphism $f$ preserves addition. ›
lemma (in ring_homo) homomor_dest_add:
assumes "x∈R" "y∈R"
shows "f`(x\<ra>⇩Ry) = (f`(x))\<ra>⇩S(f`(y))"
using homomor_eq origin target homomorphism assms
unfolding IsAring_def ringHomomor_def IsMorphism_def
by simp
text‹For $x\in R$ the value of $f$ is in $S$.›
lemma (in ring_homo) homomor_val: assumes "x∈R"
shows "f`(x) ∈ S"
using homomorphism assms apply_funtype unfolding ringHomomor_def
by blast
text‹A ring homomorphism preserves taking negative of an element.›
lemma (in ring_homo) homomor_dest_minus:
assumes "x∈R"
shows "f`(\<rm>⇩Rx) = \<rm>⇩S(f`(x))"
using origin target homomorphism assms ringHomHom image_inv
unfolding IsAring_def by auto
text‹A ring homomorphism preserves substraction.›
lemma (in ring_homo) homomor_dest_subs:
assumes "x∈R" "y∈R"
shows "f`(x\<rs>⇩Ry) = (f`(x))\<rs>⇩S(f`(y))"
using assms homomor_dest_add homomor_dest_minus
using origin_ring.Ring_ZF_1_L3(1) by auto
text‹A ring homomorphism maps zero to zero.›
lemma (in ring_homo) homomor_dest_zero:
shows "f`(𝟬⇩R) = 𝟬⇩S"
using origin target homomorphism ringHomHom(1) image_neutral
unfolding IsAring_def by auto
text‹The kernel of a homomorphism is never empty.›
lemma (in ring_homo) kernel_non_empty:
shows "𝟬⇩R ∈ker" and "ker≠0"
using homomor_dest_zero origin_ring.Ring_ZF_1_L2(1)
func1_1_L15 f_is_fun by auto
text‹The image of the kernel by $f$ is the singleton $\{ 0_R\}$.›
corollary (in ring_homo) image_kernel_2: shows "f``(ker) = {𝟬⇩S}"
proof -
have "f:R→S" "ker⊆R" "ker≠0" "∀x∈ker. f`(x) = 𝟬⇩S"
using f_is_fun kernel_def_alt kernel_non_empty by auto
then show "f``(ker) = {𝟬⇩S}" using image_constant_singleton
by simp
qed
text‹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◃R⇩t"
shows
"IsAnormalSubgroup(R,A,f-``(J))"
"(f-``(J))◃R⇩o" "ker ⊆ f-``(J)"
proof -
from origin target homomorphism assms
show "IsAnormalSubgroup(R,A,f-``(J))"
using ringHomHom(1) preimage_normal_subgroup
target_ring.ideal_normal_add_subgroup
unfolding IsAring_def by blast
then have "IsAsubgroup(f-``(J),A)" unfolding IsAnormalSubgroup_def
by auto
moreover
{ fix x y assume "x ∈ f-``(J)" "y∈R"
from homomorphism have "f:R→S"
unfolding ringHomomor_def by simp
with ‹x ∈ f-``(J)› have "x∈R" and "f`(x) ∈ J"
using func1_1_L15 unfolding ringHomomor_def
by simp_all
with assms ‹y∈R› ‹f:R→S› have
"V`⟨f`(x),f`(y)⟩ ∈ J" and "V`⟨f`(y),f`(x)⟩∈J"
using apply_funtype target_ring.ideal_dest_mult by simp_all
with ‹x∈R› ‹y∈R› have "f`(M`⟨x,y⟩) ∈ J" and "f`(M`⟨y,x⟩) ∈ J"
using homomor_dest_mult by auto
with ‹x∈R› ‹y∈R› ‹f:R→S› have
"M`⟨x,y⟩ ∈ f-``(J)" and "M`⟨y,x⟩ ∈ f-``(J)"
using origin_ring.Ring_ZF_1_L4(3) func1_1_L15 by auto
}
ultimately show "(f-``(J))◃R⇩o" using origin_ring.Ideal_def
by auto
from assms show "ker ⊆ f-``(J)" using target_ring.ideal_dest_zero
by auto
qed
text‹Kernel of the homomorphism in an ideal.›
lemma (in ring_homo) kernel_ideal: shows "ker ◃R⇩o"
using target_ring.zero_ideal preimage_ideal(2) by simp
text‹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◃⇩pR⇩t" shows "f-``(J) ≠ R"
proof -
{ assume "R = f-``(J)"
then have "R = {x∈R. f`(x)∈J}" using f_is_fun func1_1_L15
by simp
then have "𝟭⇩R ∈ {x∈R. f`(x)∈J}" using origin_ring.Ring_ZF_1_L2(2)
by simp
with origin_ring.ringAssum target_ring.ringAssum homomorphism assms
have False using target_ring.ideal_with_one
unfolding target_ring.primeIdeal_def ringHomomor_def by auto
} thus "f-``(J) ≠ R" by blast
qed
text‹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◃⇩pR⇩t" "V {is commutative on} S"
shows "(f-``(J))◃⇩pR⇩o"
proof -
have "∀x∈R. ∀y∈R. (∀z∈R. x⋅⇩Rz⋅⇩Ry ∈ f-``(J)) ⟶ x∈f-``(J) ∨ y∈f-``( J)"
proof -
{ fix x y assume "x∈R" "y∈R" and as: "∀z∈R. x⋅⇩Rz⋅⇩Ry ∈ f-``(J)"
and "y ∉ f-``(J)"
{ fix s assume "s∈S"
with assms(2) ‹x∈R› ‹y∈R› have
"(f`(x))⋅⇩Ss⋅⇩S(f`(y)) = s⋅⇩S((f`(x))⋅⇩S(f`(y)))"
using f_is_fun apply_funtype target_ring.Ring_ZF_1_L11(2)
unfolding IsCommutative_def by auto
with ‹x∈R› ‹y∈R› have "(f`x)⋅⇩Ss⋅⇩S(f`y) = s⋅⇩S(f`(x⋅⇩Ry))"
using homomor_dest_mult by simp
with assms(1) ‹s∈S› ‹x∈R› as have "(f`(x))⋅⇩Ss⋅⇩S(f`(y)) ∈ J"
using origin_ring.Ring_ZF_1_L2(2) origin_ring.Ring_ZF_1_L3(5)
func1_1_L15 f_is_fun target_ring.ideal_dest_mult(2)
unfolding target_ring.primeIdeal_def by auto
} hence "∀z∈S. (f`x) ⋅⇩S z ⋅⇩S (f`y) ∈ J" by simp
with assms(1) ‹x∈R› ‹y∈R› have "f`(x)∈ J ∨ f`(y)∈J"
using target_ring.equivalent_prime_ideal f_is_fun apply_funtype
by simp
with ‹x∈R› ‹y∈R› ‹y ∉ f-``(J)› have "x∈f-``(J)"
using func1_1_L15 f_is_fun by simp
} thus ?thesis by blast
qed
moreover from assms have "(f-``J)◃R⇩o" using preimage_ideal
unfolding target_ring.primeIdeal_def by auto
moreover from assms(1) have "f-``(J) ≠ R" using vimage_prime_ideal_not_all
by simp
ultimately show "(f-``(J))◃⇩pR⇩o"
by (rule origin_ring.equivalent_prime_ideal_2)
qed
text‹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◃⇩pR⇩t" "f ∈ surj(R,S)"
shows "(f-``(J))◃⇩pR⇩o"
proof -
have "∀x∈R. ∀y∈R. (∀z∈R. x⋅⇩Rz⋅⇩Ry ∈ f-``(J)) ⟶ x∈f-``(J) ∨ y∈f-``(J)"
proof -
{ fix x y assume "x∈R" "y∈R" and as: "∀z∈R. x⋅⇩Rz⋅⇩Ry ∈ f-``(J)"
and "y ∉ f-``(J)"
{ fix s assume s: "s∈S"
with assms(2) obtain t where "s=f`(t)" "t∈R"
unfolding surj_def by auto
with ‹x∈R› ‹y∈R› as have "(f`x)⋅⇩Ss⋅⇩S(f`y)∈J"
using homomor_dest_mult origin_ring.Ring_ZF_1_L4(3)
func1_1_L15 f_is_fun by simp
} hence "∀z∈S. (f`(x)) ⋅⇩S z ⋅⇩S (f`(y)) ∈ J" by simp
with target_ring.equivalent_prime_ideal assms(1) ‹x∈R› ‹y∈R›
have "f`(x)∈J∨f`(y)∈J" using f_is_fun apply_funtype
by auto
with ‹x∈R› ‹y∈R› ‹y ∉ f-``(J)› have "x∈f-``(J)"
using func1_1_L15 f_is_fun by auto
} thus ?thesis by blast
qed
moreover from assms have "(f-``(J))◃R⇩o" using preimage_ideal
unfolding target_ring.primeIdeal_def by auto
moreover from assms(1) have "f-``(J) ≠ R" using vimage_prime_ideal_not_all
by simp
ultimately show "(f-``(J))◃⇩pR⇩o"
by (rule origin_ring.equivalent_prime_ideal_2)
qed
subsection‹Quotient ring with quotient map›
text‹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. ›
text‹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 +
fixes I
assumes idealAssum: "I◃R"
fixes quot ("R⇩I")
defines quot_def [simp]: "R⇩I ≡ QuotientBy(I)"
fixes qrel ("r⇩I")
defines qrel_def [simp]: "r⇩I ≡ QuotientGroupRel(R,A,I)"
fixes qfun ("f⇩I")
defines qfun_def [simp]: "f⇩I ≡ λr∈R. r⇩I``{r}"
fixes qadd ("A⇩I")
defines qadd_def [simp]: "A⇩I ≡ QuotientGroupOp(R, A, I)"
fixes qmul ("M⇩I")
defines qmul_def [simp]: "M⇩I ≡ ProjFun2(R, qrel, M)"
text‹The expression ‹J◃R⇩I› will mean that $J$ is an ideal of the quotient ring $R_I$
(with the quotient addition and multiplication).›
abbreviation (in ring2) qideal ("_◃R⇩I") where
"J◃R⇩I ≡ ring0.Ideal(R⇩I,A⇩I,M⇩I,J)"
text‹In the ‹ring2› The expression ‹J◃⇩pR⇩I› means that $J$ is a prime ideal of the quotient
ring $R_I$. ›
abbreviation (in ring2) qprimeIdeal ("_◃⇩pR⇩I") where
"J◃⇩pR⇩I ≡ ring0.primeIdeal(R⇩I,A⇩I,M⇩I,J)"
text‹Theorems proven in the ‹ring0› context can be applied
to the quotient ring in the ‹ring2› context. ›
sublocale ring2 < quotient_ring: ring0 quot qadd qmul
"λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)"
"λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)"
"𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧2⇧I)"
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 by auto
text‹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 "ringHomomor(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 ringHomomor_def
by simp
text‹The quotient map is surjective›
lemma (in ring2) quot_fun:
shows "f⇩I∈surj(R,R⇩I)"
using lam_funtype idealAssum QuotientBy_def
unfolding quotient_def surj_def by auto
text‹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 R A M quot qadd qmul qfun
_ _ _ _ _ _ _ _ "λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)"
"λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)"
"𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧2⇧I)"
using ringAssum quotient_ring.ringAssum quotient_fun_homomor
unfolding ring_homo_def by simp_all
text‹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 ⊆ I"
using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup
neutral_quotient QuotientBy_def
quot_homomorphism.image_kernel func1_1_L15
unfolding ideal_rzero_def QuotientBy_def by auto
{ fix t assume "t∈I"
then have "t∈R" using ideal_dest_subset idealAssum by auto
with idealAssum ‹t∈I› have "t ∈ f⇩I-``{𝟬⇩I}"
using add_group.Group_ZF_2_4_L5E ideal_normal_add_subgroup
neutral_quotient QuotientBy_def func1_1_L15 surj_is_fun
unfolding ideal_rzero_def by auto
} thus "I ⊆ quot_homomorphism.kernel" by blast
qed
text‹The theorems proven in the ‹ring0› context are valid in the
‹ring 2› context when applied to the quotient ring.›
sublocale ring2 < quotient_ring: ring0 quot qadd qmul
"λx y. ideal_radd(x,I,y)" "λy. ideal_rmin(I,y)"
"λx y. ideal_rsub(x,I,y)" "λx y. ideal_rmult(x,I,y)"
"𝟬⇩I" "𝟭⇩I" "𝟮⇩I" "λx. (x⇧2⇧I)"
using idealAssum quotientBy_is_ring neutral_quotient
one_quotient two_quotient
unfolding ring0_def by simp_all
text‹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◃R" "I ⊆ ker" "I◃R"
shows "f``(J+⇩II) = f``(J)" "f``(I+⇩IJ) = f``(J)"
proof-
from assms(1,3) have "J+⇩II ⊆ R"
using origin_ring.sum_ideals_is_ideal
origin_ring.ideal_dest_subset by auto
show "f``(J+⇩II) = f``(J)"
proof
{ fix t assume "t∈f``(J+⇩II)"
with ‹J+⇩II ⊆ R› obtain q where q: "q ∈ J+⇩II" "t=f`(q)"
using func_imagedef f_is_fun by auto
with assms(1,3) ‹q ∈ J+⇩II› have "q∈A``(J×I)" "J×I ⊆ R×R"
using origin_ring.sum_ideals_is_sum_elements
assms(1,3) origin_ring.ideal_dest_subset by auto
from origin_ring.add_group.groupAssum ‹J×I ⊆ R×R›
have "A``(J×I) = {A`(p). p∈J×I}"
unfolding IsAgroup_def IsAmonoid_def IsAssociative_def
using func_imagedef by auto
with ‹q∈A``(J×I)› obtain q⇩j q⇩i where "q⇩j∈J" "q⇩i∈I" "q=q⇩j\<ra>⇩Rq⇩i"
by auto
with assms have "f`(q) = (f`(q⇩j)) \<ra>⇩S 𝟬⇩S"
using homomor_dest_add origin_ring.ideal_dest_subset image_kernel
by blast
moreover from assms(1) ‹q⇩j∈J› have "f`(q⇩j) ∈ S"
using origin_ring.ideal_dest_subset f_is_fun apply_funtype by blast
ultimately have "f`(q) = f`(q⇩j)" using target_ring.Ring_ZF_1_L3(3)
by auto
with assms ‹t=f`(q)› ‹q⇩j∈J› have "t ∈ f``(J)"
using func_imagedef f_is_fun origin_ring.ideal_dest_subset by auto
} thus "f``(J+⇩II) ⊆ f``(J)" by blast
{ fix t assume "t∈f``(J)"
with assms(1) obtain q where q:"q∈J" "t=f`(q)"
using func_imagedef f_is_fun origin_ring.ideal_dest_subset
by auto
from ‹q∈J› have "q∈J∪I" by auto
moreover from assms(1,3) have "J∪I ⊆ R"
using origin_ring.ideal_dest_subset by auto
ultimately have "q∈⟨J∪I⟩⇩I" using origin_ring.generated_ideal_contains_set
by auto
with assms(1,3) ‹J+⇩II ⊆ R› ‹t=f`(q)› have "t∈f``(J+⇩II)"
using origin_ring.sumIdeal_def f_is_fun func_imagedef by auto
} thus "f``(J) ⊆ f``(J+⇩II)" by auto
qed
with assms(1,3) show "f ``(I+⇩IJ) = f``(J)"
using origin_ring.sum_ideals_commute by auto
qed
subsection‹Quotient ideals›
text‹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$.›
text‹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◃R⇩I"
shows "(f⇩I-``(J)) ◃R" "I ⊆ f⇩I-``(J)"
proof -
from assms quot_homomorphism.preimage_ideal show "(f⇩I-``(J)) ◃R"
by simp
{ fix x assume x: "x∈I"
with idealAssum have "x∈R" using ideal_dest_subset by auto
from assms ‹x∈I› have "f⇩I`(x) ∈ J"
using quotient_kernel quot_homomorphism.image_kernel
quotient_ring.ideal_dest_zero by simp
with ‹x∈R› have "x∈f⇩I-``(J)" using quot_homomorphism.f_is_fun func1_1_L15
by simp
} thus "I ⊆ f⇩I-``(J)" by auto
qed
text‹Since the map is surjective, the image is also an ideal›
lemma (in ring_homo) image_ideal_surj:
assumes "J◃R⇩o" "f∈surj(R,S)"
shows "(f``(J)) ◃R⇩t"
proof -
from assms homomorphism target_ring.ringAssum origin_ring.ringAssum
have "IsAsubgroup(f``(J),U)"
using ringHomHom(1) image_subgroup f_is_fun
unfolding IsAring_def origin_ring.Ideal_def by blast
moreover
{ fix x y assume "x∈f``(J)" "y∈S"
from assms(1) ‹x∈f``(J)› obtain j where "x=f`(j)" "j∈J"
using func_imagedef f_is_fun origin_ring.ideal_dest_subset
by auto
from assms ‹y∈S› ‹j∈J› have "j∈R" and "y∈f``(R)"
using origin_ring.ideal_dest_subset surj_range_image_domain
by auto
with assms(1) obtain s where "y=f`(s)" "s∈R"
using func_imagedef origin_ring.ideal_dest_subset f_is_fun
by auto
with assms(1) ‹j∈R› ‹x=f`(j)› ‹x∈f``(J)› have
"V`⟨x,y⟩ = f`(M`⟨j,s⟩)" and "V`⟨y,x⟩ = f`(M`⟨s,j⟩)"
using homomor_dest_mult origin_ring.ideal_dest_subset by auto
with assms(1) ‹j∈J› ‹s∈R› have "(x⋅⇩Sy)∈f``(J)" and "(y⋅⇩Sx)∈f``J"
using origin_ring.ideal_dest_mult func_imagedef f_is_fun
origin_ring.ideal_dest_subset by auto
} hence "∀x∈f``(J). ∀y∈S. (y⋅⇩Sx) ∈ f``(J) ∧ (x⋅⇩Sy) ∈ f``(J)"
by auto
ultimately show ?thesis unfolding target_ring.Ideal_def by simp
qed
text‹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◃R⇩t" "K◃R⇩t" "f∈surj(R,S)"
shows "f-``(target_ring.productIdeal(J, K)) =
origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), ker)"
proof
let ?P = "origin_ring.sumIdeal(origin_ring.productIdeal((f-``(J)),(f-``(K))), f-``{𝟬⇩S})"
let ?Q = "target_ring.productIdeal(J, K)"
from assms(1,2) have ideals: "(f-``(J)) ◃R⇩o" "(f-``(K)) ◃R⇩o"
using preimage_ideal by auto
then have idealJK: "((f-``(J))⋅⇩I(f-``(K))) ◃R⇩o"
using origin_ring.product_in_intersection(2) by auto
then have "?P ◃R⇩o" and "?P⊆R"
using kernel_ideal origin_ring.sum_ideals_is_ideal
origin_ring.ideal_dest_subset by simp_all
with assms(3) have "(f``(?P)) ◃R⇩t" using image_ideal_surj
by simp
let ?X = "((f-``(J)) ⋅⇩I (f-``(K)))∪(f-``{𝟬⇩S})"
from assms(3) idealJK have "?X ⊆ R"
using func1_1_L6A surj_is_fun origin_ring.ideal_dest_subset
by blast
with idealJK have "?X ⊆ ?P"
using kernel_ideal origin_ring.sumIdeal_def
origin_ring.generated_ideal_contains_set by simp
{ fix t assume "t∈V ``(J×K)"
moreover from assms have "J×K ⊆ S×S"
using target_ring.ideal_dest_subset by blast
ultimately obtain j k where "j∈J" "k∈K" "t=V`⟨j,k⟩"
using func_imagedef AMUV_are_ops(4) by auto
from assms(1) ‹j∈J› have "j∈S"
using target_ring.ideal_dest_subset by blast
with assms(3) obtain j⇩0 where "j⇩0∈R" "f`(j⇩0) = j"
unfolding surj_def by auto
with assms(2,3) ‹k∈K› obtain k⇩0 where "k⇩0∈R" "f`(k⇩0) = k"
using target_ring.ideal_dest_subset unfolding surj_def
by blast
with ‹t=V`⟨j,k⟩› ‹f`(j⇩0) = j› ‹j⇩0∈R› have "t=f`(M`⟨j⇩0,k⇩0⟩)"
using homomor_dest_mult by simp
from assms(3) have "(f-``(J))×(f-``(K)) ⊆ R×R"
using func1_1_L6A f_is_fun by blast
moreover from assms(3) ‹j⇩0∈R› ‹f`(j⇩0) = j› ‹j∈J› ‹k∈K› ‹k⇩0∈R› ‹f`(k⇩0) = k›
have "⟨j⇩0,k⇩0⟩ ∈ (f-``J)×(f-``K)"
using func1_1_L15 unfolding surj_def by auto
ultimately have "M`⟨j⇩0,k⇩0⟩ ∈ M``((f-``(J))×(f-``(K)))"
using AMUV_are_ops func_imagedef by auto
with ideals ‹?X ⊆ ?P› have "M`⟨j⇩0,k⇩0⟩ ∈ ?P"
using origin_ring.product_in_intersection(3)
by blast
with ‹?P⊆R› ‹t=f`(M`⟨j⇩0,k⇩0⟩)› have "t∈(f``(?P))"
using f_is_fun func1_1_L15D by simp
} hence "V``(J × K) ⊆ f``(?P)" by blast
with assms(1,2) ‹(f``(?P)) ◃R⇩t› have "?Q⊆f``(?P)"
using target_ring.generated_ideal_small target_ring.productIdeal_def
by simp
then have R: "f-``(?Q) ⊆ f-``(f``?P)"
unfolding vimage_def by blast
from ‹?X ⊆ ?P› ‹?P ◃R⇩o› ‹?P⊆R› have P_ideal: "?P ∈ {N∈ℐ. f-``{𝟬⇩S} ⊆ N}"
by auto
{ fix t assume "t∈f-``(f``(?P))"
then have "f`(t) ∈ f``(?P)" and "t∈R"
using func1_1_L15 f_is_fun by simp_all
with P_ideal obtain s where "f`(t) = f`(s)" "s∈?P"
using func_imagedef f_is_fun by auto
from P_ideal ‹s∈?P› have "s∈R" by blast
from ‹t∈R› ‹s∈R› ‹f`(t) = f`(s)› have "f`(t\<rs>⇩Rs) = 𝟬⇩S"
using f_is_fun apply_funtype target_ring.Ring_ZF_1_L3(7)
homomor_dest_subs by simp
with ‹t∈R› ‹s∈R› ‹?X⊆?P› have "t\<rs>⇩Rs ∈ ?P"
using origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun
by auto
with P_ideal ‹s∈?P› have "s\<ra>⇩R(t\<rs>⇩Rs) ∈ ?P"
using origin_ring.ideal_dest_sum by auto
with ‹t∈R› ‹s∈R› have "t∈?P"
using origin_ring.Ring_ZF_2_L1A(5) by auto
} with R show "f-``(?Q) ⊆ ?P"
by auto
{ fix t assume as: "t ∈ M``((f-``(J))×(f-``(K)))"
have "(f-``(J))×(f-``(K)) ⊆ R×R"
using func1_1_L15 f_is_fun by auto
with as obtain t⇩j t⇩k where
jk: "t=t⇩j⋅⇩Rt⇩k" "t⇩j∈f-``(J)" "t⇩k∈f-``(K)"
using AMUV_are_ops(2) func_imagedef IsAssociative_def
by auto
from as have "t∈R" using AMUV_are_ops(2) func1_1_L6(2) by blast
from jk(2,3) have "t⇩j∈R" "f`(t⇩j)∈J" and "t⇩k∈R" "f`(t⇩k)∈K"
using func1_1_L15 f_is_fun by simp_all
from jk(1) ‹t⇩j∈R› ‹t⇩k∈R› have ft: "f`(t) = ((f`(t⇩j))⋅⇩S(f`(t⇩k)))"
using homomor_dest_mult by simp
from ‹f`(t⇩j)∈J› ‹f`(t⇩k) ∈K› have "⟨f`(t⇩j),f`(t⇩k)⟩ ∈ J×K"
by simp
moreover from assms have "V:S×S→S" and "J×K ⊆ S×S"
using AMUV_are_ops(4) target_ring.ideal_dest_subset
by auto
ultimately have "V`⟨f`(t⇩j), f`(t⇩k)⟩ ∈V``(J×K)"
using func_imagedef by force
with assms ft ‹t∈R› have "t ∈ f-``(?Q)"
using target_ring.product_in_intersection(3) func1_1_L15 f_is_fun
by auto
} hence "M``(f-``(J)×f-``(K))⊆f-``(?Q)"
by auto
moreover from assms(1,2) have
id: "(f-``(?Q)) ◃R⇩o"
using preimage_ideal target_ring.product_in_intersection(2)
by simp
ultimately have "(f -`` J) ⋅⇩I (f -`` K)⊆f-``(?Q)"
using ideals origin_ring.generated_ideal_small origin_ring.productIdeal_def
by auto
with assms(1,2) have "?X ⊆ f-``(?Q)"
using target_ring.product_in_intersection(2) target_ring.ideal_dest_zero
by auto
with idealJK id show
"((f-``(J))⋅⇩I(f-``(K)))+⇩I(f-``{𝟬⇩S}) ⊆ f-``(?Q)"
using origin_ring.generated_ideal_small kernel_ideal origin_ring.sumIdeal_def
by simp
qed
text‹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◃R⇩t" "K◃R⇩t" "f∈surj(R,S)"
shows "target_ring.productIdeal(J, K) =
f``(origin_ring.productIdeal((f-``(J)), (f-``(K))))"
proof -
from assms have "f``(f-``(target_ring.productIdeal(J, K)))
= f``(((f-``(J)) ⋅⇩I (f-``(K))) +⇩I (ker))"
using prime_ideal_quot by simp
with assms show ?thesis
using target_ring.product_in_intersection(2)
target_ring.ideal_dest_subset surj_image_vimage
origin_ring.product_in_intersection(2) preimage_ideal
kernel_empty_image(1) target_ring.zero_ideal
by simp
qed
text‹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◃⇩pR⇩o" "ker ⊆ J" "f∈surj(R,S)"
shows "(f``(J))◃⇩pR⇩t"
proof -
from assms(1) have "J ⊆ R" "J ≠ R"
unfolding origin_ring.primeIdeal_def
using origin_ring.ideal_dest_subset by auto
from assms(1,3) have "(f``(J))◃R⇩t"
using image_ideal_surj unfolding origin_ring.primeIdeal_def
by auto
moreover
{ assume "f``(J) = S"
from ‹J ⊆ R› ‹J ≠ R› obtain t where "t∈R-J" by auto
with assms(3) have "f`(t)∈S"
using apply_funtype f_is_fun by auto
with assms(3) ‹J ⊆ R› ‹f``(J) = S› obtain j
where j: "j∈J" "f`(t)= f`(j)"
using func_imagedef f_is_fun by auto
from ‹j∈J› ‹J ⊆ R› have "j∈R" by auto
with assms(3) ‹f`(t)= f`(j)› ‹t∈R-J› have "t\<rs>⇩Rj∈f-``{𝟬⇩S}"
using apply_type target_ring.Ring_ZF_1_L3(7) f_is_fun
homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15
by auto
with assms(1,2) j(1) have "j\<ra>⇩R(t\<rs>⇩Rj) ∈J"
unfolding origin_ring.primeIdeal_def
using origin_ring.ideal_dest_sum by auto
with ‹j∈R› ‹t∈R-J› have False using origin_ring.Ring_ZF_2_L1A(5)
by auto
} hence "f``(J) ≠ S" by auto
moreover
{ fix I K assume as: "I∈target_ring.ideals" "K∈target_ring.ideals"
"target_ring.productIdeal(I, K) ⊆ f``(J)"
let ?A = "(f-``(I)) ⋅⇩I (f-``(K))"
from as(1,2) have "?A ⊆ f-``(f``(?A))"
using origin_ring.product_in_intersection(2) preimage_ideal(2)
origin_ring.ideal_dest_subset func1_1_L9 f_is_fun by auto
with assms(3) as have "?A ⊆ f-``(f``(J))"
using prime_ideal_quot_2 vimage_mono by force
moreover from assms(1) have "J ⊆ f-``(f``(J))"
using func1_1_L9 f_is_fun origin_ring.ideal_dest_subset
unfolding origin_ring.primeIdeal_def by auto
moreover
{ fix t assume "t ∈ f-``(f``(J))"
then have "f`(t)∈f``(J)" "t∈R" using func1_1_L15 f_is_fun
by auto
from assms(1) ‹f`(t)∈f``(J)› obtain s where "f`(t)=f`(s)" "s∈J"
using func_imagedef f_is_fun origin_ring.ideal_dest_subset
unfolding origin_ring.primeIdeal_def by auto
from assms(1) ‹s∈J› have "s∈R"
unfolding origin_ring.primeIdeal_def
using origin_ring.ideal_dest_subset by auto
with assms(2) ‹f`(t)=f`(s)› ‹t∈R› have "t\<rs>⇩Rs ∈ J"
using target_ring.Ring_ZF_1_L3(7) apply_funtype f_is_fun
homomor_dest_subs origin_ring.Ring_ZF_1_L4(2) func1_1_L15
by auto
with assms(1) ‹s∈J› have "s\<ra>⇩R(t\<rs>⇩Rs)∈J"
using origin_ring.ideal_dest_sum
unfolding origin_ring.primeIdeal_def by auto
with ‹s∈R› ‹t∈R› have "t∈J" using origin_ring.Ring_ZF_2_L1A(5)
by auto
} hence "f-``(f``J) ⊆ J" by auto
ultimately have "?A ⊆ J" by auto
with assms(1) as(1,2) have "(f-``(I)) ⊆ J ∨ (f-``(K)) ⊆ J"
using preimage_ideal origin_ring.ideal_dest_subset
unfolding origin_ring.primeIdeal_def
by auto
hence "f``(f-``(I)) ⊆ f``J ∨ f``(f-``(K)) ⊆ f``(J)"
by auto
with assms(3) as(1,2) have "I ⊆ f``(J) ∨ K ⊆ f``(J)"
using surj_image_vimage by auto
}
ultimately show ?thesis unfolding target_ring.primeIdeal_def by auto
qed
text‹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∈surj(R,S)"
defines "idealFun ≡ λJ∈target_ring.ideals. f-``(J)"
shows "idealFun ∈ bij(target_ring.ideals,{K∈ℐ. ker ⊆ K})"
proof -
let ?ℐ⇩t = "target_ring.ideals"
have "idealFun : ?ℐ⇩t → {f-``(J). J∈?ℐ⇩t}"
unfolding idealFun_def using lam_funtype by simp
moreover
{ fix t assume "t ∈ {f-``(J). J∈?ℐ⇩t}"
then obtain K where "K ∈ ?ℐ⇩t" "f-``(K) = t" by auto
then have "K◃R⇩t" by simp
then have "(f-``(K))◃R" "ker ⊆ f-``(K)" using preimage_ideal(2,3)
by simp_all
with ‹f-``(K) = t› have "ker ⊆ t" "t◃R" by simp_all
with ‹f-``(K) = t› have "t∈{K∈ℐ. ker ⊆ K}" using func1_1_L3 f_is_fun
by blast
} hence "{f-``(J). J∈?ℐ⇩t} ⊆ {K∈ℐ. ker ⊆ K}" by blast
ultimately have I: "idealFun : ?ℐ⇩t → {K∈ℐ. ker ⊆ K}"
using func1_1_L1B by auto
{ fix w x assume
as: "w◃R⇩t" "x◃R⇩t" "w⊆S" "x⊆S" "idealFun`(w) = idealFun`(x)"
then have "f``(f-``(w)) = f``(f-``(x))" unfolding idealFun_def by simp
with assms(1) as have "w = x" using surj_image_vimage
by simp
}
with I have "idealFun ∈ inj(?ℐ⇩t,{K∈ℐ. ker ⊆ K})"
unfolding inj_def by auto
moreover
{ fix y assume "y◃R" "y⊆R" "ker ⊆ y"
from ‹y⊆R› have "y ⊆ f-``(f``y)" using func1_1_L9 f_is_fun
by auto
moreover
{ fix t assume "t∈f-``(f``(y))"
then have "f`(t) ∈ f``(y)" "t∈R" using func1_1_L15 f_is_fun
by auto
from ‹f`(t) ∈ f``(y)› ‹y⊆R› obtain s where "s∈y" "f`(t) = f`(s)"
using func_imagedef f_is_fun by auto
from ‹s∈y› ‹y⊆R› have "s∈R" by auto
with ‹t∈R› ‹f`(t) = f`(s)› ‹ker ⊆ y› have "t\<rs>⇩Rs ∈ y"
using target_ring.Ring_ZF_1_L3(7) homomor_dest_subs
origin_ring.Ring_ZF_1_L4(2) func1_1_L15 f_is_fun
by auto
with ‹s∈y› ‹y◃R› ‹s∈R› ‹t∈R› have "t∈y"
using origin_ring.ideal_dest_sum origin_ring.Ring_ZF_2_L1A(5)
by force
}
ultimately have "f-``(f``(y)) = y" by blast
moreover have "f``(y) ⊆ S" using func1_1_L6(2) f_is_fun
unfolding surj_def by auto
moreover from assms(1) ‹y◃R› have "(f``(y))◃R⇩t" using image_ideal_surj
by auto
ultimately have "∃x∈?ℐ⇩t. idealFun`(x) = y"
unfolding idealFun_def by auto
}
with I have "idealFun ∈ surj(?ℐ⇩t,{K∈ℐ. ker ⊆ K})"
unfolding surj_def by auto
ultimately show ?thesis unfolding bij_def by blast
qed
text‹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 ≡ λJ∈target_ring.ideals. f-``(J)"
assumes "J◃R" "ker⊆J" "f∈surj(R,S)"
shows "converse(F)`(J) = f``(J)"
proof-
let ?g = "λJ∈{K∈ℐ. ker⊆K}. f``(J)"
let ?ℐ⇩t = "target_ring.ideals"
let ?C⇩F = "converse(F)"
from assms(1,4) have "?C⇩F ∈ bij({K∈ℐ. ker⊆K}, ?ℐ⇩t)"
using bij_converse_bij ideal_quot_bijection
by auto
then have I: "?C⇩F:{K∈ℐ. ker⊆K} → ?ℐ⇩t"
unfolding bij_def inj_def by auto
moreover from assms(2,3) have J: "J ∈ {K∈ℐ. ker⊆K}"
using origin_ring.ideal_dest_subset by auto
ultimately have ideal: "?C⇩F`(J) ∈ ?ℐ⇩t"
using apply_funtype by blast
with assms(1,4) ideal have "?g`(F`(?C⇩F`(J))) = ?C⇩F`(J)"
using preimage_ideal origin_ring.ideal_dest_subset
surj_image_vimage by auto
moreover
from assms(1) have "F: ?ℐ⇩t → {f-``(J). J∈?ℐ⇩t}"
using lam_funtype by simp
with I J have "F`(?C⇩F`(J)) = J"
using right_inverse_lemma by simp
ultimately have "?g`(J) = ?C⇩F`(J)" by simp
with J show ?thesis by simp
qed
text‹Since the map is surjective, this bijection
restricts to prime ideals on both sides.›
corollary (in ring_homo) prime_ideal_quot_3:
assumes "K◃R⇩t" "f ∈ surj(R,S)"
shows "K◃⇩pR⇩t ⟷ ((f-``(K))◃⇩pR)"
proof
{ assume "K◃⇩pR⇩t"
with assms(2) show "(f-``(K))◃⇩pR"
using preimage_prime_ideal_surj target_ring.ideal_dest_subset
unfolding target_ring.primeIdeal_def by auto
}
{ assume "(f-``(K))◃⇩pR"
with assms(1,2) have "K◃R⇩t" and "K≠S"
using func1_1_L4 unfolding origin_ring.primeIdeal_def surj_def
by auto
moreover
{ fix J P assume jp: "J∈target_ring.ideals"
"P∈target_ring.ideals"
"target_ring.productIdeal(J, P) ⊆ K"
from jp(3) have "f-``(target_ring.productIdeal(J, P)) ⊆ f-``(K)"
by auto
with assms(2) jp(1,2) have
A: "((f-``(J)) ⋅⇩I (f-``(P))) +⇩I (ker) ⊆ f-``(K)"
using prime_ideal_quot by auto
from jp(1,2) have
"(f-``(J))⋅⇩I(f-``(P)) ∪ ker ⊆ ((f-``(J))⋅⇩I(f-``(P))) +⇩I (ker)"
using preimage_ideal origin_ring.product_in_intersection(2)
kernel_ideal origin_ring.comp_in_sum_ideals(3) by simp
with A have "((f -`` J) ⋅⇩I (f -`` P)) ⊆ f-``(K)" by auto
with ‹(f-``(K))◃⇩pR› jp(1,2) have
"f-``(J) ⊆ f-``(K) ∨ f-``(P) ⊆ f-``(K)"
using preimage_ideal origin_ring.ideal_dest_subset
unfolding origin_ring.primeIdeal_def by auto
then have
"f``(f-``(J)) ⊆ f``(f-``(K)) ∨ f``(f-``(P)) ⊆ f``(f-``(K))"
by blast
with assms jp(1,2) have "J ⊆ K ∨ P ⊆ K"
using surj_image_vimage target_ring.ideal_dest_subset
by auto
}
ultimately show "K◃⇩pR⇩t"
unfolding target_ring.primeIdeal_def by auto
}
qed
text‹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 ≡ λJ∈target_ring.ideals. f-``(J)"
assumes "f ∈ surj(R,S)"
shows "restrict(F,{J∈Pow(S). J◃⇩pR⇩t}) ∈
bij({J∈Pow(S). J◃⇩pR⇩t}, {J∈Pow(R). ker⊆J ∧ (J◃⇩pR)})"
proof -
let ?ℐ⇩t = "target_ring.ideals"
from assms have I: "F:?ℐ⇩t → {K∈ℐ. ker ⊆ K}"
using ideal_quot_bijection bij_is_fun by simp
have II: "{J∈Pow(S). J◃⇩pR⇩t} ⊆ ?ℐ⇩t"
unfolding target_ring.primeIdeal_def by auto
have III: "{J∈Pow(S). J◃⇩pR⇩t} ⊆ ?ℐ⇩t"
unfolding target_ring.primeIdeal_def by auto
with assms have "restrict(F,{J∈Pow(S). J◃⇩pR⇩t}) ∈
bij({J∈Pow(S). J◃⇩pR⇩t}, F``{J∈Pow(S). J◃⇩pR⇩t})"
using restrict_bij ideal_quot_bijection unfolding bij_def
by auto
moreover have "{t∈Pow(R). ker⊆t ∧ (t◃⇩pR)} = F``{J∈Pow(S). J◃⇩pR⇩t}"
proof
{ fix t assume "t ∈ F``{J∈Pow(S). J◃⇩pR⇩t}"
with I III obtain q where "q∈Pow(S)" "q◃⇩pR⇩t" "t=F`(q)"
using func_imagedef by auto
from ‹q∈Pow(S)› ‹q◃⇩pR⇩t› have "q∈?ℐ⇩t"
unfolding target_ring.primeIdeal_def by auto
with I have "F`(q) ∈ {K∈ℐ. ker ⊆ K}" using apply_funtype
by blast
with assms ‹q◃⇩pR⇩t› ‹t=F`(q)› ‹q∈?ℐ⇩t› ‹t=F`(q)›
have "t◃R" "t◃⇩pR" "ker⊆t"
using prime_ideal_quot_3 by simp_all
} then show "F``{J∈Pow(S). J◃⇩pR⇩t} ⊆ {t∈Pow(R). ker⊆t ∧ (t◃⇩pR)}"
using origin_ring.ideal_dest_subset by blast
{ fix t assume "t∈{t∈Pow(R). ker⊆t ∧ (t◃⇩pR)}"
then have "t∈Pow(R)" "ker⊆t" "t◃⇩pR" by auto
then have tSet: "t ∈ {t∈ℐ. ker ⊆ t}"
unfolding origin_ring.primeIdeal_def by auto
with assms have cont: "converse(F)`(t) ∈ ?ℐ⇩t"
using ideal_quot_bijection bij_converse_bij
apply_funtype bij_is_fun by blast
moreover from assms tSet have "F`(converse(F)`(t)) = t"
using ideal_quot_bijection right_inverse_bij by blast
ultimately have "f-``(converse(F)`(t)) = t"
using assms(1) by simp
with assms II tSet ‹t◃⇩pR› cont have "t ∈ F``{J∈Pow(S). J◃⇩pR⇩t}"
using prime_ideal_quot_3 target_ring.ideal_dest_subset
bij_val_image_vimage ideal_quot_bijection
unfolding target_ring.primeIdeal_def by auto
} thus "{t∈Pow(R). ker⊆t ∧ (t◃⇩pR)} ⊆ F``{J∈Pow(S). J◃⇩pR⇩t}"
by auto
qed
ultimately show ?thesis by auto
qed
end