Quelle QuotRing.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/QuotRing.thy
    Author:     Stephan Hohe
    Author:     Paulo Emílio de Vilhena
*)

theory QuotRing
imports RingHom
begin

section \<open>Quotient Rings\<close>

subsection \<open>Multiplication on Cosets\<close>

definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \ 'a set"
    (\<open>(\<open>open_block notation=\<open>mixfix rcoset_mult\<close>\<close>[mod _:] _ \<Otimes>\<index> _)\<close> [81,81,81] 80)
  where "rcoset_mult R I A B = (\a\A. \b\B. I +>\<^bsub>R\<^esub> (a \\<^bsub>R\<^esub> b))"

text \<open>\<^const>\<open>rcoset_mult\<close> fulfils the properties required by congruences\<close>
lemma (in ideal) rcoset_mult_add:
  assumes "x \ carrier R" "y \ carrier R"
  shows "[mod I:] (I +> x) \ (I +> y) = I +> (x \ y)"
proof -
  have 1: "z \ I +> x \ y"
    if x'rcos: "x' \<in> I +> x" and y'rcos: "y' \<in> I +> y" and zrcos: "z \<in> I +> x' \<otimes> y'" for z x' y'
  proof -
    from that
    obtain hx hy hz where hxI: "hx \ I" and x': "x' = hx \ x" and hyI: "hy \ I" and y': "y' = hy \ y"
      and hzI: "hz \ I" and z: "z = hz \ (x' \ y')"
      by (auto simp: a_r_coset_def r_coset_def)
    note carr = assms hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr]
    from z  x' y' have "z = hz \ ((hx \ x) \ (hy \ y))" by simp
    also from carr have "\ = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" by algebra
    finally have z2: "z = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" .
    from hxI hyI hzI carr have "hz \ (hx \ (hy \ y)) \ x \ hy \ I"
      by (simp add: I_l_closed I_r_closed)
    with z2 show ?thesis
      by (auto simp add: a_r_coset_def r_coset_def)
  qed
  have 2: "\a\I +> x. \b\I +> y. z \ I +> a \ b" if "z \ I +> x \ y" for z
    using assms a_rcos_self that by blast
  show ?thesis
    unfolding rcoset_mult_def using assms
    by (auto simp: intro!: 1 2)
qed

subsection \<open>Quotient Ring Definition\<close>

definition FactRing :: "[('a,'b) ring_scheme, 'a set] \ ('a set) ring"
    (infixl \<open>Quot\<close> 65)
  where "FactRing R I =
    \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I,
      one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"

lemmas FactRing_simps = FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]

subsection \<open>Factorization over General Ideals\<close>

text \<open>The quotient is a ring\<close>
lemma (in ideal) quotient_is_ring: "ring (R Quot I)"
proof (rule ringI)
  show "abelian_group (R Quot I)"
    by (rule comm_group_abelian_groupI)
      (simp add: FactRing_def a_factorgroup_is_comm_group[unfolded A_FactGroup_def'])
  show "Group.monoid (R Quot I)"
    by (rule monoidI)
      (auto simp add: FactRing_simps rcoset_mult_add m_assoc)
qed (auto simp: FactRing_simps rcoset_mult_add a_rcos_sum l_distr r_distr)

text \<open>This is a ring homomorphism\<close>

lemma (in ideal) rcos_ring_hom: "((+>) I) \ ring_hom R (R Quot I)"
  by (simp add: ring_hom_memI FactRing_def a_rcosetsI[OF a_subset] rcoset_mult_add a_rcos_sum)

lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) ((+>) I)"
  by (simp add: local.ring_axioms quotient_is_ring rcos_ring_hom ring_hom_ringI2)

text \<open>The quotient of a cring is also commutative\<close>
lemma (in ideal) quotient_is_cring:
  assumes "cring R"
  shows "cring (R Quot I)"
proof -
  interpret cring R by fact
  show ?thesis
    apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro quotient_is_ring)
     apply (rule ring.axioms[OF quotient_is_ring])
    apply (auto simp add: FactRing_simps rcoset_mult_add m_comm)
    done
qed

text \<open>Cosets as a ring homomorphism on crings\<close>
lemma (in ideal) rcos_ring_hom_cring:
  assumes "cring R"
  shows "ring_hom_cring R (R Quot I) ((+>) I)"
proof -
  interpret cring R by fact
  show ?thesis
    apply (rule ring_hom_cringI)
      apply (rule rcos_ring_hom_ring)
     apply (rule is_cring)
    apply (rule quotient_is_cring)
    apply (rule is_cring)
    done
qed

subsection \<open>Factorization over Prime Ideals\<close>

text \<open>The quotient ring generated by a prime ideal is a domain\<close>
lemma (in primeideal) quotient_is_domain: "domain (R Quot I)"
proof -
  have 1: "I +> \ = I \ False"
    using I_notcarr a_rcos_self one_imp_carrier by blast
  have 2: "I +> x = I"
    if  carr: "x \ carrier R" "y \ carrier R"
    and a: "I +> x \ y = I"
    and b: "I +> y \ I" for x y
    by (metis I_prime a a_rcos_const a_rcos_self b m_closed that)
  show ?thesis
    apply (intro domain.intro quotient_is_cring is_cring domain_axioms.intro)
     apply (metis "1" FactRing_def monoid.simps(2) ring.simps(1))
    apply (simp add: FactRing_simps)
    apply (metis "2" rcoset_mult_add)
    done
qed

text \<open>Generating right cosets of a prime ideal is a homomorphism
        on commutative rings\<close>
lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) ((+>) I)"
  by (rule rcos_ring_hom_cring) (rule is_cring)

subsection \<open>Factorization over Maximal Ideals\<close>

text \<open>In a commutative ring, the quotient ring over a maximal ideal is a field.
        The proof follows ``W. Adkins, S. Weintraub: Algebra -- An Approach via Module Theory''\<close>
proposition (in maximalideal) quotient_is_field:
  assumes "cring R"
  shows "field (R Quot I)"
