Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Chinese_Remainder.thy Sprache: Isabelle

Original von: Isabelle^©

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

theory Chinese_Remainder
  imports Weak_Morphisms Ideal_Product

begin

section \<open>Direct Product of Rings\<close>

subsection \<open>Definitions\<close>

definition RDirProd :: "('a, 'n) ring_scheme \ ('b, 'm) ring_scheme \ ('a \ 'b) ring"
  where "RDirProd R S = monoid.extend (R \\ S)
           \<lparr> zero = one ((add_monoid R) \<times>\<times> (add_monoid S)),
              add = mult ((add_monoid R) \<times>\<times> (add_monoid S)) \<rparr> "

abbreviation nil_ring :: "('a list) ring"
  where "nil_ring \ monoid.extend nil_monoid \ zero = [], add = (\a b. []) \"

definition RDirProd_list :: "(('a, 'n) ring_scheme) list \ ('a list) ring"
  where "RDirProd_list Rs = foldr (\R S. image_ring (\(a, as). a # as) (RDirProd R S)) Rs nil_ring"

subsection \<open>Basic Properties\<close>

lemma RDirProd_carrier: "carrier (RDirProd R S) = carrier R \ carrier S"
  unfolding RDirProd_def DirProd_def by (simp add: monoid.defs)

lemma RDirProd_add_monoid [simp]: "add_monoid (RDirProd R S) = (add_monoid R) \\ (add_monoid S)"
  by (simp add: RDirProd_def monoid.defs)

lemma RDirProd_ring:
  assumes "ring R" and "ring S" shows "ring (RDirProd R S)"
proof -
  have "monoid (RDirProd R S)"
    using DirProd_monoid[OF assms[THEN ring.axioms(2)]] unfolding monoid_def
    by (auto simp add: DirProd_def RDirProd_def monoid.defs)
  then interpret Prod: group "add_monoid (RDirProd R S)" + monoid "RDirProd R S"
    using DirProd_group[OF assms[THEN abelian_group.a_group[OF ring.is_abelian_group]]]
    unfolding RDirProd_add_monoid by auto
  show ?thesis
    by (unfold_locales, auto simp add: RDirProd_def DirProd_def monoid.defs assms ring.ring_simprules)
qed

