Theory Chinese_Remainder_Rings
section ‹The Chinese Remainder Theorem for commutative rings›
theory Chinese_Remainder_Rings
imports Ideal_Theory Ring_Family_Product
begin
text ‹For two comaximal ideals ‹I›, ‹J› of a commutative ring ‹R› (i.e.\ ‹I + J = R›), the quotient
‹R / (I ∩ J)› is isomorphic to the product ring ‹(R / I) × (R / J)›. The proof follows the classical
route: the canonical map ‹a ↦ (I + a, J + a)› into the product of the two quotient rings is a ring
homomorphism, surjective by comaximality, with kernel ‹I ∩ J›; the fundamental theorem of ring
homomorphisms then yields the isomorphism.›
subsection ‹Associative-commutative rewriting in an abelian group›
text ‹The @{locale Abelian_Group} locale exposes only the raw associativity, commutativity and inverse
axioms (each with a carrier side condition), so plain @{method simp} cannot ac-normalise sums. We
prove a few confluent cancellation lemmas and a couple of rearrangement lemmas that the
Chinese-Remainder arithmetic below relies on.›
context Abelian_Group
begin
text ‹Left-nested inverse cancellations (safe as simp rules: not permutative).›
lemma add_assoc_inverse_left [simp]:
"⟦ a ∈ G; b ∈ G ⟧ ⟹ inverse a ⋅ (a ⋅ b) = b"
by (simp add: associative [symmetric])
lemma add_assoc_inverse_left' [simp]:
"⟦ a ∈ G; b ∈ G ⟧ ⟹ a ⋅ (inverse a ⋅ b) = b"
by (simp add: associative [symmetric])
text ‹Rearrangement: @{term "(q ⋅ p) ⋅ inverse (s ⋅ q) = p ⋅ inverse s"}. This is the shape needed to
simplify ‹(x⋅j + y⋅i) - (x⋅i + x⋅j)› in the surjectivity argument.›
lemma add_diff_cancel_mid:
assumes q: "q ∈ G" and p: "p ∈ G" and s: "s ∈ G"
shows "(q ⋅ p) ⋅ inverse (s ⋅ q) = p ⋅ inverse s"
proof -
have ninv: "inverse (s ⋅ q) = inverse q ⋅ inverse s"
using q s by (simp add: inverse_composition_commute commutative)
have "(q ⋅ p) ⋅ inverse (s ⋅ q) = (p ⋅ q) ⋅ (inverse q ⋅ inverse s)"
using q p by (simp add: ninv commutative)
also have "… = p ⋅ (q ⋅ (inverse q ⋅ inverse s))"
using q p s by (simp add: associative)
also have "… = p ⋅ inverse s" using q s by simp
finally show ?thesis .
qed
end
subsection ‹The binary direct product of two rings›
text ‹The external direct product of two rings, carried on pairs, with pointwise operations. This
specialises the indexed direct product of ‹Ring_Family_Product› to two factors, which keeps the
carrier type @{typ "'a × 'b"} rather than a dependent function space --- convenient for the two
quotient rings occurring in the Chinese Remainder Theorem. The notation follows @{locale
ring_homomorphism}: primed operations for the second factor.›
locale ring_pair =
A: Ring R "(+)" "(⋅)" 𝟬 𝟭 + B: Ring R' "(+')" "(⋅')" "𝟬'" "𝟭'"
for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›)
and R' and addition' (infixl ‹+''› 65) and multiplication' (infixl ‹⋅''› 70) and zero' (‹𝟬''›) and unit' (‹𝟭''›)
begin
definition Bcarrier :: "('a × 'b) set"
where "Bcarrier = R × R'"
definition Badd :: "('a × 'b) ⇒ ('a × 'b) ⇒ ('a × 'b)" (infixl ‹⊕⇩×› 65)
where "x ⊕⇩× y = (fst x + fst y, snd x +' snd y)"
definition Bmult :: "('a × 'b) ⇒ ('a × 'b) ⇒ ('a × 'b)" (infixl ‹⊗⇩×› 70)
where "x ⊗⇩× y = (fst x ⋅ fst y, snd x ⋅' snd y)"
definition Bzero :: "'a × 'b" (‹𝟬⇩×›)
where "𝟬⇩× = (𝟬, 𝟬')"
definition Bone :: "'a × 'b" (‹𝟭⇩×›)
where "𝟭⇩× = (𝟭, 𝟭')"
lemma Bcarrier_iff [simp]: "(a, b) ∈ Bcarrier ⟷ a ∈ R ∧ b ∈ R'"
by (simp add: Bcarrier_def)
lemma Badd_apply [simp]: "(a⇩1, b⇩1) ⊕⇩× (a⇩2, b⇩2) = (a⇩1 + a⇩2, b⇩1 +' b⇩2)"
by (simp add: Badd_def)
lemma Bmult_apply [simp]: "(a⇩1, b⇩1) ⊗⇩× (a⇩2, b⇩2) = (a⇩1 ⋅ a⇩2, b⇩1 ⋅' b⇩2)"
by (simp add: Bmult_def)
theorem Ring_Bcarrier: "Ring Bcarrier (⊕⇩×) (⊗⇩×) 𝟬⇩× 𝟭⇩×"
proof (rule Ring.intro)
show "Abelian_Group Bcarrier (⊕⇩×) 𝟬⇩×"
proof (rule Abelian_Group.intro)
show "Group Bcarrier (⊕⇩×) 𝟬⇩×"
proof (rule GroupI)
show "⋀x y. x ∈ Bcarrier ⟹ y ∈ Bcarrier ⟹ x ⊕⇩× y ∈ Bcarrier"
by (auto simp: Badd_def Bcarrier_def)
show "𝟬⇩× ∈ Bcarrier" by (simp add: Bzero_def Bcarrier_def)
next
fix x y z assume "x ∈ Bcarrier" "y ∈ Bcarrier" "z ∈ Bcarrier"
then show "(x ⊕⇩× y) ⊕⇩× z = x ⊕⇩× (y ⊕⇩× z)"
by (auto simp: Badd_def Bcarrier_def A.additive.associative B.additive.associative)
next
fix x assume "x ∈ Bcarrier" then show "𝟬⇩× ⊕⇩× x = x"
by (cases x) (simp add: Bzero_def Bcarrier_def)
next
fix x assume "x ∈ Bcarrier" then show "x ⊕⇩× 𝟬⇩× = x"
by (cases x) (simp add: Bzero_def Bcarrier_def)
next
fix x assume x: "x ∈ Bcarrier"
then have x1: "fst x ∈ R" and x2: "snd x ∈ R'" by (auto simp: Bcarrier_def)
let ?v = "(A.additive.inverse (fst x), B.additive.inverse (snd x))"
have "?v ∈ Bcarrier" using x1 x2 by (simp add: Bcarrier_def)
moreover have "x ⊕⇩× ?v = 𝟬⇩× ∧ ?v ⊕⇩× x = 𝟬⇩×"
using x1 x2 by (cases x) (simp add: Badd_def Bzero_def)
ultimately show "∃y ∈ Bcarrier. x ⊕⇩× y = 𝟬⇩× ∧ y ⊕⇩× x = 𝟬⇩×" by blast
qed
show "commutative_monoid Bcarrier (⊕⇩×) 𝟬⇩×"
proof (rule commutative_monoid.intro)
show "Monoid Bcarrier (⊕⇩×) 𝟬⇩×"
proof (unfold_locales)
show "⋀x y. x ∈ Bcarrier ⟹ y ∈ Bcarrier ⟹ x ⊕⇩× y ∈ Bcarrier"
by (auto simp: Badd_def Bcarrier_def)
show "𝟬⇩× ∈ Bcarrier" by (simp add: Bzero_def Bcarrier_def)
next
fix x y z assume "x ∈ Bcarrier" "y ∈ Bcarrier" "z ∈ Bcarrier"
then show "(x ⊕⇩× y) ⊕⇩× z = x ⊕⇩× (y ⊕⇩× z)"
by (auto simp: Badd_def Bcarrier_def A.additive.associative B.additive.associative)
next
fix x assume "x ∈ Bcarrier" then show "𝟬⇩× ⊕⇩× x = x"
by (cases x) (simp add: Bzero_def Bcarrier_def)
next
fix x assume "x ∈ Bcarrier" then show "x ⊕⇩× 𝟬⇩× = x"
by (cases x) (simp add: Bzero_def Bcarrier_def)
qed
show "commutative_monoid_axioms Bcarrier (⊕⇩×)"
proof (unfold_locales)
fix x y assume "x ∈ Bcarrier" "y ∈ Bcarrier"
then show "x ⊕⇩× y = y ⊕⇩× x"
by (auto simp: Badd_def Bcarrier_def A.additive.commutative B.additive.commutative)
qed
qed
qed
show "Monoid Bcarrier (⊗⇩×) 𝟭⇩×"
proof (unfold_locales)
show "⋀x y. x ∈ Bcarrier ⟹ y ∈ Bcarrier ⟹ x ⊗⇩× y ∈ Bcarrier"
by (auto simp: Bmult_def Bcarrier_def)
show "𝟭⇩× ∈ Bcarrier" by (simp add: Bone_def Bcarrier_def)
next
fix x y z assume "x ∈ Bcarrier" "y ∈ Bcarrier" "z ∈ Bcarrier"
then show "(x ⊗⇩× y) ⊗⇩× z = x ⊗⇩× (y ⊗⇩× z)"
by (auto simp: Bmult_def Bcarrier_def A.multiplicative.associative B.multiplicative.associative)
next
fix x assume "x ∈ Bcarrier" then show "𝟭⇩× ⊗⇩× x = x"
by (cases x) (simp add: Bone_def Bcarrier_def)
next
fix x assume "x ∈ Bcarrier" then show "x ⊗⇩× 𝟭⇩× = x"
by (cases x) (simp add: Bone_def Bcarrier_def)
qed
show "Ring_axioms Bcarrier (⊕⇩×) (⊗⇩×)"
proof
fix x y z assume "x ∈ Bcarrier" "y ∈ Bcarrier" "z ∈ Bcarrier"
then show "x ⊗⇩× (y ⊕⇩× z) = x ⊗⇩× y ⊕⇩× (x ⊗⇩× z)"
by (auto simp: Bmult_def Badd_def Bcarrier_def A.distributive B.distributive)
next
fix x y z assume "x ∈ Bcarrier" "y ∈ Bcarrier" "z ∈ Bcarrier"
then show "(y ⊕⇩× z) ⊗⇩× x = y ⊗⇩× x ⊕⇩× (z ⊗⇩× x)"
by (auto simp: Bmult_def Badd_def Bcarrier_def A.distributive B.distributive)
qed
qed
sublocale product: Ring Bcarrier "(⊕⇩×)" "(⊗⇩×)" Bzero Bone
by (rule Ring_Bcarrier)
end
subsection ‹Sum of two ideals›
text ‹The sum ‹I + J› of two ideals: all sums ‹i + j› with ‹i ∈ I›, ‹j ∈ J›. We work in a commutative
ring throughout (the setting of the Chinese Remainder Theorem).›
context ideal_in_comm_ring
begin
definition ideal_sum :: "'a set ⇒ 'a set"
where "ideal_sum J = {i + j | i j. i ∈ I ∧ j ∈ J}"
lemma ideal_sum_memI: "⟦ i ∈ I; j ∈ J ⟧ ⟹ i + j ∈ ideal_sum J"
unfolding ideal_sum_def by blast
lemma ideal_sum_memE:
assumes "x ∈ ideal_sum J"
obtains i j where "i ∈ I" "j ∈ J" "x = i + j"
using assms unfolding ideal_sum_def by blast
text ‹The sum contains both summands (using that ideals contain ‹𝟬›).›
lemma I_subset_ideal_sum:
assumes "Ideal J R (+) (⋅) 𝟬 𝟭" shows "I ⊆ ideal_sum J"
proof
interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule assms)
fix x assume x: "x ∈ I"
then have xR: "x ∈ R" using additive.subset by blast
have "x + 𝟬 ∈ ideal_sum J" using x J.additive.sub_unit_closed by (rule ideal_sum_memI)
then show "x ∈ ideal_sum J" using xR by simp
qed
lemma J_subset_ideal_sum:
assumes "Ideal J R (+) (⋅) 𝟬 𝟭" shows "J ⊆ ideal_sum J"
proof
interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule assms)
fix x assume x: "x ∈ J"
then have xR: "x ∈ R" using J.additive.subset by blast
have "𝟬 + x ∈ ideal_sum J" using additive.sub_unit_closed x by (rule ideal_sum_memI)
then show "x ∈ ideal_sum J" using xR by simp
qed
text ‹The intersection of the ambient ideal @{term I} with another ideal is again an ideal.›
lemma inter_ideal:
assumes "Ideal J R (+) (⋅) 𝟬 𝟭"
shows "Ideal (I ∩ J) R (+) (⋅) 𝟬 𝟭"
proof -
interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule assms)
have sg: "Subgroup (I ∩ J) R (+) 𝟬"
proof (rule additive.subgroupI)
show "I ∩ J ⊆ R" using additive.subset by blast
show "𝟬 ∈ I ∩ J" using additive.sub_unit_closed J.additive.sub_unit_closed by simp
next
fix g h assume "g ∈ I ∩ J" "h ∈ I ∩ J"
then show "g + h ∈ I ∩ J"
using additive.sub_composition_closed J.additive.sub_composition_closed by auto
next
fix g assume "g ∈ I ∩ J"
then show "additive.invertible g" using additive.subset by auto
next
fix g assume g: "g ∈ I ∩ J"
then have gI: "g ∈ I" and gJ: "g ∈ J" by auto
have "additive.inverse g ∈ I" using gI by simp
moreover have "additive.inverse g ∈ J"
using gJ J.additive.submonoid_inverse_closed J.additive.sub.invertible by auto
ultimately show "additive.inverse g ∈ I ∩ J" by simp
qed
interpret IJ: Subgroup "I ∩ J" R "(+)" 𝟬 by (rule sg)
show ?thesis
proof unfold_locales
fix a b assume a: "a ∈ R" and b: "b ∈ I ∩ J"
show "a ⋅ b ∈ I ∩ J" using a b Ideal J.Ideal by auto
show "b ⋅ a ∈ I ∩ J" using a b Ideal J.Ideal by auto
qed
qed
text ‹Comaximality is preserved under intersection: if @{term I} is comaximal with @{term J} and
with @{term K} (meaning @{term "𝟭 ∈ ideal_sum J"} and @{term "𝟭 ∈ ideal_sum K"}), then @{term I}
is comaximal with @{term "J ∩ K"}. The key step multiplies the two witnesses
@{term "i⇩1 + j = 𝟭"}, @{term "i⇩2 + k = 𝟭"} and regroups.›
lemma comaximal_inter:
assumes J: "Ideal J R (+) (⋅) 𝟬 𝟭" and K: "Ideal K R (+) (⋅) 𝟬 𝟭"
and comIJ: "∃i∈I. ∃j∈J. i + j = 𝟭"
and comIK: "∃i∈I. ∃k∈K. i + k = 𝟭"
shows "∃i∈I. ∃m∈J ∩ K. i + m = 𝟭"
proof -
interpret J: Ideal J R "(+)" "(⋅)" 𝟬 𝟭 by (rule J)
interpret K: Ideal K R "(+)" "(⋅)" 𝟬 𝟭 by (rule K)
obtain i⇩1 j where i1: "i⇩1 ∈ I" and j: "j ∈ J" and ij: "i⇩1 + j = 𝟭"
using comIJ by blast
obtain i⇩2 k where i2: "i⇩2 ∈ I" and k: "k ∈ K" and ik: "i⇩2 + k = 𝟭"
using comIK by blast
have i1R: "i⇩1 ∈ R" using i1 additive.subset by blast
have i2R: "i⇩2 ∈ R" using i2 additive.subset by blast
have jR: "j ∈ R" using j J.additive.subset by blast
have kR: "k ∈ R" using k K.additive.subset by blast
define m where "m = i⇩1 ⋅ i⇩2 + i⇩1 ⋅ k + j ⋅ i⇩2"
have mR: "m ∈ R" unfolding m_def using i1R i2R jR kR by simp
have expand: "(i⇩1 + j) ⋅ (i⇩2 + k) = m + j ⋅ k"
proof -
have d1: "i⇩1 ⋅ (i⇩2 + k) = i⇩1 ⋅ i⇩2 + i⇩1 ⋅ k"
using i1R i2R kR by (simp add: distributive)
have d2: "j ⋅ (i⇩2 + k) = j ⋅ i⇩2 + j ⋅ k"
using jR i2R kR by (simp add: distributive)
have "(i⇩1 + j) ⋅ (i⇩2 + k) = i⇩1 ⋅ (i⇩2 + k) + j ⋅ (i⇩2 + k)"
using distributive(2)[OF _ i1R jR] i2R kR by simp
also have "… = (i⇩1 ⋅ i⇩2 + i⇩1 ⋅ k) + (j ⋅ i⇩2 + j ⋅ k)"
by (simp add: d1 d2)
also have "… = (i⇩1 ⋅ i⇩2 + i⇩1 ⋅ k + j ⋅ i⇩2) + j ⋅ k"
using i1R i2R jR kR by (simp add: additive.associative)
finally show ?thesis unfolding m_def .
qed
have eq: "m + j ⋅ k = 𝟭"
using expand ij ik by simp
have m_in_I: "m ∈ I"
proof -
have "i⇩1 ⋅ i⇩2 ∈ I" using i2R i1 by (simp add: Ideal)
moreover have "i⇩1 ⋅ k ∈ I" using kR i1 by (simp add: Ideal)
moreover have "j ⋅ i⇩2 ∈ I" using jR i2 by (simp add: Ideal)
ultimately show ?thesis unfolding m_def by (simp add: additive.sub_composition_closed)
qed
have jk_in_JK: "j ⋅ k ∈ J ∩ K"
proof
show "j ⋅ k ∈ J" using kR j by (simp add: J.Ideal)
show "j ⋅ k ∈ K" using jR k by (simp add: K.Ideal)
qed
show ?thesis using m_in_I jk_in_JK eq by blast
qed
text ‹The reduction step underlying Chinese-Remainder surjectivity, phrased for a single ideal (where
subtraction notation is unambiguous): if @{term "i + j = 𝟭"} with @{term "i ∈ I"}, then the element
@{term "x ⋅ j + y ⋅ i"} has the same coset as @{term x} modulo @{term I} (because @{term "x ⋅ j ≡ x"}
and @{term "y ⋅ i ≡ 𝟬"} modulo @{term I}).›
lemma coset_comaximal:
assumes x: "x ∈ R" and y: "y ∈ R" and i: "i ∈ I" and jR: "j ∈ R" and ij: "i + j = 𝟭"
shows "coset (x ⋅ j + y ⋅ i) = coset x"
proof -
have iR: "i ∈ R" using i additive.subset by blast
have sumR: "x ⋅ j + y ⋅ i ∈ R" using x y iR jR by simp
have xdecomp: "x = x ⋅ i + x ⋅ j"
proof -
have "x = x ⋅ (i + j)" using ij x by simp
also have "… = x ⋅ i + x ⋅ j" using x iR jR by (simp add: distributive)
finally show ?thesis .
qed
have "(x ⋅ j + y ⋅ i) - x = (x ⋅ j + y ⋅ i) - (x ⋅ i + x ⋅ j)" using xdecomp by simp
also have "… = y ⋅ i - x ⋅ i"
using additive.add_diff_cancel_mid[of "x ⋅ j" "y ⋅ i" "x ⋅ i"] x y iR jR by simp
also have "… = (y - x) ⋅ i" using x y iR by (simp add: distributive left_minus)
finally have eq: "(x ⋅ j + y ⋅ i) - x = (y - x) ⋅ i" .
have "(y - x) ⋅ i ∈ I" using x y i by (simp add: Ideal)
then have "(x ⋅ j + y ⋅ i) - x ∈ I" using eq by simp
then show ?thesis using coset_eq_iff[OF sumR x] by simp
qed
end
subsection ‹Two comaximal ideals›
text ‹The Chinese Remainder Theorem setting: a commutative ring @{term R} with two ideals @{term I},
@{term J} that are ∗‹comaximal› (‹I + J = R›). We package these in a locale, giving each ideal its
own quotient-ring interface (‹I.› and ‹J.›).›
locale comaximal_ideals =
I: quotient_ring I R "(+)" "(⋅)" 𝟬 𝟭 + J: quotient_ring J R "(+)" "(⋅)" 𝟬 𝟭
for I and J and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) +
assumes comm: "⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⋅ b = b ⋅ a"
and comaximal: "∃i∈I. ∃j∈J. i + j = 𝟭"
begin
text ‹Both ideals live in a commutative ring; expose the commutative-ring structure and the
‹ideal_in_comm_ring› facts for each.›
sublocale I: ideal_in_comm_ring I R "(+)" "(⋅)" 𝟬 𝟭
by unfold_locales (rule comm)
sublocale J: ideal_in_comm_ring J R "(+)" "(⋅)" 𝟬 𝟭
by unfold_locales (rule comm)
text ‹The product ring ‹(R/I) × (R/J)› of the two quotient rings.›
sublocale prod: ring_pair
"R / I.Ring_Congruence" "I.additive.quotient_composition" "I.multiplicative.quotient_composition"
"I.additive.Class 𝟬" "I.additive.Class 𝟭"
"R / J.Ring_Congruence" "J.additive.quotient_composition" "J.multiplicative.quotient_composition"
"J.additive.Class 𝟬" "J.additive.Class 𝟭"
by unfold_locales
text ‹The canonical projection ‹a ↦ (I + a, J + a)› into the product of the two quotients.›
definition canon :: "'a ⇒ 'a set × 'a set"
where "canon = restrict (λa. (I.coset a, J.coset a)) R"
lemma canon_apply [simp]: "a ∈ R ⟹ canon a = (I.coset a, J.coset a)"
by (simp add: canon_def)
lemma coset_I_in_carrier: "a ∈ R ⟹ I.coset a ∈ R / I.Ring_Congruence"
using I.coset_in_quotient_set by (simp add: I.quotient_set_def)
lemma coset_J_in_carrier: "a ∈ R ⟹ J.coset a ∈ R / J.Ring_Congruence"
using J.coset_in_quotient_set by (simp add: J.quotient_set_def)
text ‹The canonical projection is a ring homomorphism into the product ring.›
theorem canon_hom:
"ring_homomorphism canon R (+) (⋅) 𝟬 𝟭 prod.Bcarrier (prod.Badd) (prod.Bmult) prod.Bzero prod.Bone"
proof (unfold_locales)
show "canon ∈ R →⇩E prod.Bcarrier"
proof (rule PiE_I)
fix a assume "a ∈ R"
then show "canon a ∈ prod.Bcarrier"
by (simp add: prod.Bcarrier_def coset_I_in_carrier coset_J_in_carrier)
next
fix a assume "a ∉ R" then show "canon a = undefined" by (simp add: canon_def)
qed
next
fix a b assume ab: "a ∈ R" "b ∈ R"
have "I.coset (a + b) = I.additive.quotient_composition (I.coset a) (I.coset b)"
using ab by (simp add: I.coset_def I.additive.Class_commutes_with_composition)
moreover have "J.coset (a + b) = J.additive.quotient_composition (J.coset a) (J.coset b)"
using ab by (simp add: J.coset_def J.additive.Class_commutes_with_composition)
ultimately show "canon (a + b) = prod.Badd (canon a) (canon b)"
using ab by (simp add: prod.Badd_def)
next
fix a b assume ab: "a ∈ R" "b ∈ R"
have "I.coset (a ⋅ b) = I.multiplicative.quotient_composition (I.coset a) (I.coset b)"
using ab by (simp add: I.coset_def I.quot_mult_Class)
moreover have "J.coset (a ⋅ b) = J.multiplicative.quotient_composition (J.coset a) (J.coset b)"
using ab by (simp add: J.coset_def J.quot_mult_Class)
ultimately show "canon (a ⋅ b) = prod.Bmult (canon a) (canon b)"
using ab by (simp add: prod.Bmult_def)
next
show "canon 𝟬 = prod.Bzero"
by (simp add: prod.Bzero_def I.coset_def J.coset_def)
next
show "canon 𝟭 = prod.Bone"
by (simp add: prod.Bone_def I.coset_def J.coset_def)
qed
interpretation canon: ring_homomorphism canon R "(+)" "(⋅)" 𝟬 𝟭
prod.Bcarrier "prod.Badd" "prod.Bmult" prod.Bzero prod.Bone
by (rule canon_hom)
text ‹The kernel of the canonical projection is @{term "I ∩ J"}: an element maps to zero exactly
when both its cosets vanish, i.e.\ it lies in both ideals.›
theorem canon_kernel: "canon.additive.Ker = I ∩ J"
proof (rule set_eqI)
fix a
have "a ∈ canon.additive.Ker ⟷ a ∈ R ∧ canon a = prod.Bzero"
unfolding canon.additive.Ker_def by auto
also have "… ⟷ a ∈ R ∧ I.coset a = I.coset 𝟬 ∧ J.coset a = J.coset 𝟬"
proof (cases "a ∈ R")
case True
then show ?thesis by (simp add: prod.Bzero_def I.coset_def J.coset_def)
qed simp
also have "… ⟷ a ∈ R ∧ a ∈ I ∧ a ∈ J"
by (simp add: I.coset_def J.coset_def I.Class_eq_zero_iff J.Class_eq_zero_iff cong: conj_cong)
also have "… ⟷ a ∈ I ∩ J"
using I.additive.subset by blast
finally show "a ∈ canon.additive.Ker ⟷ a ∈ I ∩ J" .
qed
text ‹Comaximality makes the canonical projection surjective: given target cosets of @{term x} and
@{term y}, the element @{term "x ⋅ j + y ⋅ i"} (where @{term "i + j = 𝟭"}, @{term "i ∈ I"},
@{term "j ∈ J"}) reduces to @{term x} mod @{term I} and to @{term y} mod @{term J}.›
theorem canon_surjective: "canon ` R = prod.Bcarrier"
proof (rule set_eqI)
fix z
show "z ∈ canon ` R ⟷ z ∈ prod.Bcarrier"
proof
assume "z ∈ canon ` R"
then show "z ∈ prod.Bcarrier" using canon.graph by blast
next
assume "z ∈ prod.Bcarrier"
then obtain X Y where zXY: "z = (X, Y)" and X: "X ∈ R / I.Ring_Congruence"
and Y: "Y ∈ R / J.Ring_Congruence" by (auto simp: prod.Bcarrier_def)
obtain x where x: "x ∈ R" and Xx: "X = I.coset x"
using X I.quotient_set_repr by (metis I.quotient_set_def)
obtain y where y: "y ∈ R" and Yy: "Y = J.coset y"
using Y J.quotient_set_repr by (metis J.quotient_set_def)
obtain i j where i: "i ∈ I" and j: "j ∈ J" and ij: "i + j = 𝟭"
using comaximal by blast
have iR: "i ∈ R" using i I.additive.subset by blast
have jR: "j ∈ R" using j J.additive.subset by blast
define a where "a = x ⋅ j + y ⋅ i"
have aR: "a ∈ R" unfolding a_def using x y iR jR by simp
have IX: "I.coset a = I.coset x"
unfolding a_def by (rule I.coset_comaximal[OF x y i jR ij])
have ji: "j + i = 𝟭" using ij iR jR by (simp add: I.additive.commutative)
have "J.coset (y ⋅ i + x ⋅ j) = J.coset y"
by (rule J.coset_comaximal[OF y x j iR ji])
moreover have "y ⋅ i + x ⋅ j = a"
unfolding a_def using x y iR jR by (simp add: I.additive.commutative)
ultimately have JY: "J.coset a = J.coset y" by simp
have "canon a = (X, Y)" using aR IX JY Xx Yy by simp
then show "z ∈ canon ` R" using aR zXY by auto
qed
qed
subsection ‹The Chinese Remainder Theorem›
text ‹Feeding the canonical projection to the fundamental theorem of ring homomorphisms yields
@{term "R / Ker canon"} isomorphic to the image, which surjectivity identifies with the whole
product ring, and the kernel is @{term "I ∩ J"}.›
interpretation canon: ring_homomorphism_fundamental canon R "(+)" "(⋅)" 𝟬 𝟭
prod.Bcarrier "prod.Badd" "prod.Bmult" prod.Bzero prod.Bone
by unfold_locales
text ‹The induced map ‹η¦› is an isomorphism from ‹R / Ker› onto the image; surjectivity identifies the
image with the whole product ring. With @{thm [source] canon_kernel} this is
‹R / (I ∩ J) ≅ (R / I) × (R / J)›.›
theorem chinese_remainder:
"(R / (subgroup_of_additive_group_of_ring.Ring_Congruence (I ∩ J) R (+) 𝟬),
canon.kernel.additive.quotient_composition, canon.kernel.multiplicative.quotient_composition,
canon.kernel.additive.Class 𝟬, canon.kernel.additive.Class 𝟭)
≅⇩R (prod.Bcarrier, prod.Badd, prod.Bmult, prod.Bzero, prod.Bone)"
proof -
have ker: "canon.additive.Ker = I ∩ J" by (rule canon_kernel)
have "ring_isomorphism canon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence (I ∩ J) R (+) 𝟬))
canon.kernel.additive.quotient_composition canon.kernel.multiplicative.quotient_composition
(canon.kernel.additive.Class 𝟬) (canon.kernel.additive.Class 𝟭)
prod.Bcarrier prod.Badd prod.Bmult prod.Bzero prod.Bone"
unfolding ker[symmetric]
proof (rule ring_isomorphism.intro)
show "ring_homomorphism canon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence canon.additive.Ker R (+) 𝟬))
canon.kernel.additive.quotient_composition canon.kernel.multiplicative.quotient_composition
(canon.kernel.additive.Class 𝟬) (canon.kernel.additive.Class 𝟭)
prod.Bcarrier prod.Badd prod.Bmult prod.Bzero prod.Bone"
by (rule canon.induced.ring_homomorphism_axioms)
show "bijective_map canon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence canon.additive.Ker R (+) 𝟬))
prod.Bcarrier"
proof
show "bij_betw canon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence canon.additive.Ker R (+) 𝟬))
prod.Bcarrier"
using canon.additive.induced_image canon.additive.induced_inj_on canon_surjective
by (simp add: bij_betw_def)
qed
qed
then show ?thesis
by (auto simp: isomorphic_as_rings_def)
qed
end
text ‹Transfer of the ring structure along operations that agree on the carrier. If ‹R› is a ring
under ‹(+)›, ‹(⋅)› and the alternative operations ‹(⊕)›, ‹(⊗)› agree with them on all pairs of
carrier elements, then ‹R› is also a ring under ‹(⊕)›, ‹(⊗)›.›
lemma Ring_cong_on_carrier:
fixes R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70)
and addition' (infixl ‹⊕› 65) and multiplication' (infixl ‹⊗› 70) and zero (‹𝟬›) and unit (‹𝟭›)
assumes ring: "Ring R (+) (⋅) 𝟬 𝟭"
and add_eq: "⋀a b. ⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⊕ b = a + b"
and mult_eq: "⋀a b. ⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⊗ b = a ⋅ b"
shows "Ring R (⊕) (⊗) 𝟬 𝟭"
proof -
interpret R: Ring R "(+)" "(⋅)" 𝟬 𝟭 by (rule ring)
show ?thesis
proof (rule Ring.intro)
show "Abelian_Group R (⊕) 𝟬"
proof (rule Abelian_Group.intro)
show "Group R (⊕) 𝟬"
proof (rule GroupI)
show "⋀a b. ⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⊕ b ∈ R" by (simp add: add_eq)
show "𝟬 ∈ R" by simp
show "⋀a b c. ⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (a ⊕ b) ⊕ c = a ⊕ (b ⊕ c)"
by (simp add: add_eq R.additive.associative)
show "⋀a. a ∈ R ⟹ 𝟬 ⊕ a = a" by (simp add: add_eq)
show "⋀a. a ∈ R ⟹ a ⊕ 𝟬 = a" by (simp add: add_eq)
fix u assume u: "u ∈ R"
have "u ⊕ R.additive.inverse u = 𝟬 ∧ R.additive.inverse u ⊕ u = 𝟬"
using u by (simp add: add_eq)
then show "∃v∈R. u ⊕ v = 𝟬 ∧ v ⊕ u = 𝟬" using u by blast
qed
show "commutative_monoid R (⊕) 𝟬"
proof (rule commutative_monoid.intro)
show "Monoid R (⊕) 𝟬"
by unfold_locales (auto simp: add_eq R.additive.associative)
show "commutative_monoid_axioms R (⊕)"
by unfold_locales (simp add: add_eq R.additive.commutative)
qed
qed
show "Monoid R (⊗) 𝟭"
by unfold_locales (auto simp: mult_eq R.multiplicative.associative)
show "Ring_axioms R (⊕) (⊗)"
proof
fix a b c assume "a ∈ R" "b ∈ R" "c ∈ R"
then show "a ⊗ (b ⊕ c) = a ⊗ b ⊕ (a ⊗ c)"
by (simp add: add_eq mult_eq R.distributive)
next
fix a b c assume "a ∈ R" "b ∈ R" "c ∈ R"
then show "(b ⊕ c) ⊗ a = b ⊗ a ⊕ (c ⊗ a)"
by (simp add: add_eq mult_eq R.distributive)
qed
qed
qed
section ‹The n-ary Chinese Remainder Theorem›
text ‹Generalise the binary CRT to a finite family of pairwise-comaximal ideals:
@{text "R / (⋂i∈S. J i) ≅⇩R ∏i∈S. R / J i"}. The proof proceeds by induction on the finite
index set, reducing (n+1) ideals to the binary theorem via the lemma that comaximality is
preserved under intersection.›
subsection ‹Pairwise-comaximal ideals›
locale pairwise_comaximal_ideals =
fixes S :: "'i set"
and J :: "'i ⇒ 'a set"
and R :: "'a set"
and addition (infixl ‹+› 65)
and multiplication (infixl ‹⋅› 70)
and zero (‹𝟬›)
and unit (‹𝟭›)
assumes fin: "finite S"
and nonempty: "S ≠ {}"
and comm: "⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⋅ b = b ⋅ a"
and ideals: "⋀i. i ∈ S ⟹ quotient_ring (J i) R (+) (⋅) 𝟬 𝟭"
and pairwise: "⋀i j. ⟦ i ∈ S; j ∈ S; i ≠ j ⟧ ⟹ ∃a∈J i. ∃b∈J j. a + b = 𝟭"
begin
sublocale Ring R "(+)" "(⋅)" 𝟬 𝟭
proof -
obtain i where "i ∈ S" using nonempty by blast
then interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals)
show "Ring R (+) (⋅) 𝟬 𝟭" ..
qed
sublocale commutative_ring R "(+)" "(⋅)" 𝟬 𝟭
by unfold_locales (rule comm)
text ‹Each @{term "J i"} is an ideal in the commutative ring.›
lemma Ji_ideal: "i ∈ S ⟹ Ideal (J i) R (+) (⋅) 𝟬 𝟭"
proof -
assume "i ∈ S"
then interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals)
show "Ideal (J i) R (+) (⋅) 𝟬 𝟭" ..
qed
lemma Ji_ideal_comm: "i ∈ S ⟹ ideal_in_comm_ring (J i) R (+) (⋅) 𝟬 𝟭"
by (intro ideal_in_comm_ring.intro Ji_ideal commutative_ring_axioms)
text ‹The intersection @{term "⋂ (J ` T)"} over a subset @{term "T ⊆ S"} is again an ideal.›
lemma Inter_ideal:
assumes TS: "T ⊆ S" and Tne: "T ≠ {}"
shows "Ideal (⋂ (J ` T)) R (+) (⋅) 𝟬 𝟭"
proof -
have finT: "finite T" using TS fin finite_subset by blast
show ?thesis using finT Tne TS
proof (induction rule: finite_ne_induct)
case (singleton x)
then show ?case using Ji_ideal by simp
next
case (insert x F)
then have xS: "x ∈ S" and FS: "F ⊆ S" by auto
interpret Jx: ideal_in_comm_ring "J x" R "(+)" "(⋅)" 𝟬 𝟭 by (rule Ji_ideal_comm[OF xS])
have "Ideal (⋂ (J ` F)) R (+) (⋅) 𝟬 𝟭" using insert by auto
then have "Ideal (J x ∩ ⋂ (J ` F)) R (+) (⋅) 𝟬 𝟭"
by (rule Jx.inter_ideal)
then show ?case using insert by simp
qed
qed
text ‹Key induction step: if @{term "J i"} is comaximal with every @{term "J j"} for @{term "j ∈ T"},
then @{term "J i"} is comaximal with @{term "⋂ (J ` T)"}.›
lemma comaximal_with_Inter:
assumes iS: "i ∈ S" and TS: "T ⊆ S" and Tne: "T ≠ {}" and iT: "i ∉ T"
and pw: "⋀j. j ∈ T ⟹ ∃a∈J i. ∃b∈J j. a + b = 𝟭"
shows "∃a∈J i. ∃b∈⋂ (J ` T). a + b = 𝟭"
proof -
have finT: "finite T" using TS fin finite_subset by blast
show ?thesis using finT Tne TS iT pw
proof (induction rule: finite_ne_induct)
case (singleton x)
then show ?case by simp
next
case (insert x F)
then have xS: "x ∈ S" and FS: "F ⊆ S" by auto
have Fne: "F ≠ {}" using insert by simp
have iF: "i ∉ F" using insert.prems by simp
have comF: "∃a∈J i. ∃b∈⋂ (J ` F). a + b = 𝟭"
using insert by auto
have comx: "∃a∈J i. ∃b∈J x. a + b = 𝟭" using insert.prems by simp
interpret Ji: ideal_in_comm_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule Ji_ideal_comm[OF iS])
have Jx_ideal: "Ideal (J x) R (+) (⋅) 𝟬 𝟭" by (rule Ji_ideal[OF xS])
have IF_ideal: "Ideal (⋂ (J ` F)) R (+) (⋅) 𝟬 𝟭"
by (rule Inter_ideal[OF FS Fne])
have "∃a∈J i. ∃b∈J x ∩ ⋂ (J ` F). a + b = 𝟭"
by (rule Ji.comaximal_inter[OF Jx_ideal IF_ideal comx comF])
then show ?case using insert by simp
qed
qed
subsection ‹The canonical projection into the indexed product›
text ‹The quotient rings form a ring family. The coset @{text "Ji_Class i a"} is the equivalence
class of @{term a} modulo the ring congruence induced by @{term "J i"}. The quotient carrier,
operations, and constants are defined in terms of this class map.›
definition Ji_Cong :: "'i ⇒ ('a × 'a) set" where
"Ji_Cong i = {(a, b). a ∈ R ∧ b ∈ R ∧ a - b ∈ J i}"
definition Ji_Class :: "'i ⇒ 'a ⇒ 'a set" where
"Ji_Class i a = {b ∈ R. (a, b) ∈ Ji_Cong i}"
definition quot_carrier :: "'i ⇒ 'a set set" where
"quot_carrier i = Ji_Class i ` R"
definition quot_add :: "'i ⇒ 'a set ⇒ 'a set ⇒ 'a set" where
"quot_add i A B = (THE C. ∃a∈A. ∃b∈B. C = Ji_Class i (a + b))"
definition quot_mult :: "'i ⇒ 'a set ⇒ 'a set ⇒ 'a set" where
"quot_mult i A B = (THE C. ∃a∈A. ∃b∈B. C = Ji_Class i (a ⋅ b))"
definition quot_zero :: "'i ⇒ 'a set" where
"quot_zero i = Ji_Class i 𝟬"
definition quot_one :: "'i ⇒ 'a set" where
"quot_one i = Ji_Class i 𝟭"
lemma Ji_Cong_eq:
assumes "i ∈ S"
shows "Ji_Cong i = subgroup_of_additive_group_of_ring.Ring_Congruence (J i) R addition 𝟬"
proof -
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF assms])
show ?thesis
unfolding Ji_Cong_def qi.Ring_Congruence_def by auto
qed
text ‹Key bridge: @{const Ji_Class} agrees with the quotient-ring coset.
The proof is by unfolding definitions within a local interpretation.›
lemma Ji_Class_unfold:
assumes "a ∈ R"
shows "Ji_Class i a = {b ∈ R. a - b ∈ J i}"
unfolding Ji_Class_def Ji_Cong_def using assms by auto
lemma Ji_Cong_sym:
assumes i: "i ∈ S" and "(a, b) ∈ Ji_Cong i"
shows "(b, a) ∈ Ji_Cong i"
proof -
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
from assms(2) have aR: "a ∈ R" and bR: "b ∈ R" and d: "a - b ∈ J i"
unfolding Ji_Cong_def by auto
have "- (a - b) ∈ J i" using d qi.additive.submonoid_inverse_closed aR bR by simp
then have "b - a ∈ J i"
using aR bR by (simp add: additive.inverse_composition_commute additive.commutative)
then show ?thesis using aR bR unfolding Ji_Cong_def by auto
qed
lemma Ji_Class_mem_sym:
assumes i: "i ∈ S" and "a ∈ R" "b ∈ Ji_Class i a"
shows "a ∈ Ji_Class i b"
proof -
from assms(3) have bR: "b ∈ R" and ab: "(a, b) ∈ Ji_Cong i"
unfolding Ji_Class_def by auto
have "(b, a) ∈ Ji_Cong i" by (rule Ji_Cong_sym[OF i ab])
then show ?thesis using assms(2) unfolding Ji_Class_def by auto
qed
lemma Ji_Class_coset_bridge:
assumes i: "i ∈ S" and aR: "a ∈ R"
shows "Ji_Class i a = {b ∈ R. (a, b) ∈ Ji_Cong i}"
unfolding Ji_Class_def by auto
text ‹Within an interpretation @{text "qi: quotient_ring (J i) R (+) (⋅) 𝟬 𝟭"},
the coset @{text "qi.coset a"} equals @{term "Ji_Class i a"}. We package this as a
fact to use in proofs.›
lemma Ji_Class_qi_coset:
assumes i: "i ∈ S" and aR: "a ∈ R"
shows "Ji_Class i a = {b ∈ R. a - b ∈ J i}"
by (rule Ji_Class_unfold[OF aR])
text ‹The coset map is well-defined modulo the congruence.›
lemma Ji_Class_cong:
assumes i: "i ∈ S" and "a ∈ R" "b ∈ R" "(a, b) ∈ Ji_Cong i"
shows "Ji_Class i a = Ji_Class i b"
proof -
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have ca: "Ji_Class i a = qi.coset a" and cb: "Ji_Class i b = qi.coset b"
using ‹a ∈ R› ‹b ∈ R› qi.additive.symmetric
by (auto simp: Ji_Class_def Ji_Cong_eq i qi.coset_def)
have "qi.coset a = qi.coset b"
using assms by (simp add: qi.coset_def qi.additive.Class_equivalence
qi.additive_congruence Ji_Cong_eq[OF i])
then show ?thesis using ca cb by simp
qed
lemma Ji_Class_repr:
assumes i: "i ∈ S" and "A ∈ quot_carrier i"
obtains a where "a ∈ R" "A = Ji_Class i a"
using assms unfolding quot_carrier_def by auto
lemma quot_Ring:
assumes i: "i ∈ S"
shows "Ring (quot_carrier i) (quot_add i) (quot_mult i) (quot_zero i) (quot_one i)"
proof -
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have class_eq: "⋀a. a ∈ R ⟹ Ji_Class i a = qi.coset a"
using qi.additive.symmetric
by (auto simp: Ji_Class_def Ji_Cong_eq i qi.coset_def)
have carrier: "quot_carrier i = qi.quotient_set"
unfolding quot_carrier_def qi.quotient_set_def qi.additive.Partition_def qi.coset_def
using class_eq qi.coset_def by (auto simp: image_def)
have qzero: "quot_zero i = qi.coset 𝟬" by (simp add: quot_zero_def class_eq)
have qone: "quot_one i = qi.coset 𝟭" by (simp add: quot_one_def class_eq)
have qadd: "quot_add i A B = qi.additive.quotient_composition A B"
if AB: "A ∈ quot_carrier i" "B ∈ quot_carrier i" for A B
proof -
obtain a b where aR: "a ∈ R" "A = Ji_Class i a" and bR: "b ∈ R" "B = Ji_Class i b"
using AB unfolding quot_carrier_def by auto
have Aca: "A = qi.coset a" using aR class_eq by simp
have Bcb: "B = qi.coset b" using bR class_eq by simp
have rhs: "qi.additive.quotient_composition A B = qi.coset (a + b)"
using aR(1) bR(1) Aca Bcb by (simp add: qi.coset_def qi.additive.Class_commutes_with_composition)
have aA: "a ∈ A" using aR(1,2) unfolding Ji_Class_def Ji_Cong_def by auto
moreover have bB: "b ∈ B" using bR(1,2) unfolding Ji_Class_def Ji_Cong_def by auto
moreover have "⋀a' b'. a' ∈ A ⟹ b' ∈ B ⟹ Ji_Class i (a' + b') = Ji_Class i (a + b)"
proof -
fix a' b' assume "a' ∈ A" "b' ∈ B"
then have a'R: "a' ∈ R" and b'R: "b' ∈ R"
using AB unfolding quot_carrier_def Ji_Class_def by auto
have "qi.coset a' = qi.coset a"
using ‹a' ∈ A› Aca a'R aR(1) qi.coset_def qi.additive.Class_equivalence qi.additive_congruence
by auto
moreover have "qi.coset b' = qi.coset b"
using ‹b' ∈ B› Bcb b'R bR(1) qi.coset_def qi.additive.Class_equivalence qi.additive_congruence
by auto
ultimately have "qi.coset (a' + b') = qi.coset (a + b)"
proof -
assume eq_a: "qi.coset a' = qi.coset a" and eq_b: "qi.coset b' = qi.coset b"
have "qi.coset (a' + b') = qi.additive.quotient_composition (qi.coset a') (qi.coset b')"
using a'R b'R by (simp add: qi.coset_def qi.additive.Class_commutes_with_composition)
also have "… = qi.additive.quotient_composition (qi.coset a) (qi.coset b)"
by (simp add: eq_a eq_b)
also have "… = qi.coset (a + b)"
using aR(1) bR(1) by (simp add: qi.coset_def qi.additive.Class_commutes_with_composition)
finally show "qi.coset (a' + b') = qi.coset (a + b)" .
qed
then show "Ji_Class i (a' + b') = Ji_Class i (a + b)"
using class_eq a'R b'R aR(1) bR(1) by simp
qed
ultimately have "quot_add i A B = Ji_Class i (a + b)"
unfolding quot_add_def by (intro the_equality; blast)
also have "… = qi.coset (a + b)" using class_eq aR(1) bR(1) by simp
finally show ?thesis using rhs by simp
qed
have qmult: "quot_mult i A B = qi.multiplicative.quotient_composition A B"
if AB: "A ∈ quot_carrier i" "B ∈ quot_carrier i" for A B
proof -
interpret qi_comm: ideal_in_comm_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule Ji_ideal_comm[OF i])
obtain a b where aR: "a ∈ R" "A = Ji_Class i a" and bR: "b ∈ R" "B = Ji_Class i b"
using AB unfolding quot_carrier_def by auto
have Aca: "A = qi.coset a" using aR class_eq by simp
have Bcb: "B = qi.coset b" using bR class_eq by simp
have rhs: "qi.multiplicative.quotient_composition A B = qi.coset (a ⋅ b)"
using aR(1) bR(1) Aca Bcb by (simp add: qi.coset_def qi_comm.quot_mult_Class)
have "a ∈ A" using aR(1,2) unfolding Ji_Class_def Ji_Cong_def by auto
moreover have "b ∈ B" using bR(1,2) unfolding Ji_Class_def Ji_Cong_def by auto
moreover have "⋀a' b'. a' ∈ A ⟹ b' ∈ B ⟹ Ji_Class i (a' ⋅ b') = Ji_Class i (a ⋅ b)"
proof -
fix a' b' assume "a' ∈ A" "b' ∈ B"
then have a'R: "a' ∈ R" and b'R: "b' ∈ R"
using AB unfolding quot_carrier_def Ji_Class_def by auto
have "(a, a') ∈ Ji_Cong i" using ‹a' ∈ A› aR(2) unfolding Ji_Class_def by auto
then have ca: "(a', a) ∈ qi.Ring_Congruence" using Ji_Cong_sym[OF i] Ji_Cong_eq[OF i] by simp
have "(b, b') ∈ Ji_Cong i" using ‹b' ∈ B› bR(2) unfolding Ji_Class_def by auto
then have cb: "(b', b) ∈ qi.Ring_Congruence" using Ji_Cong_sym[OF i] Ji_Cong_eq[OF i] by simp
have "(a' ⋅ b', a ⋅ b) ∈ qi.Ring_Congruence"
using ca cb by (rule qi.multiplicative_congruence)
then have "(a' ⋅ b', a ⋅ b) ∈ Ji_Cong i" using Ji_Cong_eq[OF i] by simp
then show "Ji_Class i (a' ⋅ b') = Ji_Class i (a ⋅ b)"
using Ji_Class_cong[OF i] a'R b'R aR(1) bR(1) by simp
qed
ultimately have "quot_mult i A B = Ji_Class i (a ⋅ b)"
unfolding quot_mult_def by (intro the_equality; blast)
also have "… = qi.coset (a ⋅ b)" using class_eq aR(1) bR(1) by simp
finally show ?thesis using rhs by simp
qed
have "Ring (quot_carrier i) qi.additive.quotient_composition qi.multiplicative.quotient_composition
(quot_zero i) (quot_one i)"
unfolding carrier qzero qone qi.quotient_set_def qi.coset_def by unfold_locales
then show ?thesis
using qadd qmult by (rule Ring_cong_on_carrier) auto
qed
interpretation prod: ring_family S quot_carrier quot_add quot_mult quot_zero quot_one
by (rule ring_family.intro) (rule quot_Ring)
text ‹The coset map for each component --- directly uses @{const Ji_Class}.›
definition ncoset :: "'i ⇒ 'a ⇒ 'a set" where
"ncoset i a = Ji_Class i a"
lemma ncoset_in_carrier:
assumes "i ∈ S" "a ∈ R"
shows "ncoset i a ∈ quot_carrier i"
unfolding ncoset_def quot_carrier_def using assms(2) by auto
text ‹The canonical map ‹a ↦ (λi∈S. Ji_Class i a)› into the indexed product.›
definition ncanon :: "'a ⇒ ('i ⇒ 'a set)" where
"ncanon = restrict (λa. λi∈S. ncoset i a) R"
lemma ncanon_apply:
assumes "a ∈ R" "i ∈ S"
shows "ncanon a i = ncoset i a"
using assms by (simp add: ncanon_def)
lemma ncanon_closed:
assumes "a ∈ R"
shows "ncanon a ∈ prod.Pcarrier"
proof (rule prod.Pcarrier_memI)
fix i assume i: "i ∈ S"
show "ncanon a i ∈ quot_carrier i"
using assms i by (simp add: ncanon_apply ncoset_in_carrier)
next
show "ncanon a ∈ extensional S" using assms by (simp add: ncanon_def)
qed
lemma ncanon_outside: "a ∉ R ⟹ ncanon a = undefined"
by (simp add: ncanon_def)
text ‹The canonical map is a ring homomorphism.›
theorem ncanon_hom:
"ring_homomorphism ncanon R (+) (⋅) 𝟬 𝟭
prod.Pcarrier prod.Padd prod.Pmult prod.Pzero prod.Pone"
proof unfold_locales
show "ncanon ∈ R →⇩E prod.Pcarrier"
proof (rule PiE_I)
fix a assume "a ∈ R" then show "ncanon a ∈ prod.Pcarrier" by (rule ncanon_closed)
next
fix a assume "a ∉ R" then show "ncanon a = undefined" by (rule ncanon_outside)
qed
next
fix a b assume ab: "a ∈ R" "b ∈ R"
show "ncanon (a + b) = prod.Padd (ncanon a) (ncanon b)"
proof (rule prod.Pcarrier_eqI)
show "ncanon (a + b) ∈ prod.Pcarrier" using ab by (simp add: ncanon_closed)
show "prod.Padd (ncanon a) (ncanon b) ∈ prod.Pcarrier"
using ab by (simp add: ncanon_closed)
next
fix i assume i: "i ∈ S"
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have lhs: "ncanon (a + b) i = Ji_Class i (a + b)"
using ab i by (simp add: ncanon_apply ncoset_def)
have rhs: "prod.Padd (ncanon a) (ncanon b) i =
quot_add i (Ji_Class i a) (Ji_Class i b)"
using ab i by (simp add: ncanon_apply prod.Padd_apply ncoset_def)
also have "… = Ji_Class i (a + b)"
unfolding quot_add_def
proof (rule the_equality)
show "∃a'∈Ji_Class i a. ∃b'∈Ji_Class i b. Ji_Class i (a + b) = Ji_Class i (a' + b')"
proof (intro bexI)
show "a ∈ Ji_Class i a" using ab(1) unfolding Ji_Class_def Ji_Cong_def by auto
show "b ∈ Ji_Class i b" using ab(2) unfolding Ji_Class_def Ji_Cong_def by auto
qed simp
next
fix C assume "∃a'∈Ji_Class i a. ∃b'∈Ji_Class i b. C = Ji_Class i (a' + b')"
then obtain a' b' where a'A: "a' ∈ Ji_Class i a" and b'B: "b' ∈ Ji_Class i b"
and Ceq: "C = Ji_Class i (a' + b')" by auto
have a'R: "a' ∈ R" using a'A unfolding Ji_Class_def by auto
have b'R: "b' ∈ R" using b'B unfolding Ji_Class_def by auto
have ca: "(a', a) ∈ qi.Ring_Congruence"
proof -
have d: "a - a' ∈ J i" using a'A ab(1) unfolding Ji_Class_def Ji_Cong_def by auto
have dR: "a - a' ∈ R" using ab(1) a'R by simp
have "a' - a = - (a - a')"
using ab(1) a'R by (simp add: additive.inverse_composition_commute additive.commutative)
also have "- (a - a') ∈ J i" using d dR qi.additive.submonoid_inverse_closed by simp
finally have "a' - a ∈ J i" .
then show ?thesis using a'R ab(1) unfolding qi.Ring_Congruence_def by auto
qed
have cb: "(b', b) ∈ qi.Ring_Congruence"
proof -
have d: "b - b' ∈ J i" using b'B ab(2) unfolding Ji_Class_def Ji_Cong_def by auto
have dR: "b - b' ∈ R" using ab(2) b'R by simp
have "b' - b = - (b - b')"
using ab(2) b'R by (simp add: additive.inverse_composition_commute additive.commutative)
also have "- (b - b') ∈ J i" using d dR qi.additive.submonoid_inverse_closed by simp
finally have "b' - b ∈ J i" .
then show ?thesis using b'R ab(2) unfolding qi.Ring_Congruence_def by auto
qed
have "(a' + b', a + b) ∈ qi.Ring_Congruence"
using qi.additive.cong[simplified qi.additive_congruence, OF ca cb] .
then have "(a' + b', a + b) ∈ Ji_Cong i" using Ji_Cong_eq[OF i] by simp
then have "Ji_Class i (a' + b') = Ji_Class i (a + b)"
using a'R b'R ab(1) ab(2) by (intro Ji_Class_cong[OF i]) auto
then show "C = Ji_Class i (a + b)" using Ceq by simp
qed
finally show "ncanon (a + b) i = prod.Padd (ncanon a) (ncanon b) i"
using lhs by simp
qed
next
fix a b assume ab: "a ∈ R" "b ∈ R"
show "ncanon (a ⋅ b) = prod.Pmult (ncanon a) (ncanon b)"
proof (rule prod.Pcarrier_eqI)
show "ncanon (a ⋅ b) ∈ prod.Pcarrier" using ab by (simp add: ncanon_closed)
show "prod.Pmult (ncanon a) (ncanon b) ∈ prod.Pcarrier"
using ab by (simp add: ncanon_closed)
next
fix i assume i: "i ∈ S"
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have lhs: "ncanon (a ⋅ b) i = Ji_Class i (a ⋅ b)"
using ab i by (simp add: ncanon_apply ncoset_def)
have rhs: "prod.Pmult (ncanon a) (ncanon b) i =
quot_mult i (Ji_Class i a) (Ji_Class i b)"
using ab i by (simp add: ncanon_apply prod.Pmult_apply ncoset_def)
also have "… = Ji_Class i (a ⋅ b)"
unfolding quot_mult_def
proof (rule the_equality)
show "∃a'∈Ji_Class i a. ∃b'∈Ji_Class i b. Ji_Class i (a ⋅ b) = Ji_Class i (a' ⋅ b')"
proof (intro bexI)
show "a ∈ Ji_Class i a" using ab(1) unfolding Ji_Class_def Ji_Cong_def by auto
show "b ∈ Ji_Class i b" using ab(2) unfolding Ji_Class_def Ji_Cong_def by auto
qed simp
next
fix C assume "∃a'∈Ji_Class i a. ∃b'∈Ji_Class i b. C = Ji_Class i (a' ⋅ b')"
then obtain a' b' where a'A: "a' ∈ Ji_Class i a" and b'B: "b' ∈ Ji_Class i b"
and Ceq: "C = Ji_Class i (a' ⋅ b')" by auto
have a'R: "a' ∈ R" using a'A unfolding Ji_Class_def by auto
have b'R: "b' ∈ R" using b'B unfolding Ji_Class_def by auto
have ca: "(a', a) ∈ qi.Ring_Congruence"
proof -
have "a - a' ∈ J i" using a'A ab(1) unfolding Ji_Class_def Ji_Cong_def by auto
then have "- (a - a') ∈ J i"
using qi.additive.submonoid_inverse_closed ab(1) a'R by simp
then have "a' - a ∈ J i"
using ab(1) a'R by (simp add: additive.inverse_composition_commute additive.commutative)
then show ?thesis using a'R ab(1) unfolding qi.Ring_Congruence_def by auto
qed
have cb: "(b', b) ∈ qi.Ring_Congruence"
proof -
have "b - b' ∈ J i" using b'B ab(2) unfolding Ji_Class_def Ji_Cong_def by auto
then have "- (b - b') ∈ J i"
using qi.additive.submonoid_inverse_closed ab(2) b'R by simp
then have "b' - b ∈ J i"
using ab(2) b'R by (simp add: additive.inverse_composition_commute additive.commutative)
then show ?thesis using b'R ab(2) unfolding qi.Ring_Congruence_def by auto
qed
have "(a' ⋅ b', a ⋅ b) ∈ qi.Ring_Congruence"
using ca cb by (rule qi.multiplicative_congruence)
then have "(a' ⋅ b', a ⋅ b) ∈ Ji_Cong i" using Ji_Cong_eq[OF i] by simp
then have "Ji_Class i (a' ⋅ b') = Ji_Class i (a ⋅ b)"
using a'R b'R ab(1) ab(2) by (intro Ji_Class_cong[OF i]) auto
then show "C = Ji_Class i (a ⋅ b)" using Ceq by simp
qed
finally show "ncanon (a ⋅ b) i = prod.Pmult (ncanon a) (ncanon b) i"
using lhs by simp
qed
next
show "ncanon 𝟬 = prod.Pzero"
proof (rule prod.Pcarrier_eqI)
show "ncanon 𝟬 ∈ prod.Pcarrier" by (simp add: ncanon_closed)
show "prod.Pzero ∈ prod.Pcarrier" by simp
next
fix i assume i: "i ∈ S"
show "ncanon 𝟬 i = prod.Pzero i"
using i by (simp add: ncanon_apply prod.Pzero_apply quot_zero_def ncoset_def)
qed
next
show "ncanon 𝟭 = prod.Pone"
proof (rule prod.Pcarrier_eqI)
show "ncanon 𝟭 ∈ prod.Pcarrier" by (simp add: ncanon_closed)
show "prod.Pone ∈ prod.Pcarrier" by simp
next
fix i assume i: "i ∈ S"
show "ncanon 𝟭 i = prod.Pone i"
using i by (simp add: ncanon_apply prod.Pone_apply quot_one_def ncoset_def)
qed
qed
interpretation ncanon: ring_homomorphism ncanon R "(+)" "(⋅)" 𝟬 𝟭
prod.Pcarrier prod.Padd prod.Pmult prod.Pzero prod.Pone
by (rule ncanon_hom)
interpretation ncanon: ring_homomorphism_fundamental ncanon R "(+)" "(⋅)" 𝟬 𝟭
prod.Pcarrier prod.Padd prod.Pmult prod.Pzero prod.Pone
by unfold_locales
subsection ‹Kernel and surjectivity›
text ‹The kernel of the canonical projection is @{term "⋂ (J ` S)"}.›
theorem ncanon_kernel: "ncanon.additive.Ker = ⋂ (J ` S)"
proof (rule set_eqI)
fix a
show "a ∈ ncanon.additive.Ker ⟷ a ∈ ⋂ (J ` S)"
proof
assume ker: "a ∈ ncanon.additive.Ker"
then have aR: "a ∈ R" and eq: "ncanon a = prod.Pzero"
unfolding ncanon.additive.Ker_def by auto
show "a ∈ ⋂ (J ` S)"
proof (rule InterI)
fix X assume "X ∈ J ` S"
then obtain i where i: "i ∈ S" and Xi: "X = J i" by auto
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have "ncanon a i = prod.Pzero i" using eq by simp
then have cls: "Ji_Class i a = Ji_Class i 𝟬"
using i aR by (simp add: ncanon_apply prod.Pzero_apply ncoset_def quot_zero_def)
have "a ∈ Ji_Class i a"
using aR qi.additive.sub_unit_closed unfolding Ji_Class_def Ji_Cong_def by simp
then have "a ∈ Ji_Class i 𝟬" using cls by simp
then have "(𝟬, a) ∈ Ji_Cong i" unfolding Ji_Class_def by simp
then have "(a, 𝟬) ∈ Ji_Cong i" by (rule Ji_Cong_sym[OF i])
then have "a - 𝟬 ∈ J i" using aR unfolding Ji_Cong_def by simp
then have "a ∈ J i" using aR by simp
then show "a ∈ X" using Xi by simp
qed
next
assume aInt: "a ∈ ⋂ (J ` S)"
then have aI: "⋀i. i ∈ S ⟹ a ∈ J i" by auto
have aR: "a ∈ R"
proof -
obtain i where "i ∈ S" using nonempty by blast
then interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals)
show "a ∈ R" using aI[OF ‹i ∈ S›] qi.additive.subset by blast
qed
have "ncanon a = prod.Pzero"
proof (rule prod.Pcarrier_eqI)
show "ncanon a ∈ prod.Pcarrier" by (rule ncanon_closed[OF aR])
show "prod.Pzero ∈ prod.Pcarrier" by simp
next
fix i assume i: "i ∈ S"
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
have "a ∈ J i" using aI[OF i] .
then have "a - 𝟬 ∈ J i" using aR by simp
then have cong: "(a, 𝟬) ∈ Ji_Cong i" using aR unfolding Ji_Cong_def by auto
then have "Ji_Class i a = Ji_Class i 𝟬"
by (intro Ji_Class_cong[OF i aR _ cong]) simp
then show "ncanon a i = prod.Pzero i"
using i aR by (simp add: ncanon_apply prod.Pzero_apply ncoset_def quot_zero_def)
qed
then show "a ∈ ncanon.additive.Ker"
unfolding ncanon.additive.Ker_def using aR by auto
qed
qed
text ‹The @{const Ji_Class} version of @{thm ideal_in_comm_ring.coset_comaximal}: if
@{term "m + n = 𝟭"} with @{term "m ∈ J i"}, then @{term "x ⋅ n + y ⋅ m"} and @{term x} have the
same class modulo @{term "J i"}.›
lemma Ji_Class_comaximal:
assumes i: "i ∈ S" and x: "x ∈ R" and y: "y ∈ R"
and m: "m ∈ J i" and nR: "n ∈ R" and mn: "m + n = 𝟭"
shows "Ji_Class i (x ⋅ n + y ⋅ m) = Ji_Class i x"
proof -
interpret qi: quotient_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule ideals[OF i])
interpret Ji: ideal_in_comm_ring "J i" R "(+)" "(⋅)" 𝟬 𝟭 by (rule Ji_ideal_comm[OF i])
have bridge: "⋀c. c ∈ R ⟹ Ji_Class i c = qi.coset c"
using qi.additive.symmetric by (auto simp: Ji_Class_def Ji_Cong_eq i qi.coset_def)
have mR: "m ∈ R" using m qi.additive.subset by blast
have xnymR: "x ⋅ n + y ⋅ m ∈ R" using x y mR nR by simp
have "qi.coset (x ⋅ n + y ⋅ m) = qi.coset x"
using Ji.coset_comaximal[OF x y m nR mn] by (simp add: qi.coset_def)
then show ?thesis using bridge[OF xnymR] bridge[OF x] by simp
qed
text ‹Surjectivity of the canonical map. We first prove, by induction on a nonempty finite
subset ‹T ⊆ S›, that any family of target classes over ‹T› is realised simultaneously by a
single element of ‹R›. The inductive step splits off one index ‹k› and combines a solution
over the rest via the comaximality of ‹J k› with ‹⋂ (J ` F)› (@{thm comaximal_with_Inter}).›
lemma partial_solution:
assumes "T ⊆ S" and "T ≠ {}" and "⋀i. i ∈ T ⟹ x i ∈ R"
shows "∃a∈R. ∀i∈T. Ji_Class i a = Ji_Class i (x i)"
proof -
have finT: "finite T" using assms(1) fin finite_subset by blast
have "T ≠ {} ⟹ T ⊆ S ⟹ (∀i∈T. x i ∈ R) ⟹
(∃a∈R. ∀i∈T. Ji_Class i a = Ji_Class i (x i))"
using finT
proof (induction T rule: finite_induct)
case empty
then show ?case by simp
next
case (insert k F)
have kS: "k ∈ S" using insert.prems by auto
have xkR: "x k ∈ R" using insert.prems by simp
show ?case
proof (cases "F = {}")
case True
have "∀i∈insert k F. Ji_Class i (x k) = Ji_Class i (x i)" using True by simp
then show ?thesis using xkR by blast
next
case Fne: False
have FS: "F ⊆ S" using insert.prems by auto
have kF: "k ∉ F" by (rule insert.hyps)
obtain y where yR: "y ∈ R" and yF: "⋀i. i ∈ F ⟹ Ji_Class i y = Ji_Class i (x i)"
using insert.IH Fne FS insert.prems(3) by auto
have "∃m∈J k. ∃n∈⋂ (J ` F). m + n = 𝟭"
proof (rule comaximal_with_Inter[OF kS FS Fne kF])
fix j assume j: "j ∈ F"
then have "j ∈ S" using FS by auto
then show "∃a∈J k. ∃b∈J j. a + b = 𝟭"
using pairwise[OF kS] kF j by auto
qed
then obtain m n where m: "m ∈ J k" and n: "n ∈ ⋂ (J ` F)" and mn: "m + n = 𝟭" by blast
have mR: "m ∈ R"
proof -
interpret Jk: Ideal "J k" R "(+)" "(⋅)" 𝟬 𝟭 by (rule Ji_ideal[OF kS])
show ?thesis using m Jk.additive.subset by blast
qed
have nR: "n ∈ R"
proof -
obtain j where j: "j ∈ F" using Fne by blast
then interpret Jj: Ideal "J j" R "(+)" "(⋅)" 𝟬 𝟭 using Ji_ideal FS by blast
have "n ∈ J j" using n j by blast
then show ?thesis using Jj.additive.subset by blast
qed
define a where "a = x k ⋅ n + y ⋅ m"
have aR: "a ∈ R" unfolding a_def using xkR yR mR nR by simp
have "∀i∈insert k F. Ji_Class i a = Ji_Class i (x i)"
proof
fix i assume "i ∈ insert k F"
then consider "i = k" | "i ∈ F" by auto
then show "Ji_Class i a = Ji_Class i (x i)"
proof cases
case 1
have "Ji_Class k a = Ji_Class k (x k)"
unfolding a_def by (rule Ji_Class_comaximal[OF kS xkR yR m nR mn])
then show ?thesis using 1 by simp
next
case 2
have iS: "i ∈ S" using 2 FS by auto
have nJi: "n ∈ J i" using n 2 by blast
have nm: "n + m = 𝟭" using mn mR nR by (simp add: additive.commutative)
have "Ji_Class i (y ⋅ m + x k ⋅ n) = Ji_Class i y"
by (rule Ji_Class_comaximal[OF iS yR xkR nJi mR nm])
moreover have "y ⋅ m + x k ⋅ n = a"
unfolding a_def using xkR yR mR nR by (simp add: additive.commutative)
ultimately have "Ji_Class i a = Ji_Class i y" by simp
then show ?thesis using yF[OF 2] by simp
qed
qed
then show ?thesis using aR by blast
qed
qed
then show ?thesis using assms by blast
qed
theorem ncanon_surjective: "ncanon ` R = prod.Pcarrier"
proof
show "ncanon ` R ⊆ prod.Pcarrier" using ncanon_closed by blast
next
show "prod.Pcarrier ⊆ ncanon ` R"
proof
fix f assume f: "f ∈ prod.Pcarrier"
have "∀i∈S. ∃xi∈R. f i = Ji_Class i xi"
proof
fix i assume i: "i ∈ S"
have "f i ∈ quot_carrier i" using f i by (simp add: prod.Pcarrier_component)
then show "∃xi∈R. f i = Ji_Class i xi" unfolding quot_carrier_def by auto
qed
then obtain x where xR: "⋀i. i ∈ S ⟹ x i ∈ R"
and fx: "⋀i. i ∈ S ⟹ f i = Ji_Class i (x i)" by metis
have "∃a∈R. ∀i∈S. Ji_Class i a = Ji_Class i (x i)"
by (rule partial_solution[OF subset_refl nonempty]) (rule xR)
then obtain a where aR: "a ∈ R" and aeq: "⋀i. i ∈ S ⟹ Ji_Class i a = Ji_Class i (x i)"
by blast
have "ncanon a = f"
proof (rule prod.Pcarrier_eqI)
show "ncanon a ∈ prod.Pcarrier" by (rule ncanon_closed[OF aR])
show "f ∈ prod.Pcarrier" by (rule f)
next
fix i assume i: "i ∈ S"
have "ncanon a i = Ji_Class i a" using aR i by (simp add: ncanon_apply ncoset_def)
also have "… = Ji_Class i (x i)" using aeq[OF i] .
also have "… = f i" using fx[OF i] by simp
finally show "ncanon a i = f i" .
qed
then show "f ∈ ncanon ` R" using aR by blast
qed
qed
subsection ‹The n-ary Chinese Remainder Theorem›
theorem chinese_remainder_general:
"(R / (subgroup_of_additive_group_of_ring.Ring_Congruence (⋂ (J ` S)) R (+) 𝟬),
ncanon.kernel.additive.quotient_composition, ncanon.kernel.multiplicative.quotient_composition,
ncanon.kernel.additive.Class 𝟬, ncanon.kernel.additive.Class 𝟭)
≅⇩R (prod.Pcarrier, prod.Padd, prod.Pmult, prod.Pzero, prod.Pone)"
proof -
have ker: "ncanon.additive.Ker = ⋂ (J ` S)" by (rule ncanon_kernel)
have "ring_isomorphism ncanon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence (⋂ (J ` S)) R (+) 𝟬))
ncanon.kernel.additive.quotient_composition ncanon.kernel.multiplicative.quotient_composition
(ncanon.kernel.additive.Class 𝟬) (ncanon.kernel.additive.Class 𝟭)
prod.Pcarrier prod.Padd prod.Pmult prod.Pzero prod.Pone"
unfolding ker[symmetric]
proof (rule ring_isomorphism.intro)
show "ring_homomorphism ncanon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence ncanon.additive.Ker R (+) 𝟬))
ncanon.kernel.additive.quotient_composition ncanon.kernel.multiplicative.quotient_composition
(ncanon.kernel.additive.Class 𝟬) (ncanon.kernel.additive.Class 𝟭)
prod.Pcarrier prod.Padd prod.Pmult prod.Pzero prod.Pone"
by (rule ncanon.induced.ring_homomorphism_axioms)
show "bijective_map ncanon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence ncanon.additive.Ker R (+) 𝟬))
prod.Pcarrier"
proof
show "bij_betw ncanon.additive.induced
(R / (subgroup_of_additive_group_of_ring.Ring_Congruence ncanon.additive.Ker R (+) 𝟬))
prod.Pcarrier"
using ncanon.additive.induced_image ncanon.additive.induced_inj_on ncanon_surjective
by (simp add: bij_betw_def)
qed
qed
then show ?thesis
by (auto simp: isomorphic_as_rings_def)
qed
end
end