proof -
  interpret cring R by fact
  have 1: "\\<^bsub>R Quot I\<^esub> \ \\<^bsub>R Quot I\<^esub>" \ \Quotient is not empty\
  proof
    assume "\\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot I\<^esub>"
    then have II1: "I = I +> \" by (simp add: FactRing_def)
    then have "I = carrier R"
      using a_rcos_self one_imp_carrier by blast
    with I_notcarr show False by simp
  qed
  have 2: "\y\carrier R. I +> a \ y = I +> \" if IanI: "I +> a \ I" and acarr: "a \ carrier R" for a
    \<comment> \<open>Existence of Inverse\<close>
  proof -
    \<comment> \<open>Helper ideal \<open>J\<close>\<close>
    define J :: "'a set" where "J = (carrier R #> a) <+> I"
    have idealJ: "ideal J R"
      using J_def acarr add_ideals cgenideal_eq_rcos cgenideal_ideal is_ideal by auto
    have IinJ: "I \ J"
    proof (clarsimp simp: J_def r_coset_def set_add_defs)
      fix x
      assume xI: "x \ I"
      have "x = \ \ a \ x"
        by (simp add: acarr xI)
      with xI show "\xa\carrier R. \k\I. x = xa \ a \ k" by fast
    qed
    have JnI: "J \ I"
    proof -
      have "a \ I"
        using IanI a_rcos_const by blast
      moreover have "a \ J"
      proof (simp add: J_def r_coset_def set_add_defs)
        from acarr
        have "a = \ \ a \ \" by algebra
        with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup]
        show "\x\carrier R. \k\I. a = x \ a \ k" by fast
      qed
      ultimately show ?thesis by blast
    qed
    then have Jcarr: "J = carrier R"
      using I_maximal IinJ additive_subgroup.a_subset idealJ ideal_def by blast

    \<comment> \<open>Calculating an inverse for \<^term>\<open>a\<close>\<close>
    from one_closed[folded Jcarr]
    obtain r i where rcarr: "r \ carrier R"
      and iI: "i \ I" and one: "\ = r \ a \ i"
      by (auto simp add: J_def r_coset_def set_add_defs)

    from one and rcarr and acarr and iI[THEN a_Hcarr]
    have rai1: "a \ r = \i \ \" by algebra

    \<comment> \<open>Lifting to cosets\<close>
    from iI have "\i \ \ \ I +> \"
      by (intro a_rcosI, simp, intro a_subset, simp)
    with rai1 have "a \ r \ I +> \" by simp
    then have "I +> \ = I +> a \ r"
      by (rule a_repr_independence, simp) (rule a_subgroup)

    from rcarr and this[symmetric]
    show "\r\carrier R. I +> a \ r = I +> \" by fast
  qed
  show ?thesis
    apply (intro cring.cring_fieldI2 quotient_is_cring is_cring 1)
     apply (clarsimp simp add: FactRing_simps rcoset_mult_add 2)
    done
qed

lemma (in ring_hom_ring) trivial_hom_iff:
  "(h ` (carrier R) = { \\<^bsub>S\<^esub> }) = (a_kernel R S h = carrier R)"
  using group_hom.trivial_hom_iff[OF a_group_hom] by (simp add: a_kernel_def)

lemma (in ring_hom_ring) trivial_ker_imp_inj:
  assumes "a_kernel R S h = { \ }"
  shows "inj_on h (carrier R)"
  using group_hom.trivial_ker_imp_inj[OF a_group_hom] assms a_kernel_def[of R S h] by simp

(* NEW ========================================================================== *)
lemma (in ring_hom_ring) inj_iff_trivial_ker:
  shows "inj_on h (carrier R) \ a_kernel R S h = { \ }"
  using group_hom.inj_iff_trivial_ker[OF a_group_hom] a_kernel_def[of R S h] by simp

(* NEW ========================================================================== *)
corollary ring_hom_in_hom:
  assumes "h \ ring_hom R S" shows "h \ hom R S" and "h \ hom (add_monoid R) (add_monoid S)"
  using assms unfolding ring_hom_def hom_def by auto

(* NEW ========================================================================== *)
corollary set_add_hom:
  assumes "h \ ring_hom R S" "I \ carrier R" and "J \ carrier R"
  shows "h ` (I <+>\<^bsub>R\<^esub> J) = h ` I <+>\<^bsub>S\<^esub> h ` J"
  using set_mult_hom[OF ring_hom_in_hom(2)[OF assms(1)]] assms(2-3)
  unfolding a_kernel_def[of R S h] set_add_def by simp

(* NEW ========================================================================== *)
corollary a_coset_hom:
  assumes "h \ ring_hom R S" "I \ carrier R" "a \ carrier R"
  shows "h ` (a <+\<^bsub>R\<^esub> I) = h a <+\<^bsub>S\<^esub> (h ` I)" and "h ` (I +>\<^bsub>R\<^esub> a) = (h ` I) +>\<^bsub>S\<^esub> h a"
  using assms coset_hom[OF ring_hom_in_hom(2)[OF assms(1)], of I a]
  unfolding a_l_coset_def l_coset_eq_set_mult
            a_r_coset_def r_coset_eq_set_mult
  by simp_all

(* NEW ========================================================================== *)
corollary (in ring_hom_ring) set_add_ker_hom:
  assumes "I \ carrier R"
  shows "h ` (I <+> (a_kernel R S h)) = h ` I" and "h ` ((a_kernel R S h) <+> I) = h ` I"
  using group_hom.set_mult_ker_hom[OF a_group_hom] assms
  unfolding a_kernel_def[of R S h] set_add_def by simp+

lemma (in ring_hom_ring) non_trivial_field_hom_imp_inj:
  assumes R: "field R"
    and h: "h ` (carrier R) \ { \\<^bsub>S\<^esub> }"
  shows "inj_on h (carrier R)"
proof -
  from h have "a_kernel R S h \ carrier R"
    using trivial_hom_iff by linarith
  hence "a_kernel R S h = { \ }"
    using field.all_ideals[OF R] kernel_is_ideal by blast
  thus "inj_on h (carrier R)"
    using trivial_ker_imp_inj by blast
qed

lemma "field R \ cring R"
  using fieldE(1) by blast

lemma non_trivial_field_hom_is_inj:
  assumes "h \ ring_hom R S" and "field R" and "field S"
  shows "inj_on h (carrier R)"
proof -
  interpret ring_hom_cring R S h
    using assms(1) ring_hom_cring.intro[OF assms(2-3)[THEN fieldE(1)]]
    unfolding symmetric[OF ring_hom_cring_axioms_def] by simp

  have "h \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>" and "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>"
    using domain.one_not_zero[OF field.axioms(1)[OF assms(3)]] by auto
  hence "h ` (carrier R) \ { \\<^bsub>S\<^esub> }"
    using ring.kernel_zero ring.trivial_hom_iff by fastforce
  thus ?thesis
    using ring.non_trivial_field_hom_imp_inj[OF assms(2)] by simp
qed

lemma (in ring_hom_ring) img_is_add_subgroup:
  assumes "subgroup H (add_monoid R)"
  shows "subgroup (h ` H) (add_monoid S)"