lemma RDirProd_iso1:
  "(\(x, y). (y, x)) \ ring_iso (RDirProd R S) (RDirProd S R)"
  unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
  by (auto simp add: RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_iso2:
  "(\(x, (y, z)). ((x, y), z)) \ ring_iso (RDirProd R (RDirProd S T)) (RDirProd (RDirProd R S) T)"
  unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
  by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_iso3:
  "(\((x, y), z). (x, (y, z))) \ ring_iso (RDirProd (RDirProd R S) T) (RDirProd R (RDirProd S T))"
  unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
  by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_iso4:
  assumes "f \ ring_iso R S" shows "(\(r, t). (f r, t)) \ ring_iso (RDirProd R T) (RDirProd S T)"
  using assms unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
  by (auto simp add: image_iff RDirProd_def DirProd_def monoid.defs)+

lemma RDirProd_iso5:
  assumes "f \ ring_iso S T" shows "(\(r, s). (r, f s)) \ ring_iso (RDirProd R S) (RDirProd R T)"
  using ring_iso_set_trans[OF ring_iso_set_trans[OF RDirProd_iso1 RDirProd_iso4[OF assms]] RDirProd_iso1]
  by (simp add: case_prod_unfold comp_def)

lemma RDirProd_iso6:
  assumes "f \ ring_iso R R'" and "g \ ring_iso S S'"
  shows "(\(r, s). (f r, g s)) \ ring_iso (RDirProd R S) (RDirProd R' S')"
  using ring_iso_set_trans[OF RDirProd_iso4[OF assms(1)] RDirProd_iso5[OF assms(2)]]
  by (simp add: case_prod_beta' comp_def)

lemma RDirProd_iso7:
  shows "(\a. (a, [])) \ ring_iso R (RDirProd R nil_ring)"
  unfolding ring_iso_def ring_hom_def bij_betw_def inj_on_def
  by (auto simp add: RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_hom1:
  shows "(\a. (a, a)) \ ring_hom R (RDirProd R R)"
  by (auto simp add: ring_hom_def RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_hom2:
  assumes "f \ ring_hom S T"
  shows "(\(x, y). (x, f y)) \ ring_hom (RDirProd R S) (RDirProd R T)"
    and "(\(x, y). (f x, y)) \ ring_hom (RDirProd S R) (RDirProd T R)"
  using assms by (auto simp add: ring_hom_def RDirProd_def DirProd_def monoid.defs)

lemma RDirProd_hom3:
  assumes "f \ ring_hom R R'" and "g \ ring_hom S S'"
  shows "(\(r, s). (f r, g s)) \ ring_hom (RDirProd R S) (RDirProd R' S')"
  using ring_hom_trans[OF RDirProd_hom2(2)[OF assms(1)] RDirProd_hom2(1)[OF assms(2)]]
  by (simp add: case_prod_beta' comp_def)

subsection \<open>Direct Product of a List of Rings\<close>

lemma RDirProd_list_nil [simp]: "RDirProd_list [] = nil_ring"
  unfolding RDirProd_list_def by simp

lemma nil_ring_simprules [simp]:
  "carrier nil_ring = { [] }" and "one nil_ring = []" and "zero nil_ring = []"
  by (auto simp add: monoid.defs)

lemma RDirProd_list_truncate:
  shows "monoid.truncate (RDirProd_list Rs) = DirProd_list Rs"
proof (induct Rs, simp add: RDirProd_list_def DirProd_list_def monoid.defs)
  case (Cons R Rs)
  have "monoid.truncate (RDirProd_list (R # Rs)) =
        monoid.truncate (image_ring (\<lambda>(a, as). a # as) (RDirProd R (RDirProd_list Rs)))"
    unfolding RDirProd_list_def by simp
  also have " ... = image_group (\(a, as). a # as) (monoid.truncate (RDirProd R (RDirProd_list Rs)))"
  by (simp add: image_ring_def image_group_def monoid.defs)
  also have " ... = image_group (\(a, as). a # as) (R \\ (monoid.truncate (RDirProd_list Rs)))"
    by (simp add: RDirProd_def DirProd_def monoid.defs)
  also have " ... = DirProd_list (R # Rs)"
    unfolding Cons DirProd_list_def by simp
  finally show ?case .
qed

lemma RDirProd_list_carrier_def':
  shows "carrier (RDirProd_list Rs) = carrier (DirProd_list Rs)"
proof -
  have "carrier (RDirProd_list Rs) = carrier (monoid.truncate (RDirProd_list Rs))"
    by (simp add: monoid.defs)
  thus ?thesis
    unfolding RDirProd_list_truncate .
qed

lemma RDirProd_list_carrier:
  shows "carrier (RDirProd_list (G # Gs)) = (\(x, xs). x # xs) ` (carrier G \ carrier (RDirProd_list Gs))"
  unfolding RDirProd_list_carrier_def' using DirProd_list_carrier .

lemma RDirProd_list_one:
  shows "one (RDirProd_list Rs) = foldr (\R tl. (one R) # tl) Rs []"
  unfolding RDirProd_list_def RDirProd_def image_ring_def image_group_def
  by (induct Rs) (auto simp add: monoid.defs)

lemma RDirProd_list_zero:
  shows "zero (RDirProd_list Rs) = foldr (\R tl. (zero R) # tl) Rs []"
  unfolding RDirProd_list_def RDirProd_def image_ring_def
  by (induct Rs) (auto simp add: monoid.defs)

lemma RDirProd_list_zero':
  shows "zero (RDirProd_list (R # Rs)) = (zero R) # (zero (RDirProd_list Rs))"
  unfolding RDirProd_list_zero by simp

lemma RDirProd_list_carrier_mem:
  assumes "as \ carrier (RDirProd_list Rs)"
  shows "length as = length Rs" and "\i. i < length Rs \ (as ! i) \ carrier (Rs ! i)"
  using assms DirProd_list_carrier_mem unfolding RDirProd_list_carrier_def' by auto

lemma RDirProd_list_carrier_memI:
  assumes "length as = length Rs" and "\i. i < length Rs \ (as ! i) \ carrier (Rs ! i)"
  shows "as \ carrier (RDirProd_list Rs)"
  using assms DirProd_list_carrier_memI unfolding RDirProd_list_carrier_def' by auto

lemma inj_on_RDirProd_carrier:
  shows "inj_on (\(a, as). a # as) (carrier (RDirProd R (RDirProd_list Rs)))"
  unfolding RDirProd_def DirProd_def inj_on_def by auto

lemma RDirProd_list_is_ring:
  assumes "\i. i < length Rs \ ring (Rs ! i)" shows "ring (RDirProd_list Rs)"
  using assms
proof (induct Rs)
  case Nil thus ?case
    unfolding RDirProd_list_def by (unfold_locales, auto simp add: monoid.defs Units_def)
next
  case (Cons R Rs)
  hence is_ring: "ring (RDirProd R (RDirProd_list Rs))"
    using RDirProd_ring[of R "RDirProd_list Rs"] by force
  show ?case
    using ring.inj_imp_image_ring_is_ring[OF is_ring inj_on_RDirProd_carrier]
    unfolding RDirProd_list_def by auto
qed

lemma RDirProd_list_iso1:
  "(\(a, as). a # as) \ ring_iso (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))"
  using inj_imp_image_ring_iso[OF inj_on_RDirProd_carrier] unfolding RDirProd_list_def by auto

lemma RDirProd_list_iso2:
  "Hilbert_Choice.inv (\(a, as). a # as) \ ring_iso (RDirProd_list (R # Rs)) (RDirProd R (RDirProd_list Rs))"
  unfolding RDirProd_list_def by (auto intro: inj_imp_image_ring_inv_iso simp add: inj_def)

lemma RDirProd_list_iso3:
  "(\a. [ a ]) \ ring_iso R (RDirProd_list [ R ])"
proof -
  have [simp]: "(\a. [ a ]) = (\(a, as). a # as) \ (\a. (a, []))" by auto
  show ?thesis
    using ring_iso_set_trans[OF RDirProd_iso7] RDirProd_list_iso1[of R "[]"]
    unfolding RDirProd_list_def by simp
qed

lemma RDirProd_list_hom1:
  "(\(a, as). a # as) \ ring_hom (RDirProd R (RDirProd_list Rs)) (RDirProd_list (R # Rs))"
  using RDirProd_list_iso1 unfolding ring_iso_def by auto

lemma RDirProd_list_hom2:
  assumes "f \ ring_hom R S" shows "(\a. [ f a ]) \ ring_hom R (RDirProd_list [ S ])"
proof -
  have hom1: "(\a. (a, [])) \ ring_hom R (RDirProd R nil_ring)"
    using RDirProd_iso7 unfolding ring_iso_def by auto
  have hom2: "(\(a, as). a # as) \ ring_hom (RDirProd S nil_ring) (RDirProd_list [ S ])"
    using RDirProd_list_hom1[of _ "[]"] unfolding RDirProd_list_def by auto
  have [simp]: "(\(a, as). a # as) \ ((\(x, y). (f x, y)) \ (\a. (a, []))) = (\a. [ f a ])" by auto
  show ?thesis
    using ring_hom_trans[OF ring_hom_trans[OF hom1 RDirProd_hom2(2)[OF assms]] hom2] by simp
qed

section \<open>Chinese Remainder Theorem\<close>

subsection \<open>Definitions\<close>

abbreviation (in ring) canonical_proj :: "'a set \ 'a set \ 'a \ 'a set \ 'a set"
  where "canonical_proj I J \ (\a. (I +> a, J +> a))"

definition (in ring) canonical_proj_ext :: "(nat \ 'a set) \ nat \ 'a \ ('a set) list"
  where "canonical_proj_ext I n = (\a. map (\i. (I i) +> a) [0..< Suc n])"

subsection \<open>Chinese Remainder Simple\<close>

lemma (in ring) canonical_proj_is_surj:
  assumes "ideal I R" "ideal J R" and "I <+> J = carrier R"
  shows "(canonical_proj I J) ` carrier R = carrier (RDirProd (R Quot I) (R Quot J))"
  unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
proof (auto simp add: monoid.defs)
  { fix I i assume "ideal I R" "i \ I" hence "I +> i = \\<^bsub>R Quot I\<^esub>"
      using a_rcos_zero by (simp add: FactRing_def)
  } note aux_lemma1 = this

  { fix I i j assume A: "ideal I R" "i \ I" "j \ carrier R" "i \ j = \"
    have "(I +> i) \\<^bsub>R Quot I\<^esub> (I +> j) = I +> \"
      using ring_hom_memE(3)[OF ideal.rcos_ring_hom ideal.Icarr[OF _ A(2)] A(3)] A(1,4) by simp
    moreover have "I +> i = I"
      using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group]
      by (simp add: A(1-2) abelian_subgroup.a_rcos_const)
    moreover have "I +> j \ carrier (R Quot I)" and "I = \\<^bsub>R Quot I\<^esub>" and "I +> \ = \\<^bsub>R Quot I\<^esub>"
      by (auto simp add: FactRing_def A_RCOSETS_def' A(3))
    ultimately have "I +> j = \\<^bsub>R Quot I\<^esub>"
      using ring.ring_simprules(8)[OF ideal.quotient_is_ring[OF A(1)]] by simp
  } note aux_lemma2 = this

  interpret I: ring "R Quot I" + J: ring "R Quot J"
    using assms(1-2)[THEN ideal.quotient_is_ring] by auto

  fix a b assume a: "a \ carrier R" and b: "b \ carrier R"
  have "\ \ I <+> J"
    using assms(3) by blast
  then obtain i j where i: "i \ carrier R" "i \ I" and j: "j \ carrier R" "j \ J" and ij: "i \ j = \"
    using assms(1-2)[THEN ideal.Icarr] unfolding set_add_def' by auto
  hence rcos_j: "I +> j = \\<^bsub>R Quot I\<^esub>" and rcos_i: "J +> i = \\<^bsub>R Quot J\<^esub>"
    using assms(1-2)[THEN aux_lemma2] a_comm by simp+

  define s where "s = (a \ j) \ (b \ i)"
  hence "s \ carrier R"
    using a b i j by simp

  have "I +> s = ((I +> a) \\<^bsub>R Quot I\<^esub> (I +> j)) \\<^bsub>R Quot I\<^esub> (I +> (b \ i))"
    using ring_hom_memE(2-3)[OF ideal.rcos_ring_hom[OF assms(1)]]
    by (simp add: a b i(1) j(1) s_def)
  moreover have "I +> a \ carrier (R Quot I)"
    by (auto simp add: FactRing_def A_RCOSETS_def' a)
  ultimately have "I +> s = I +> a"
    unfolding rcos_j aux_lemma1[OF assms(1) ideal.I_l_closed[OF assms(1) i(2) b]] by simp

  have "J +> s = (J +> (a \ j)) \\<^bsub>R Quot J\<^esub> ((J +> b) \\<^bsub>R Quot J\<^esub> (J +> i))"
    using ring_hom_memE(2-3)[OF ideal.rcos_ring_hom[OF assms(2)]]
    by (simp add: a b i(1) j(1) s_def)
  moreover have "J +> b \ carrier (R Quot J)"
    by (auto simp add: FactRing_def A_RCOSETS_def' b)
  ultimately have "J +> s = J +> b"
    unfolding rcos_i aux_lemma1[OF assms(2) ideal.I_l_closed[OF assms(2) j(2) a]] by simp

  from \<open>I +> s = I +> a\<close> and \<open>J +> s = J +> b\<close> and \<open>s \<in> carrier R\<close>
  show "(I +> a, J +> b) \ (canonical_proj I J) ` carrier R" by blast
qed

lemma (in ring) canonical_proj_ker:
  assumes "ideal I R" and "ideal J R"
  shows "a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J) = I \ J"
proof
  show "a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J) \ I \ J"
    unfolding FactRing_def RDirProd_def DirProd_def a_kernel_def'
    by (auto simp add: assms[THEN ideal.rcos_const_imp_mem] monoid.defs)
next
  show "I \ J \ a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
  proof
    fix s assume s: "s \ I \ J" then have "I +> s = I" and "J +> s = J"
      using abelian_subgroupI3[OF ideal.axioms(1) is_abelian_group]
      by (simp add: abelian_subgroup.a_rcos_const assms)+
    thus "s \ a_kernel R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
      unfolding FactRing_def RDirProd_def DirProd_def a_kernel_def'
      using ideal.Icarr[OF assms(1)] s by (simp add: monoid.defs)
  qed
qed

lemma (in ring) canonical_proj_is_hom:
  assumes "ideal I R" and "ideal J R"
  shows "(canonical_proj I J) \ ring_hom R (RDirProd (R Quot I) (R Quot J))"
  unfolding RDirProd_def DirProd_def FactRing_def A_RCOSETS_def'
  by (auto intro!: ring_hom_memI
         simp add: assms[THEN ideal.rcoset_mult_add]
                   assms[THEN ideal.a_rcos_sum] monoid.defs)

lemma (in ring) canonical_proj_ring_hom:
  assumes "ideal I R" and "ideal J R"
  shows "ring_hom_ring R (RDirProd (R Quot I) (R Quot J)) (canonical_proj I J)"
  using ring_hom_ring.intro[OF ring_axioms RDirProd_ring[OF assms[THEN ideal.quotient_is_ring]]]
  by (simp add: ring_hom_ring_axioms_def canonical_proj_is_hom[OF assms])

theorem (in ring) chinese_remainder_simple:
  assumes "ideal I R" "ideal J R" and "I <+> J = carrier R"
  shows "R Quot (I \ J) \ RDirProd (R Quot I) (R Quot J)"
  using ring_hom_ring.FactRing_iso[OF canonical_proj_ring_hom canonical_proj_is_surj]
  by (simp add: canonical_proj_ker assms)

subsection \<open>Chinese Remainder Generalized\<close>

lemma (in ring) canonical_proj_ext_zero [simp]: "(canonical_proj_ext I 0) = (\a. [ (I 0) +> a ])"
  unfolding canonical_proj_ext_def by simp

lemma (in ring) canonical_proj_ext_tl:
  "(\a. canonical_proj_ext I (Suc n) a) = (\a. ((I 0) +> a) # (canonical_proj_ext (\i. I (Suc i)) n a))"
  unfolding canonical_proj_ext_def by (induct n) (auto, metis (lifting) append.assoc append_Cons append_Nil)

lemma (in ring) canonical_proj_ext_is_hom:
  assumes "\i. i \ n \ ideal (I i) R"
  shows "(canonical_proj_ext I n) \ ring_hom R (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n]))"
  using assms
proof (induct n arbitrary: I)
  case 0 thus ?case
    using RDirProd_list_hom2[OF ideal.rcos_ring_hom[of _ R]] by (simp add: canonical_proj_ext_def)
next
  let ?DirProd = "\I n. RDirProd_list (map (\i. R Quot (I i)) [0..
  let ?proj = "\I n. canonical_proj_ext I n"

  case (Suc n)
  hence I: "ideal (I 0) R" by simp
  have hom: "(?proj (\i. I (Suc i)) n) \ ring_hom R (?DirProd (\i. I (Suc i)) n)"
    using Suc(1)[of "\i. I (Suc i)"] Suc(2) by simp
  have [simp]:
    "(\(a, as). a # as) \ ((\(r, s). (I 0 +> r, ?proj (\i. I (Suc i)) n s)) \ (\a. (a, a))) = ?proj I (Suc n)"
    unfolding canonical_proj_ext_tl by auto
  moreover have
    "(R Quot I 0) # (map (\i. R Quot I (Suc i)) [0..< Suc n]) = map (\i. R Quot (I i)) [0..< Suc (Suc n)]"
    by (induct n) (auto)
  moreover show ?case
    using ring_hom_trans[OF ring_hom_trans[OF RDirProd_hom1
          RDirProd_hom3[OF ideal.rcos_ring_hom[OF I] hom]] RDirProd_list_hom1]
    unfolding calculation(2) by simp
qed

lemma (in ring) RDirProd_Quot_list_is_ring:
  assumes "\i. i \ n \ ideal (I i) R" shows "ring (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n]))"
proof -
  have ring_list: "\i. i < Suc n \ ring ((map (\i. R Quot I i) [0..< Suc n]) ! i)"
    using ideal.quotient_is_ring[OF assms]
    by (metis add.left_neutral diff_zero le_simps(2) nth_map_upt)
  show ?thesis
    using RDirProd_list_is_ring[OF ring_list] by simp
qed

lemma (in ring) canonical_proj_ext_ring_hom:
  assumes "\i. i \ n \ ideal (I i) R"
  shows "ring_hom_ring R (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n])) (canonical_proj_ext I n)"
proof -
  have ring: "ring (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n]))"
    using RDirProd_Quot_list_is_ring[OF assms] by simp
  show ?thesis
    using canonical_proj_ext_is_hom assms ring_hom_ring.intro[OF ring_axioms ring]
    unfolding ring_hom_ring_axioms_def by blast
qed

lemma (in ring) canonical_proj_ext_ker:
  assumes "\i. i \ (n :: nat) \ ideal (I i) R"
  shows "a_kernel R (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n])) (canonical_proj_ext I n) = (\i \ n. I i)"
proof -
  let ?map_Quot = "\I n. map (\i. R Quot (I i)) [0..< Suc n]"
  let ?ker = "\I n. a_kernel R (RDirProd_list (?map_Quot I n)) (canonical_proj_ext I n)"

  from assms show ?thesis
  proof (induct n arbitrary: I)
    case 0 then have I: "ideal (I 0) R" by simp
    show ?case
      unfolding a_kernel_def' RDirProd_list_zero canonical_proj_ext_def FactRing_def
      using ideal.rcos_const_imp_mem a_rcos_zero ideal.Icarr I by auto
  next
    case (Suc n)
    hence I: "ideal (I 0) R" by simp
    have map_simp: "?map_Quot I (Suc n) = (R Quot I 0) # (?map_Quot (\i. I (Suc i)) n)"
      by (induct n) (auto)
    have ker_I0: "I 0 = a_kernel R (R Quot (I 0)) (\a. (I 0) +> a)"
      using ideal.rcos_const_imp_mem[OF I] a_rcos_zero[OF I] ideal.Icarr[OF I]
      unfolding a_kernel_def' FactRing_def by auto
    hence "?ker I (Suc n) = (?ker (\i. I (Suc i)) n) \ (I 0)"
      unfolding a_kernel_def' map_simp RDirProd_list_zero' canonical_proj_ext_tl by auto
    moreover have "?ker (\i. I (Suc i)) n = (\i \ n. I (Suc i))"
      using Suc(1)[of "\i. I (Suc i)"] Suc(2) by auto
    ultimately show ?case
      by (auto simp add: INT_extend_simps(10) atMost_atLeast0)
         (metis atLeastAtMost_iff le_zero_eq not_less_eq_eq)
  qed
qed

lemma (in cring) canonical_proj_ext_is_surj:
  assumes "\i. i \ n \ ideal (I i) R" and "\i j. \ i \ n; j \ n \ \ i \ j \ I i <+> I j = carrier R"
  shows "(canonical_proj_ext I n) ` carrier R = carrier (RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n]))"
  using assms
proof (induct n arbitrary: I)
  case 0 show ?case
    by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
next
  { fix S :: "'c ring" and T :: "'d ring" and f g
    assume A: "ring T" "f \ ring_hom R S" "g \ ring_hom R T" "f ` carrier R \ f ` (a_kernel R T g)"
    have "(\a. (f a, g a)) ` carrier R = (f ` carrier R) \ (g ` carrier R)"
    proof
      show "(\a. (f a, g a)) ` carrier R \ (f ` carrier R) \ (g ` carrier R)"
        by blast
    next
      show "(f ` carrier R) \ (g ` carrier R) \ (\a. (f a, g a)) ` carrier R"
      proof
        fix t assume "t \ (f ` carrier R) \ (g ` carrier R)"
        then obtain a b where a: "a \ carrier R" "f a = fst t" and b: "b \ carrier R" "g b = snd t"
          by auto
        obtain c where c: "c \ a_kernel R T g" "f c = f (a \ b)"
          using A(4) minus_closed[OF a(1) b (1)] by auto
        have "f (c \ b) = f (a \ b) \\<^bsub>S\<^esub> f b"
          using ring_hom_memE(3)[OF A(2)] b c unfolding a_kernel_def' by auto
        hence "f (c \ b) = f a"
          using ring_hom_memE(3)[OF A(2) minus_closed[of a b], of b] a b by algebra
        moreover have "g (c \ b) = g b"
          using ring_hom_memE(1,3)[OF A(3)] b(1) c ring.ring_simprules(8)[OF A(1)]
          unfolding a_kernel_def' by auto
        ultimately have "(\a. (f a, g a)) (c \ b) = t" and "c \ b \ carrier R"
          using a b c unfolding a_kernel_def' by auto
        thus "t \ (\a. (f a, g a)) ` carrier R"
          by blast
      qed
    qed } note aux_lemma = this

  let ?map_Quot = "\I n. map (\i. R Quot (I i)) [0..< Suc n]"
  let ?DirProd = "\I n. RDirProd_list (?map_Quot I n)"
  let ?proj = "\I n. canonical_proj_ext I n"

  case (Suc n)
  interpret I: ideal "I 0" R + Inter: ideal "\i \ n. I (Suc i)" R
    using i_Intersect[of "(\i. I (Suc i)) ` {..n}"] Suc(2) by auto

  have map_simp: "?map_Quot I (Suc n) = (R Quot I 0) # (?map_Quot (\i. I (Suc i)) n)"
    by (induct n) (auto)

  have IH: "(?proj (\i. I (Suc i)) n) ` carrier R = carrier (?DirProd (\i. I (Suc i)) n)"
   and ring: "ring (?DirProd (\i. I (Suc i)) n)"
   and hom: "?proj (\i. I (Suc i)) n \ ring_hom R (?DirProd (\i. I (Suc i)) n)"
    using RDirProd_Quot_list_is_ring[of n "\i. I (Suc i)"] Suc(1)[of "\i. I (Suc i)"]
           canonical_proj_ext_is_hom[of n "\i. I (Suc i)"] Suc(2-3) by auto

  have ker: "a_kernel R (?DirProd (\i. I (Suc i)) n) (?proj (\i. I (Suc i)) n) = (\i \ n. I (Suc i))"
    using canonical_proj_ext_ker[of n "\i. I (Suc i)"] Suc(2) by auto
  have carrier_Quot: "carrier (R Quot (I 0)) = (\a. (I 0) +> a) ` carrier R"
    by (auto simp add: RDirProd_list_carrier FactRing_def A_RCOSETS_def')
  have ring: "ring (?DirProd (\i. I (Suc i)) n)"
   and hom: "?proj (\i. I (Suc i)) n \ ring_hom R (?DirProd (\i. I (Suc i)) n)"
    using RDirProd_Quot_list_is_ring[of n "\i. I (Suc i)"]
          canonical_proj_ext_is_hom[of n "\i. I (Suc i)"] Suc(2) by auto
  have "carrier (R Quot (I 0)) \ (\a. (I 0) +> a) ` (\i \ n. I (Suc i))"
  proof
    have "(\i \ {Suc 0.. Suc n}. I i) <+> (I 0) = carrier R"
      using inter_plus_ideal_eq_carrier_arbitrary[of n I 0]
      by (simp add: Suc(2-3) atLeast1_atMost_eq_remove0)
    hence eq_carrier: "(I 0) <+> (\i \ n. I (Suc i)) = carrier R"
      using set_add_comm[OF I.a_subset Inter.a_subset]
      by (metis INT_extend_simps(10) atMost_atLeast0 image_Suc_atLeastAtMost)

    fix b assume "b \ carrier (R Quot (I 0))"
    hence "(b, (\i \ n. I (Suc i))) \ carrier (R Quot I 0) \ carrier (R Quot (\i\n. I (Suc i)))"
      using ring.ring_simprules(2)[OF Inter.quotient_is_ring] by (simp add: FactRing_def)
    then obtain s
      where "s \ carrier R" "(canonical_proj (I 0) (\i \ n. I (Suc i))) s = (b, (\i \ n. I (Suc i)))"
      using canonical_proj_is_surj[OF I.is_ideal Inter.is_ideal eq_carrier]
      unfolding RDirProd_carrier by (metis (no_types, lifting) imageE)
    hence "s \ (\i \ n. I (Suc i))" and "(\a. (I 0) +> a) s = b"
      using Inter.rcos_const_imp_mem by auto
    thus "b \ (\a. (I 0) +> a) ` (\i \ n. I (Suc i))"
      by auto
  qed
  hence "(\a. ((I 0) +> a, ?proj (\i. I (Suc i)) n a)) ` carrier R =
         carrier (R Quot (I 0)) \<times> carrier (?DirProd (\<lambda>i. I (Suc i)) n)"
    using aux_lemma[OF ring I.rcos_ring_hom hom] unfolding carrier_Quot ker IH by simp
  moreover show ?case
    unfolding map_simp RDirProd_list_carrier sym[OF calculation(1)] canonical_proj_ext_tl by auto
qed

theorem (in cring) chinese_remainder:
  assumes "\i. i \ n \ ideal (I i) R" and "\i j. \ i \ n; j \ n \ \ i \ j \ I i <+> I j = carrier R"
  shows "R Quot (\i \ n. I i) \ RDirProd_list (map (\i. R Quot (I i)) [0..< Suc n])"
  using ring_hom_ring.FactRing_iso[OF canonical_proj_ext_ring_hom, of n I]
        canonical_proj_ext_is_surj[of n I] canonical_proj_ext_ker[of n I] assms
  by auto

end

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.