proof -
  have "group ((add_monoid R) \ carrier := H \)"
    using assms R.add.subgroup_imp_group by blast
  moreover have "H \ carrier R" by (simp add: R.add.subgroupE(1) assms)
  hence "h \ hom ((add_monoid R) \ carrier := H \) (add_monoid S)"
    unfolding hom_def by (auto simp add: subsetD)
  ultimately have "subgroup (h ` carrier ((add_monoid R) \ carrier := H \)) (add_monoid S)"
    using group_hom.img_is_subgroup[of "(add_monoid R) \ carrier := H \" "add_monoid S" h]
    using a_group_hom group_hom_axioms.intro group_hom_def by blast
  thus "subgroup (h ` H) (add_monoid S)" by simp
qed

lemma (in ring) ring_ideal_imp_quot_ideal:
  assumes "ideal I R"
    and A: "ideal J R"
  shows "ideal ((+>) I ` J) (R Quot I)"
proof (rule idealI)
  show "ring (R Quot I)"
    by (simp add: assms(1) ideal.quotient_is_ring)
next
  have "subgroup J (add_monoid R)"
    by (simp add: additive_subgroup.a_subgroup A ideal.axioms(1))
  moreover have "((+>) I) \ ring_hom R (R Quot I)"
    by (simp add: assms(1) ideal.rcos_ring_hom)
  ultimately show "subgroup ((+>) I ` J) (add_monoid (R Quot I))"
    using assms(1) ideal.rcos_ring_hom_ring ring_hom_ring.img_is_add_subgroup by blast
next
  fix a x assume "a \ (+>) I ` J" "x \ carrier (R Quot I)"
  then obtain i j where i: "i \ carrier R" "x = I +> i"
    and j: "j \ J" "a = I +> j"
    unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
  hence "a \\<^bsub>R Quot I\<^esub> x = [mod I:] (I +> j) \ (I +> i)"
    unfolding FactRing_def by simp
  hence "a \\<^bsub>R Quot I\<^esub> x = I +> (j \ i)"
    using ideal.rcoset_mult_add[OF assms(1), of j i] i(1) j(1) A ideal.Icarr by force
  thus "a \\<^bsub>R Quot I\<^esub> x \ (+>) I ` J"
    using A i(1) j(1) by (simp add: ideal.I_r_closed)

  have "x \\<^bsub>R Quot I\<^esub> a = [mod I:] (I +> i) \ (I +> j)"
    unfolding FactRing_def i j by simp
  hence "x \\<^bsub>R Quot I\<^esub> a = I +> (i \ j)"
    using ideal.rcoset_mult_add[OF assms(1), of i j] i(1) j(1) A ideal.Icarr by force
  thus "x \\<^bsub>R Quot I\<^esub> a \ (+>) I ` J"
    using A i(1) j(1) by (simp add: ideal.I_l_closed)
qed

lemma (in ring_hom_ring) ideal_vimage:
  assumes "ideal I S"
  shows "ideal { r \ carrier R. h r \ I } R" (* or (carrier R) \ (h -` I) *)
proof
  show "{ r \ carrier R. h r \ I } \ carrier (add_monoid R)" by auto
  show "\\<^bsub>add_monoid R\<^esub> \ { r \ carrier R. h r \ I }"
    by (simp add: additive_subgroup.zero_closed assms ideal.axioms(1))
next
  fix a b
  assume "a \ { r \ carrier R. h r \ I }"
     and "b \ { r \ carrier R. h r \ I }"
  hence a: "a \ carrier R" "h a \ I"
    and b: "b \ carrier R" "h b \ I" by auto
  hence "h (a \ b) = (h a) \\<^bsub>S\<^esub> (h b)" using hom_add by blast
  moreover have "(h a) \\<^bsub>S\<^esub> (h b) \ I" using a b assms
    by (simp add: additive_subgroup.a_closed ideal.axioms(1))
  ultimately show "a \\<^bsub>add_monoid R\<^esub> b \ { r \ carrier R. h r \ I }"
    using a(1) b (1) by auto

  have "h (\ a) = \\<^bsub>S\<^esub> (h a)" by (simp add: a)
  moreover have "\\<^bsub>S\<^esub> (h a) \ I"
    by (simp add: a(2) additive_subgroup.a_inv_closed assms ideal.axioms(1))
  ultimately show "inv\<^bsub>add_monoid R\<^esub> a \ { r \ carrier R. h r \ I }"
    using a by (simp add: a_inv_def)
next
  fix a r
  assume "a \ { r \ carrier R. h r \ I }" and r: "r \ carrier R"
  hence a: "a \ carrier R" "h a \ I" by auto

  have "h a \\<^bsub>S\<^esub> h r \ I"
    using assms a r by (simp add: ideal.I_r_closed)
  thus "a \ r \ { r \ carrier R. h r \ I }" by (simp add: a(1) r)

  have "h r \\<^bsub>S\<^esub> h a \ I"
    using assms a r by (simp add: ideal.I_l_closed)
  thus "r \ a \ { r \ carrier R. h r \ I }" by (simp add: a(1) r)
qed

lemma (in ring) canonical_proj_vimage_in_carrier:
  assumes "ideal I R"
    and A: "J \ carrier (R Quot I)"
  shows "\ J \ carrier R"
proof
  fix j assume j: "j \ \ J"
  then obtain j' where j': "j' \ J" "j \ j'"
    by blast
  then obtain r where r: "r \ carrier R" "j' = I +> r"
    using A j' unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
  thus "j \ carrier R"
    using j' assms
    by (meson a_r_coset_subset_G additive_subgroup.a_subset contra_subsetD ideal.axioms(1))
qed

lemma (in ring) canonical_proj_vimage_mem_iff:
  assumes "ideal I R" "J \ carrier (R Quot I)"
    and a: "a \ carrier R"
  shows "(a \ \ J) = (I +> a \ J)"
proof
  assume "a \ \ J"
  then obtain j where j: "j \ J" "a \ j" by blast
  then obtain r where r: "r \ carrier R" "j = I +> r"
    using assms j unfolding FactRing_def using A_RCOSETS_def'[of R I] by auto
  hence "I +> r = I +> a"
    using add.repr_independence[of a I r] j r
    by (metis a_r_coset_def additive_subgroup.a_subgroup assms(1) ideal.axioms(1))
  thus "I +> a \ J" using r j by simp
next
  assume "I +> a \ J"
  hence "\ \ a \ I +> a"
    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]]
          a_r_coset_def'[of R I a] by blast
  thus "a \ \ J" using a \I +> a \ J\ by auto
qed

corollary (in ring) quot_ideal_imp_ring_ideal:
  assumes "ideal I R"
  shows "ideal J (R Quot I) \ ideal (\ J) R"
proof -
  assume A: "ideal J (R Quot I)"
  have "\ J = { r \ carrier R. I +> r \ J }"
    using canonical_proj_vimage_in_carrier[OF assms, of J]
          canonical_proj_vimage_mem_iff[OF assms, of J]
          additive_subgroup.a_subset[OF ideal.axioms(1)[OF A]] by blast
  thus "ideal (\ J) R"
    using ring_hom_ring.ideal_vimage[OF ideal.rcos_ring_hom_ring[OF assms] A] by simp
qed

lemma (in ring) ideal_incl_iff:
  assumes "ideal I R" "ideal J R"
  shows "(I \ J) = (J = (\ j \ J. I +> j))"
proof
  assume "J = (\ j \ J. I +> j)" hence "I +> \ \ J"
    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
  thus "I \ J" using additive_subgroup.a_subset[OF ideal.axioms(1)[OF assms(1)]] by simp
next
  assume A: "I \ J" show "J = (\j\J. I +> j)"
  proof
    show "J \ (\ j \ J. I +> j)"
    proof
      fix j assume j: "j \ J"
      have "\ \ I" by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
      hence "\ \ j \ I +> j"
        using a_r_coset_def'[of R I j] by blast
      thus "j \ (\j\J. I +> j)"
        using assms(2) j additive_subgroup.a_Hcarr ideal.axioms(1) by fastforce
    qed
    show "(\ j \ J. I +> j) \ J"
    proof
      fix x assume "x \ (\ j \ J. I +> j)"
      then obtain j where j: "j \ J" "x \ I +> j" by blast
      then obtain i where i: "i \ I" "x = i \ j"
        using a_r_coset_def'[of R I j] by blast
      thus "x \ J"
        using assms(2) j A additive_subgroup.a_closed[OF ideal.axioms(1)[OF assms(2)]] by blast
    qed
  qed
qed

theorem (in ring) quot_ideal_correspondence:
  assumes "ideal I R"
  shows "bij_betw (\J. (+>) I ` J) { J. ideal J R \ I \ J } { J . ideal J (R Quot I) }"
proof (rule bij_betw_byWitness[where ?f' = "\X. \ X"])
  show "\J \ { J. ideal J R \ I \ J }. (\X. \ X) ((+>) I ` J) = J"
    using assms ideal_incl_iff by blast
  show "(\J. (+>) I ` J) ` { J. ideal J R \ I \ J } \ { J. ideal J (R Quot I) }"
    using assms ring_ideal_imp_quot_ideal by auto
  show "(\X. \ X) ` { J. ideal J (R Quot I) } \ { J. ideal J R \ I \ J }"
  proof
    fix J assume "J \ ((\X. \ X) ` { J. ideal J (R Quot I) })"
    then obtain J' where J': "ideal J' (R Quot I)" "J = \ J'" by blast
    hence "ideal J R"
      using assms quot_ideal_imp_ring_ideal by auto
    moreover have "I \ J'"
      using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF J'(1)]] unfolding FactRing_def by simp
    ultimately show "J \ { J. ideal J R \ I \ J }" using J'(2) by auto
  qed
  show "\J' \ { J. ideal J (R Quot I) }. ((+>) I ` (\ J')) = J'"
  proof
    fix J' assume "J' \<in> { J. ideal J (R Quot I) }"
    hence subset: "J' \ carrier (R Quot I) \ ideal J' (R Quot I)"
      using additive_subgroup.a_subset ideal_def by blast
    hence "((+>) I ` (\ J')) \ J'"
      using canonical_proj_vimage_in_carrier canonical_proj_vimage_mem_iff
      by (meson assms contra_subsetD image_subsetI)
    moreover have "J' \ ((+>) I ` (\ J'))"
    proof
      fix x assume "x \ J'"
      then obtain r where r: "r \ carrier R" "x = I +> r"
        using subset unfolding FactRing_def A_RCOSETS_def'[of R I] by auto
      hence "r \ (\ J')"
        using \<open>x \<in> J'\<close> assms canonical_proj_vimage_mem_iff subset by blast
      thus "x \ ((+>) I ` (\ J'))" using r(2) by blast
    qed
    ultimately show "((+>) I ` (\ J')) = J'" by blast
  qed
qed

lemma (in cring) quot_domain_imp_primeideal:
  assumes "ideal P R"
    and A: "domain (R Quot P)"
  shows "primeideal P R"
proof -
  show "primeideal P R"
  proof (rule primeidealI)
    show "ideal P R" using assms(1) .
    show "cring R" using is_cring .
  next
    show "carrier R \ P"
    proof (rule ccontr)
      assume "\ carrier R \ P" hence "carrier R = P" by simp
      hence "\I. I \ carrier (R Quot P) \ I = P"
        unfolding FactRing_def A_RCOSETS_def' apply simp
        using a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1) by blast
      hence "\\<^bsub>(R Quot P)\<^esub> = \\<^bsub>(R Quot P)\<^esub>"
        by (metis assms ideal.quotient_is_ring ring.ring_simprules(2) ring.ring_simprules(6))
      thus False using domain.one_not_zero[OF A] by simp
    qed
  next
    fix a b assume a: "a \ carrier R" and b: "b \ carrier R" and ab: "a \ b \ P"
    hence "P +> (a \ b) = \\<^bsub>(R Quot P)\<^esub>" unfolding FactRing_def
      by (simp add: a_coset_join2 additive_subgroup.a_subgroup assms ideal.axioms(1))
    moreover have "(P +> a) \\<^bsub>(R Quot P)\<^esub> (P +> b) = P +> (a \ b)" unfolding FactRing_def
      using a b by (simp add: assms ideal.rcoset_mult_add)
    moreover have "P +> a \ carrier (R Quot P) \ P +> b \ carrier (R Quot P)"
      by (simp add: a b FactRing_def a_rcosetsI additive_subgroup.a_subset assms ideal.axioms(1))
    ultimately have "P +> a = \\<^bsub>(R Quot P)\<^esub> \ P +> b = \\<^bsub>(R Quot P)\<^esub>"
      using domain.integral[OF A, of "P +> a" "P +> b"] by auto
    thus "a \ P \ b \ P" unfolding FactRing_def apply simp
      using a b assms a_coset_join1 additive_subgroup.a_subgroup ideal.axioms(1) by blast
  qed
qed

lemma (in cring) quot_domain_iff_primeideal:
  assumes "ideal P R"
  shows "domain (R Quot P) = primeideal P R"
  using quot_domain_imp_primeideal[OF assms] primeideal.quotient_is_domain[of P R] by auto

subsection \<open>Isomorphism\<close>

definition
  ring_iso :: "_ \ _ \ ('a \ 'b) set"
  where "ring_iso R S = { h. h \ ring_hom R S \ bij_betw h (carrier R) (carrier S) }"

definition
  is_ring_iso :: "_ \ _ \ bool" (infixr \\\ 60)
  where "R \ S = (ring_iso R S \ {})"

definition
  morphic_prop :: "_ \ ('a \ bool) \ bool"
  where "morphic_prop R P =
           ((P \<one>\<^bsub>R\<^esub>) \<and>
            (\<forall>r \<in> carrier R. P r) \<and>
            (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<otimes>\<^bsub>R\<^esub> r2)) \<and>
            (\<forall>r1 \<in> carrier R. \<forall>r2 \<in> carrier R. P (r1 \<oplus>\<^bsub>R\<^esub> r2)))"

lemma ring_iso_memI:
  fixes R (structure) and S (structure)
  assumes "\x. x \ carrier R \ h x \ carrier S"
      and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y"
      and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y"
      and "h \ = \\<^bsub>S\<^esub>"
      and "bij_betw h (carrier R) (carrier S)"
  shows "h \ ring_iso R S"
  by (auto simp add: ring_hom_memI assms ring_iso_def)

lemma ring_iso_memE:
  fixes R (structure) and S (structure)
  assumes "h \ ring_iso R S"
  shows "\x. x \ carrier R \ h x \ carrier S"
   and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y"
   and "\x y. \ x \ carrier R; y \ carrier R \ \ h (x \ y) = h x \\<^bsub>S\<^esub> h y"
   and "h \ = \\<^bsub>S\<^esub>"
   and "bij_betw h (carrier R) (carrier S)"
  using assms unfolding ring_iso_def ring_hom_def by auto

lemma morphic_propI:
  fixes R (structure)
  assumes "P \"
    and "\r. r \ carrier R \ P r"
    and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)"
    and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)"
  shows "morphic_prop R P"
  unfolding morphic_prop_def using assms by auto

lemma morphic_propE:
  fixes R (structure)
  assumes "morphic_prop R P"
  shows "P \"
    and "\r. r \ carrier R \ P r"
    and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)"
    and "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ P (r1 \ r2)"
  using assms unfolding morphic_prop_def by auto

(* NEW ============================================================================ *)
lemma (in ring) ring_hom_restrict:
  assumes "f \ ring_hom R S" and "\r. r \ carrier R \ f r = g r" shows "g \ ring_hom R S"
  using assms(2) ring_hom_memE[OF assms(1)] by (auto intro: ring_hom_memI)

(* PROOF ========================================================================== *)
lemma (in ring) ring_iso_restrict:
  assumes "f \ ring_iso R S" and "\r. r \ carrier R \ f r = g r" shows "g \ ring_iso R S"
proof -
  have hom: "g \ ring_hom R S"
    using ring_hom_restrict assms unfolding ring_iso_def by auto
  have "bij_betw g (carrier R) (carrier S)"
    using bij_betw_cong[of "carrier R" f g] ring_iso_memE(5)[OF assms(1)] assms(2) by simp
  thus ?thesis
    using ring_hom_memE[OF hom] by (auto intro!: ring_iso_memI)
qed

lemma ring_iso_morphic_prop:
  assumes "f \ ring_iso R S"
    and "morphic_prop R P"
    and "\r. P r \ f r = g r"
  shows "g \ ring_iso R S"
proof -
  have eq0: "\r. r \ carrier R \ f r = g r"
   and eq1: "f \\<^bsub>R\<^esub> = g \\<^bsub>R\<^esub>"
   and eq2: "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ f (r1 \\<^bsub>R\<^esub> r2) = g (r1 \\<^bsub>R\<^esub> r2)"
   and eq3: "\r1 r2. \ r1 \ carrier R; r2 \ carrier R \ \ f (r1 \\<^bsub>R\<^esub> r2) = g (r1 \\<^bsub>R\<^esub> r2)"
    using assms(2-3) unfolding morphic_prop_def by auto
  show ?thesis
    apply (rule ring_iso_memI)
    using assms(1) eq0 ring_iso_memE(1) apply fastforce
    apply (metis assms(1) eq0 eq2 ring_iso_memE(2))
    apply (metis assms(1) eq0 eq3 ring_iso_memE(3))
    using assms(1) eq1 ring_iso_memE(4) apply fastforce
    using assms(1) bij_betw_cong eq0 ring_iso_memE(5) by blast
qed

lemma (in ring) ring_hom_imp_img_ring:
  assumes "h \ ring_hom R S"
  shows "ring (S \ carrier := h ` (carrier R), zero := h \ \)" (is "ring ?h_img")
proof -
  have "h \ hom (add_monoid R) (add_monoid S)"
    using assms unfolding hom_def ring_hom_def by auto
  hence "comm_group ((add_monoid S) \ carrier := h ` (carrier R), one := h \ \)"
    using add.hom_imp_img_comm_group[of h "add_monoid S"] by simp
  hence comm_group: "comm_group (add_monoid ?h_img)"
    by (auto intro: comm_monoidI simp add: monoid.defs)

  moreover have "h \ hom R S"
    using assms unfolding ring_hom_def hom_def by auto
  hence "monoid (S \ carrier := h ` (carrier R), one := h \ \)"
    using hom_imp_img_monoid[of h S] by simp
  hence monoid: "monoid ?h_img"
    using ring_hom_memE(4)[OF assms] unfolding monoid_def by (simp add: monoid.defs)
  show ?thesis
  proof (rule ringI, simp_all add: comm_group_abelian_groupI[OF comm_group] monoid)
    fix x y z assume "x \ h ` carrier R" "y \ h ` carrier R" "z \ h ` carrier R"
    then obtain r1 r2 r3
      where r1: "r1 \ carrier R" "x = h r1"
        and r2: "r2 \ carrier R" "y = h r2"
        and r3: "r3 \ carrier R" "z = h r3" by blast
    hence "(x \\<^bsub>S\<^esub> y) \\<^bsub>S\<^esub> z = h ((r1 \ r2) \ r3)"
      using ring_hom_memE[OF assms] by auto
    also have " ... = h ((r1 \ r3) \ (r2 \ r3))"
      using l_distr[OF r1(1) r2(1) r3(1)] by simp
    also have " ... = (x \\<^bsub>S\<^esub> z) \\<^bsub>S\<^esub> (y \\<^bsub>S\<^esub> z)"
      using ring_hom_memE[OF assms] r1 r2 r3 by auto
    finally show "(x \\<^bsub>S\<^esub> y) \\<^bsub>S\<^esub> z = (x \\<^bsub>S\<^esub> z) \\<^bsub>S\<^esub> (y \\<^bsub>S\<^esub> z)" .

    have "z \\<^bsub>S\<^esub> (x \\<^bsub>S\<^esub> y) = h (r3 \ (r1 \ r2))"
      using ring_hom_memE[OF assms] r1 r2 r3 by auto
    also have " ... = h ((r3 \ r1) \ (r3 \ r2))"
      using r_distr[OF r1(1) r2(1) r3(1)] by simp
    also have " ... = (z \\<^bsub>S\<^esub> x) \\<^bsub>S\<^esub> (z \\<^bsub>S\<^esub> y)"
      using ring_hom_memE[OF assms] r1 r2 r3 by auto
    finally show "z \\<^bsub>S\<^esub> (x \\<^bsub>S\<^esub> y) = (z \\<^bsub>S\<^esub> x) \\<^bsub>S\<^esub> (z \\<^bsub>S\<^esub> y)" .
  qed
qed

lemma (in ring) ring_iso_imp_img_ring:
  assumes "h \ ring_iso R S"
  shows "ring (S \ zero := h \ \)"
proof -
  have "ring (S \ carrier := h ` (carrier R), zero := h \ \)"
    using ring_hom_imp_img_ring[of h S] assms unfolding ring_iso_def by auto
  moreover have "h ` (carrier R) = carrier S"
    using assms unfolding ring_iso_def bij_betw_def by auto
  ultimately show ?thesis by simp
qed

lemma (in cring) ring_iso_imp_img_cring:
  assumes "h \ ring_iso R S"
  shows "cring (S \ zero := h \ \)" (is "cring ?h_img")
proof -
  note m_comm
  interpret h_img?: ring ?h_img
    using ring_iso_imp_img_ring[OF assms] .
  show ?thesis
  proof (unfold_locales)
    fix x y assume "x \ carrier ?h_img" "y \ carrier ?h_img"
    then obtain r1 r2
      where r1: "r1 \ carrier R" "x = h r1"
        and r2: "r2 \ carrier R" "y = h r2"
      using assms image_iff[where ?f = h and ?A = "carrier R"]
      unfolding ring_iso_def bij_betw_def by auto
    have "x \\<^bsub>(?h_img)\<^esub> y = h (r1 \ r2)"
      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
    also have " ... = h (r2 \ r1)"
      using m_comm[OF r1(1) r2(1)] by simp
    also have " ... = y \\<^bsub>(?h_img)\<^esub> x"
      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
    finally show "x \\<^bsub>(?h_img)\<^esub> y = y \\<^bsub>(?h_img)\<^esub> x" .
  qed
qed

lemma (in domain) ring_iso_imp_img_domain:
  assumes "h \ ring_iso R S"
  shows "domain (S \ zero := h \ \)" (is "domain ?h_img")
proof -
  note aux = m_closed integral one_not_zero one_closed zero_closed
  interpret h_img?: cring ?h_img
    using ring_iso_imp_img_cring[OF assms] .
  show ?thesis
  proof (unfold_locales)
    have "\\<^bsub>?h_img\<^esub> = \\<^bsub>?h_img\<^esub> \ h \ = h \"
      using ring_iso_memE(4)[OF assms] by simp
    moreover have "h \ \ h \"
      using ring_iso_memE(5)[OF assms] aux(3-4)
      unfolding bij_betw_def inj_on_def by force
    ultimately show "\\<^bsub>?h_img\<^esub> \ \\<^bsub>?h_img\<^esub>"
      by auto
  next
    fix a b
    assume A: "a \\<^bsub>?h_img\<^esub> b = \\<^bsub>?h_img\<^esub>" "a \ carrier ?h_img" "b \ carrier ?h_img"
    then obtain r1 r2
      where r1: "r1 \ carrier R" "a = h r1"
        and r2: "r2 \ carrier R" "b = h r2"
      using assms image_iff[where ?f = h and ?A = "carrier R"]
      unfolding ring_iso_def bij_betw_def by auto
    hence "a \\<^bsub>?h_img\<^esub> b = h (r1 \ r2)"
      using assms r1 r2 unfolding ring_iso_def ring_hom_def by auto
    hence "h (r1 \ r2) = h \"
      using A(1) by simp
    hence "r1 \ r2 = \"
      using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5)
      unfolding bij_betw_def inj_on_def by force
    hence "r1 = \ \ r2 = \"
      using aux(2)[OF _ r1(1) r2(1)] by simp
    thus "a = \\<^bsub>?h_img\<^esub> \ b = \\<^bsub>?h_img\<^esub>"
      unfolding r1 r2 by auto
  qed
qed

lemma (in field) ring_iso_imp_img_field:
  assumes "h \ ring_iso R S"
  shows "field (S \ zero := h \ \)" (is "field ?h_img")
proof -
  interpret h_img?: domain ?h_img
    using ring_iso_imp_img_domain[OF assms] .
  show ?thesis
  proof (unfold_locales, auto simp add: Units_def)
    interpret field R using field_axioms .
    fix a assume a: "a \ carrier S" "a \\<^bsub>S\<^esub> h \ = \\<^bsub>S\<^esub>"
    then obtain r where r: "r \ carrier R" "a = h r"
      using assms image_iff[where ?f = h and ?A = "carrier R"]
      unfolding ring_iso_def bij_betw_def by auto
    have "a \\<^bsub>S\<^esub> h \ = h (r \ \)" unfolding r(2)
      using ring_iso_memE(2)[OF assms r(1)] by simp
    hence "h \ = h \"
      using ring_iso_memE(4)[OF assms] r(1) a(2) by simp
    thus False
      using ring_iso_memE(5)[OF assms]
      unfolding bij_betw_def inj_on_def by force
  next
    interpret field R using field_axioms .
    fix s assume s: "s \ carrier S" "s \ h \"
    then obtain r where r: "r \ carrier R" "s = h r"
      using assms image_iff[where ?f = h and ?A = "carrier R"]
      unfolding ring_iso_def bij_betw_def by auto
    hence "r \ \" using s(2) by auto
    hence inv_r: "inv r \ carrier R" "inv r \ \" "r \ inv r = \" "inv r \ r = \"
      using field_Units r(1) by auto
    have "h (inv r) \\<^bsub>S\<^esub> h r = h \" and "h r \\<^bsub>S\<^esub> h (inv r) = h \"
      using ring_iso_memE(2)[OF assms inv_r(1) r(1)] inv_r(3-4)
            ring_iso_memE(2)[OF assms r(1) inv_r(1)] by auto
    thus "\s' \ carrier S. s' \\<^bsub>S\<^esub> s = \\<^bsub>S\<^esub> \ s \\<^bsub>S\<^esub> s' = \\<^bsub>S\<^esub>"
      using ring_iso_memE(1,4)[OF assms] inv_r(1) r(2) by auto
  qed
qed

lemma ring_iso_same_card: "R \ S \ card (carrier R) = card (carrier S)"
  using bij_betw_same_card unfolding is_ring_iso_def ring_iso_def by auto
(* ========================================================================== *)

lemma ring_iso_set_refl: "id \ ring_iso R R"
  by (rule ring_iso_memI) (auto)

corollary ring_iso_refl: "R \ R"
  using is_ring_iso_def ring_iso_set_refl by auto

lemma ring_iso_set_trans:
  "\ f \ ring_iso R S; g \ ring_iso S Q \ \ (g \ f) \ ring_iso R Q"
  unfolding ring_iso_def using bij_betw_trans ring_hom_trans by fastforce

corollary ring_iso_trans: "\ R \ S; S \ Q \ \ R \ Q"
  using ring_iso_set_trans unfolding is_ring_iso_def by blast

lemma ring_iso_set_sym:
  assumes "ring R" and h: "h \ ring_iso R S"
  shows "(inv_into (carrier R) h) \ ring_iso S R"
proof -
  have h_hom: "h \ ring_hom R S"
    and h_surj: "h ` (carrier R) = (carrier S)"
    and h_inj: "\x1 x2. \ x1 \ carrier R; x2 \ carrier R \ \ h x1 = h x2 \ x1 = x2"
    using h unfolding ring_iso_def bij_betw_def inj_on_def by auto

  have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
    by (simp add: bij_betw_inv_into h ring_iso_memE(5))

  have "inv_into (carrier R) h \ ring_hom S R"
    using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] \<open>ring R\<close>
    by (simp add: bij_betw_imp_inj_on bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules ring_hom_memI)
  moreover have "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
    using h_inv_bij by force
    ultimately show "inv_into (carrier R) h \ ring_iso S R"
      by (simp add: ring_iso_def)
qed

corollary ring_iso_sym:
  assumes "ring R"
  shows "R \ S \ S \ R"
  using assms ring_iso_set_sym unfolding is_ring_iso_def by auto

lemma (in ring_hom_ring) the_elem_simp [simp]:
  assumes x: "x \ carrier R"
  shows "the_elem (h ` ((a_kernel R S h) +> x)) = h x"
proof -
  from x have "h x \ h ` ((a_kernel R S h) +> x)"
    using homeq_imp_rcos by blast
  thus "the_elem (h ` ((a_kernel R S h) +> x)) = h x"
    by (metis (no_types, lifting) x empty_iff homeq_imp_rcos rcos_imp_homeq the_elem_image_unique)
qed

lemma (in ring_hom_ring) the_elem_inj:
  assumes "X \ carrier (R Quot (a_kernel R S h))"
    and "Y \ carrier (R Quot (a_kernel R S h))"
    and Eq: "the_elem (h ` X) = the_elem (h ` Y)"
  shows "X = Y"
proof -
  from assms obtain x y where x: "x \ carrier R" "X = (a_kernel R S h) +> x"
    and y: "y \ carrier R" "Y = (a_kernel R S h) +> y"
    unfolding FactRing_def A_RCOSETS_def' by auto
  hence "h x = h y" using Eq by simp
  hence "x \ y \ (a_kernel R S h)"
    by (simp add: a_minus_def abelian_subgroup.a_rcos_module_imp
                  abelian_subgroup_a_kernel homeq_imp_rcos x(1) y(1))
  thus "X = Y"
    by (metis R.a_coset_add_inv1 R.minus_eq abelian_subgroup.a_rcos_const
        abelian_subgroup_a_kernel additive_subgroup.a_subset additive_subgroup_a_kernel x y)
qed

lemma (in ring_hom_ring) quot_mem:
  "X \ carrier (R Quot (a_kernel R S h)) \ \x \ carrier R. X = (a_kernel R S h) +> x"
  unfolding FactRing_simps by (simp add: a_r_coset_def)

lemma (in ring_hom_ring) the_elem_wf:
  assumes "X \ carrier (R Quot (a_kernel R S h))"
  shows "\y \ carrier S. (h ` X) = { y }"
proof -
  from assms obtain x where x: "x \ carrier R" and X: "X = (a_kernel R S h) +> x"
    using quot_mem by blast
  have "h x' = h x" if "x' \ X" for x'
  proof -
    from X that have "x' \ (a_kernel R S h) +> x" by simp
    then obtain k where k: "k \ a_kernel R S h" "x' = k \ x"
      by (metis R.add.inv_closed R.add.m_assoc R.l_neg R.r_zero
          abelian_subgroup.a_elemrcos_carrier
          abelian_subgroup.a_rcos_module_imp abelian_subgroup_a_kernel x)
    hence "h x' = h k \\<^bsub>S\<^esub> h x"
      by (meson additive_subgroup.a_Hcarr additive_subgroup_a_kernel hom_add x)
    also have " ... = h x"
      using k by (auto simp add: x)
    finally show "h x' = h x" .
  qed
  moreover have "h x \ h ` X"
    by (simp add: X homeq_imp_rcos x)
  ultimately have "(h ` X) = { h x }"
    by blast
  thus "\y \ carrier S. (h ` X) = { y }" using x by simp
qed

corollary (in ring_hom_ring) the_elem_wf':
  "X \ carrier (R Quot (a_kernel R S h)) \ \r \ carrier R. (h ` X) = { h r }"
  using the_elem_wf by (metis quot_mem the_elem_eq the_elem_simp)

lemma (in ring_hom_ring) the_elem_hom:
  "(\X. the_elem (h ` X)) \ ring_hom (R Quot (a_kernel R S h)) S"
proof (rule ring_hom_memI)
  show "\x. x \ carrier (R Quot a_kernel R S h) \ the_elem (h ` x) \ carrier S"
    using the_elem_wf by fastforce

  show "the_elem (h ` \\<^bsub>R Quot a_kernel R S h\<^esub>) = \\<^bsub>S\<^esub>"
    unfolding FactRing_def  using the_elem_simp[of "\\<^bsub>R\<^esub>"] by simp

  fix X Y
  assume "X \ carrier (R Quot a_kernel R S h)"
     and "Y \ carrier (R Quot a_kernel R S h)"
  then obtain x y where x: "x \ carrier R" "X = (a_kernel R S h) +> x"
                    and y: "y \ carrier R" "Y = (a_kernel R S h) +> y"
    using quot_mem by blast

  have "X \\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \ y)"
    by (simp add: FactRing_def ideal.rcoset_mult_add kernel_is_ideal x y)
  thus "the_elem (h ` (X \\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \\<^bsub>S\<^esub> the_elem (h ` Y)"
    by (simp add: x y)

  have "X \\<^bsub>R Quot a_kernel R S h\<^esub> Y = (a_kernel R S h) +> (x \ y)"
    using ideal.rcos_ring_hom kernel_is_ideal ring_hom_add x y by fastforce
  thus "the_elem (h ` (X \\<^bsub>R Quot a_kernel R S h\<^esub> Y)) = the_elem (h ` X) \\<^bsub>S\<^esub> the_elem (h ` Y)"
    by (simp add: x y)
qed

lemma (in ring_hom_ring) the_elem_surj:
  "(\X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h)) = (h ` (carrier R))"
proof
  show "(\X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h) \ h ` carrier R"
    using the_elem_wf' by fastforce
  show "h ` carrier R \ (\X. the_elem (h ` X)) ` carrier (R Quot a_kernel R S h)"
  proof
    fix y assume "y \ h ` carrier R"
    then obtain x where x: "x \ carrier R" "h x = y"
      by (metis image_iff)
    hence "the_elem (h ` ((a_kernel R S h) +> x)) = y" by simp
    moreover have "(a_kernel R S h) +> x \ carrier (R Quot (a_kernel R S h))"
     unfolding FactRing_simps by (auto simp add: x a_r_coset_def)
    ultimately show "y \ (\X. (the_elem (h ` X))) ` carrier (R Quot (a_kernel R S h))" by blast
  qed
qed

proposition (in ring_hom_ring) FactRing_iso_set_aux:
  "(\X. the_elem (h ` X)) \ ring_iso (R Quot (a_kernel R S h)) (S \ carrier := h ` (carrier R) \)"
proof -
  have *: "bij_betw (\X. the_elem (h ` X)) (carrier (R Quot a_kernel R S h)) (h ` (carrier R))"
    unfolding bij_betw_def inj_on_def using the_elem_surj the_elem_inj by simp
  have "(\X. the_elem (h ` X)): carrier (R Quot (a_kernel R S h)) \ h ` (carrier R)"
    using the_elem_wf' by fastforce
  hence "(\X. the_elem (h ` X)) \ ring_hom (R Quot (a_kernel R S h)) (S \ carrier := h ` (carrier R) \)"
    using the_elem_hom the_elem_wf' unfolding ring_hom_def by simp
  with * show ?thesis unfolding ring_iso_def using the_elem_hom by simp
qed

theorem (in ring_hom_ring) FactRing_iso_set:
  assumes "h ` carrier R = carrier S"
  shows "(\X. the_elem (h ` X)) \ ring_iso (R Quot (a_kernel R S h)) S"
  using FactRing_iso_set_aux assms by auto

corollary (in ring_hom_ring) FactRing_iso:
  assumes "h ` carrier R = carrier S"
  shows "R Quot (a_kernel R S h) \ S"
  using FactRing_iso_set assms is_ring_iso_def by auto

corollary (in ring) FactRing_zeroideal:
  shows "R Quot { \ } \ R" and "R \ R Quot { \ }"
proof -
  have "ring_hom_ring R R id"
    using ring_axioms by (auto intro: ring_hom_ringI)
  moreover have "a_kernel R R id = { \ }"
    unfolding a_kernel_def' by auto
  ultimately show "R Quot { \ } \ R" and "R \ R Quot { \ }"
    using ring_hom_ring.FactRing_iso[of R R id]
          ring_iso_sym[OF ideal.quotient_is_ring[OF zeroideal], of R] by auto
qed

lemma (in ring_hom_ring) img_is_ring: "ring (S \ carrier := h ` (carrier R) \)"
proof -
  let ?the_elem = "\X. the_elem (h ` X)"
  have FactRing_is_ring: "ring (R Quot (a_kernel R S h))"
    by (simp add: ideal.quotient_is_ring kernel_is_ideal)
  have "ring ((S \ carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \)
                 \<lparr>    zero := ?the_elem \<zero>\<^bsub>(R Quot (a_kernel R S h))\<^esub> \<rparr>)"
    using ring.ring_iso_imp_img_ring[OF FactRing_is_ring, of ?the_elem
          "S \ carrier := ?the_elem ` (carrier (R Quot (a_kernel R S h))) \"]
          FactRing_iso_set_aux the_elem_surj by auto

  moreover
  have "\ \ (a_kernel R S h)"
    using a_kernel_def'[of R S h] by auto
  hence "\ \ (a_kernel R S h) +> \"
    using a_r_coset_def'[of R "a_kernel R S h" \] by force
  hence "\\<^bsub>S\<^esub> \ (h ` ((a_kernel R S h) +> \))"
    using hom_one by force
  hence "?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \\<^bsub>S\<^esub>"
    using the_elem_wf[of "(a_kernel R S h) +> \"] by (simp add: FactRing_def)

  moreover
  have "\\<^bsub>S\<^esub> \ (h ` (a_kernel R S h))"
    using a_kernel_def'[of R S h] hom_zero by force
  hence "\\<^bsub>S\<^esub> \ (h ` \\<^bsub>(R Quot (a_kernel R S h))\<^esub>)"
    by (simp add: FactRing_def)
  hence "?the_elem \\<^bsub>(R Quot (a_kernel R S h))\<^esub> = \\<^bsub>S\<^esub>"
    using the_elem_wf[OF ring.ring_simprules(2)[OF FactRing_is_ring]]
    by (metis singletonD the_elem_eq)

  ultimately
  have "ring ((S \ carrier := h ` (carrier R) \) \ one := \\<^bsub>S\<^esub>, zero := \\<^bsub>S\<^esub> \)"
    using the_elem_surj by simp
  thus ?thesis
    by auto
qed

lemma (in ring_hom_ring) img_is_cring:
  assumes "cring S"
  shows "cring (S \ carrier := h ` (carrier R) \)"
proof -
  interpret ring "S \ carrier := h ` (carrier R) \"
    using img_is_ring .
  show ?thesis
    by unfold_locales (use assms in \<open>auto simp: cring_def comm_monoid_def comm_monoid_axioms_def\<close>)
qed

lemma (in ring_hom_ring) img_is_domain:
  assumes "domain S"
  shows "domain (S \ carrier := h ` (carrier R) \)"
proof -
  interpret cring "S \ carrier := h ` (carrier R) \"
    using img_is_cring assms unfolding domain_def by simp
  show ?thesis
    apply unfold_locales
    using assms unfolding domain_def domain_axioms_def apply auto
    using hom_closed by blast
qed

proposition (in ring_hom_ring) primeideal_vimage:
  assumes R: "cring R"
    and A: "primeideal P S"
  shows "primeideal { r \ carrier R. h r \ P } R"
proof -
  from A have is_ideal: "ideal P S" unfolding primeideal_def by simp
  have "ring_hom_ring R (S Quot P) (((+>\<^bsub>S\<^esub>) P) \ h)" (is "ring_hom_ring ?A ?B ?h")
    using ring_hom_trans[OF homh, of "(+>\<^bsub>S\<^esub>) P" "S Quot P"]
          ideal.rcos_ring_hom_ring[OF is_ideal] R
    unfolding ring_hom_ring_def ring_hom_ring_axioms_def cring_def by simp
  then interpret hom: ring_hom_ring R "S Quot P" "((+>\<^bsub>S\<^esub>) P) \ h" by simp

  have "inj_on (\X. the_elem (?h ` X)) (carrier (R Quot (a_kernel R (S Quot P) ?h)))"
    using hom.the_elem_inj unfolding inj_on_def by simp
  moreover
  have "ideal (a_kernel R (S Quot P) ?h) R"
    using hom.kernel_is_ideal by auto
  have hom': "ring_hom_ring (R Quot (a_kernel R (S Quot P) ?h)) (S Quot P) (\X. the_elem (?h ` X))"
    using hom.the_elem_hom hom.kernel_is_ideal
    by (meson hom.ring_hom_ring_axioms ideal.rcos_ring_hom_ring ring_hom_ring_axioms_def ring_hom_ring_def)

  ultimately
  have "primeideal (a_kernel R (S Quot P) ?h) R"
    using ring_hom_ring.inj_on_domain[OF hom'] primeideal.quotient_is_domain[OF A]
          cring.quot_domain_imp_primeideal[OF R hom.kernel_is_ideal] by simp

  moreover have "a_kernel R (S Quot P) ?h = { r \ carrier R. h r \ P }"
  proof
    show "a_kernel R (S Quot P) ?h \ { r \ carrier R. h r \ P }"
    proof
      fix r assume "r \ a_kernel R (S Quot P) ?h"
      hence r: "r \ carrier R" "P +>\<^bsub>S\<^esub> (h r) = P"
        unfolding a_kernel_def kernel_def FactRing_def by auto
      hence "h r \ P"
        using S.a_rcosI R.l_zero S.l_zero additive_subgroup.a_subset[OF ideal.axioms(1)[OF is_ideal]]
              additive_subgroup.zero_closed[OF ideal.axioms(1)[OF is_ideal]] hom_closed by metis
      thus "r \ { r \ carrier R. h r \ P }" using r by simp
    qed
  next
    show "{ r \ carrier R. h r \ P } \ a_kernel R (S Quot P) ?h"
    proof
      fix r assume "r \ { r \ carrier R. h r \ P }"
      hence r: "r \ carrier R" "h r \ P" by simp_all
      hence "?h r = P"
        by (simp add: S.a_coset_join2 additive_subgroup.a_subgroup ideal.axioms(1) is_ideal)
      thus "r \ a_kernel R (S Quot P) ?h"
        unfolding a_kernel_def kernel_def FactRing_def using r(1) by auto
    qed
  qed
  ultimately show "primeideal { r \ carrier R. h r \ P } R" by simp
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.