(* Copyright (c) 2015--2019 by Clemens Ballarin This file is licensed under the 3-clause BSD license. *) theory Ring_Theory imports Group_Theory begin no_notation plus (infixl ‹+› 65) no_notation minus (infixl ‹-› 65) unbundle no uminus_syntax no_notation quotient (infixl ‹'/'/› 90) section ‹Rings› subsection ‹Definition and Elementary Properties› text ‹Def 2.1› text ‹p 86, ll 20--28› locale ring = additive: abelian_group R "(+)" 𝟬 + multiplicative: monoid R "(⋅)" 𝟭 for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) + assumes distributive: "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ a ⋅ (b + c) = a ⋅ b + a ⋅ c" "⟦ a ∈ R; b ∈ R; c ∈ R ⟧ ⟹ (b + c) ⋅ a = b ⋅ a + c ⋅ a" begin text ‹p 86, ll 20--28› notation additive.inverse (‹- _› [66] 65) abbreviation subtraction (infixl ‹-› 65) where "a - b ≡ a + (- b)" (* or, alternatively, a definition *) end (* ring *) text ‹p 87, ll 10--12› locale subring = additive: subgroup S R "(+)" 𝟬 + multiplicative: submonoid S R "(⋅)" 𝟭 for S and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) context ring begin text ‹p 88, ll 26--28› lemma right_zero [simp]: assumes [simp]: "a ∈ R" shows "a ⋅ 𝟬 = 𝟬" proof - have "a ⋅ 𝟬 = a ⋅ (𝟬 + 𝟬)" by simp also have "… = a ⋅ 𝟬 + a ⋅ 𝟬" by (simp add: distributive del: additive.left_unit additive.right_unit) finally have "a ⋅ 𝟬 - a ⋅ 𝟬 = a ⋅ 𝟬 + a ⋅ 𝟬 - a ⋅ 𝟬" by simp then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel) qed text ‹p 88, l 29› lemma left_zero [simp]: assumes [simp]: "a ∈ R" shows "𝟬 ⋅ a = 𝟬" proof - have "𝟬 ⋅ a = (𝟬 + 𝟬) ⋅ a" by simp also have "… = 𝟬 ⋅ a + 𝟬 ⋅ a" by (simp add: distributive del: additive.left_unit additive.right_unit) finally have "𝟬 ⋅ a - 𝟬 ⋅ a = 𝟬 ⋅ a + 𝟬 ⋅ a - 𝟬 ⋅ a" by simp then show ?thesis by (simp add: additive.associative del: additive.invertible_left_cancel) qed text ‹p 88, ll 29--30; p 89, ll 1--2› lemma left_minus: assumes [simp]: "a ∈ R" "b ∈ R" shows "(- a) ⋅ b = - a ⋅ b" proof - have "𝟬 = 𝟬 ⋅ b" by simp also have "… = (a - a) ⋅ b" by simp also have "… = a ⋅ b + (- a) ⋅ b" by (simp add: distributive del: additive.invertible_right_inverse) finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + (- a) ⋅ b" by (simp add: additive.associative del: additive.invertible_left_inverse) then show ?thesis by simp qed text ‹p 89, l 3› lemma right_minus: assumes [simp]: "a ∈ R" "b ∈ R" shows "a ⋅ (- b) = - a ⋅ b" proof - have "𝟬 = a ⋅ 𝟬" by simp also have "… = a ⋅ (b - b)" by simp also have "… = a ⋅ b + a ⋅ (- b)" by (simp add: distributive del: additive.invertible_right_inverse) finally have "- a ⋅ b + 𝟬 = - a ⋅ b + a ⋅ b + a ⋅ (- b)" by (simp add: additive.associative del: additive.invertible_left_inverse) then show ?thesis by simp qed end (* ring *) subsection ‹Ideals, Quotient Rings› text ‹p 101, ll 2--5› locale ring_congruence = ring + additive: group_congruence R "(+)" 𝟬 E + multiplicative: monoid_congruence R "(⋅)" 𝟭 E for E begin text ‹p 101, ll 2--5› notation additive.quotient_composition (infixl ‹[+]› 65) notation additive.quotient.inverse (‹[-] _› [66] 65) notation multiplicative.quotient_composition (infixl ‹[⋅]› 70) text ‹p 101, ll 5--11› sublocale quotient: ring "R / E" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" by unfold_locales (auto simp: additive.Class_commutes_with_composition additive.associative additive.commutative multiplicative.Class_commutes_with_composition distributive elim!: additive.quotient_ClassE) end (* ring_congruence *) text ‹p 101, ll 12--13› locale subgroup_of_additive_group_of_ring = additive: subgroup I R "(+)" 𝟬 + ring R "(+)" "(⋅)" 𝟬 𝟭 for I and R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) begin text ‹p 101, ll 13--14› definition "Ring_Congruence = {(a, b). a ∈ R ∧ b ∈ R ∧ a - b ∈ I}" text ‹p 101, ll 13--14› lemma Ring_CongruenceI: "⟦ a - b ∈ I; a ∈ R; b ∈ R ⟧ ⟹ (a, b) ∈ Ring_Congruence" using Ring_Congruence_def by blast text ‹p 101, ll 13--14› lemma Ring_CongruenceD: "(a, b) ∈ Ring_Congruence ⟹ a - b ∈ I" using Ring_Congruence_def by blast text ‹ Jacobson's definition of ring congruence deviates from that of group congruence; this complicates the proof. › text ‹p 101, ll 12--14› sublocale additive: subgroup_of_abelian_group I R "(+)" 𝟬 (* implies normal_subgroup *) rewrites additive_congruence: "additive.Congruence = Ring_Congruence" proof - show "subgroup_of_abelian_group I R (+) 𝟬" using additive.commutative additive.invertible_right_inverse2 by unfold_locales auto then interpret additive: subgroup_of_abelian_group I R "(+)" 𝟬 . { fix a b assume [simp]: "a ∈ R" "b ∈ R" have "a - b ∈ I ⟷ - (a - b) ∈ I" by auto also have "… ⟷ - a + b ∈ I" by (simp add: additive.commutative additive.inverse_composition_commute) finally have "a - b ∈ I ⟷ - a + b ∈ I" . } then show "additive.Congruence = Ring_Congruence" unfolding additive.Congruence_def Ring_Congruence_def by auto qed text ‹p 101, l 14› notation additive.Left_Coset (infixl ‹+|› 65) end (* subgroup_of_additive_group_of_ring *) text ‹Def 2.2› text ‹p 101, ll 21--22› locale ideal = subgroup_of_additive_group_of_ring + assumes ideal: "⟦ a ∈ R; b ∈ I ⟧ ⟹ a ⋅ b ∈ I" "⟦ a ∈ R; b ∈ I ⟧ ⟹ b ⋅ a ∈ I" context subgroup_of_additive_group_of_ring begin text ‹p 101, ll 14--17› theorem multiplicative_congruence_implies_ideal: assumes "monoid_congruence R (⋅) 𝟭 Ring_Congruence" shows "ideal I R (+) (⋅) 𝟬 𝟭" proof - interpret multiplicative: monoid_congruence R "(⋅)" 𝟭 Ring_Congruence by fact show ?thesis proof fix a b assume [simp]: "a ∈ R" "b ∈ I" have congs: "(a, a) ∈ Ring_Congruence" "(b, 𝟬) ∈ Ring_Congruence" by (auto simp: additive.ClassD additive.Class_unit_normal_subgroup) from congs have "(a ⋅ b, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce then show "a ⋅ b ∈ I" using additive.Class_unit_normal_subgroup by blast from congs have "(b ⋅ a, 𝟬) ∈ Ring_Congruence" using multiplicative.cong by fastforce then show "b ⋅ a ∈ I" using additive.Class_unit_normal_subgroup by blast qed qed end (* subgroup_of_additive_group_of_ring *) context ideal begin text ‹p 101, ll 17--20› theorem multiplicative_congruence [intro]: assumes a: "(a, a') ∈ Ring_Congruence" and b: "(b, b') ∈ Ring_Congruence" shows "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" proof - note Ring_CongruenceI [intro] Ring_CongruenceD [dest] from a b have [simp]: "a ∈ R" "a' ∈ R" "b ∈ R" "b' ∈ R" by auto from a have [simp]: "a - a' ∈ I" .. have "a ⋅ b - a' ⋅ b = (a - a') ⋅ b" by (simp add: distributive left_minus) also have "… ∈ I" by (simp add: ideal) finally have ab: "a ⋅ b - a' ⋅ b ∈ I" . ― ‹ll 18--19› from b have [simp]: "b - b' ∈ I" .. have "a' ⋅ b - a' ⋅ b' = a' ⋅ (b - b')" by (simp add: distributive right_minus) also have "… ∈ I" by (simp add: ideal) finally have a'b': "a' ⋅ b - a' ⋅ b' ∈ I" . ― ‹l 19› have "a ⋅ b - a' ⋅ b' = (a ⋅ b - a' ⋅ b) + (a' ⋅ b - a' ⋅ b')" by (simp add: additive.associative) (simp add: additive.associative [symmetric]) also have "… ∈ I" using ab a'b' by simp finally show "(a ⋅ b, a' ⋅ b') ∈ Ring_Congruence" by auto ― ‹ll 19--20› qed text ‹p 101, ll 23--24› sublocale ring_congruence where E = Ring_Congruence by unfold_locales rule end (* ideal *) context ring begin text ‹Pulled out of @{locale ideal} to achieve standard notation.› text ‹p 101, ll 24--26› abbreviation Quotient_Ring (infixl ‹'/'/› 75) where "S // I ≡ S / (subgroup_of_additive_group_of_ring.Ring_Congruence I R (+) 𝟬)" end (* ring *) text ‹p 101, ll 24--26› locale quotient_ring = ideal begin text ‹p 101, ll 24--26› sublocale quotient: ring "R // I" "([+])" "([⋅])" "additive.Class 𝟬" "additive.Class 𝟭" .. text ‹p 101, l 26› lemmas Left_Coset = additive.Left_CosetE text ‹Equation 17 (1)› text ‹p 101, l 28› lemmas quotient_addition = additive.factor_composition text ‹Equation 17 (2)› text ‹p 101, l 29› theorem quotient_multiplication [simp]: "⟦ a ∈ R; b ∈ R ⟧ ⟹ (a +| I) [⋅] (b +| I) = a ⋅ b +| I" using multiplicative.Class_commutes_with_composition additive.Class_is_Left_Coset by auto text ‹p 101, l 30› lemmas quotient_zero = additive.factor_unit lemmas quotient_negative = additive.factor_inverse end (* quotient_ring *) subsection ‹Homomorphisms of Rings. Basic Theorems› text ‹Def 2.3› text ‹p 106, ll 7--9› locale ring_homomorphism = map η R R' + source: ring R "(+)" "(⋅)" 𝟬 𝟭 + target: ring R' "(+')" "(⋅')" "𝟬'" "𝟭'" + additive: group_homomorphism η R "(+)" 𝟬 R' "(+')" "𝟬'" + multiplicative: monoid_homomorphism η R "(⋅)" 𝟭 R' "(⋅')" "𝟭'" for η and 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' (‹𝟭''›) text ‹p 106, l 17› locale ring_epimorphism = ring_homomorphism + surjective_map η R R' text ‹p 106, ll 14--18› sublocale quotient_ring ⊆ natural: ring_epimorphism where η = additive.Class and R' = "R // I" and addition' = "([+])" and multiplication' = "([⋅])" and zero' = "additive.Class 𝟬" and unit' = "additive.Class 𝟭" .. context ring_homomorphism begin text ‹ Jacobson reasons via @{term "a - b ∈ additive.Ker"} being a congruence; we prefer the direct proof, since it is very simple. › text ‹p 106, ll 19--21› sublocale kernel: ideal where I = additive.Ker by unfold_locales (auto simp: additive.Ker_image multiplicative.commutes_with_composition) end (* ring_homomorphism *) text ‹p 106, l 22› locale ring_monomorphism = ring_homomorphism + injective_map η R R' context ring_homomorphism begin text ‹p 106, ll 21--23› theorem ring_monomorphism_iff_kernel_unit: "ring_monomorphism η R (+) (⋅) 𝟬 𝟭 R' (+') (⋅') 𝟬' 𝟭' ⟷ additive.Ker = {𝟬}" (is "?monom ⟷ ?ker") proof assume ?monom then interpret ring_monomorphism . show ?ker by (simp add: additive.injective_iff_kernel_unit [symmetric]) next assume ?ker then show ?monom by unfold_locales (simp add: additive.injective_iff_kernel_unit) qed end (* ring_homomorphism *) text ‹p 106, ll 23--25› sublocale ring_homomorphism ⊆ image: subring "η ` R" R' "(+')" "(⋅')" "𝟬'" "𝟭'" .. text ‹p 106, ll 26--27› locale ideal_in_kernel = ring_homomorphism + contained: ideal I R "(+)" "(⋅)" 𝟬 𝟭 for I + assumes subset: "I ⊆ additive.Ker" begin text ‹p 106, ll 26--27› notation contained.additive.quotient_composition (infixl ‹[+]› 65) notation contained.multiplicative.quotient_composition (infixl ‹[⋅]› 70) text ‹Provides @{text additive.induced}, which Jacobson calls $\bar{\eta}$.› text ‹p 106, l 30› sublocale additive: normal_subgroup_in_kernel η R "(+)" 𝟬 R' "(+')" "𝟬'" I rewrites "normal_subgroup.Congruence I R addition zero = contained.Ring_Congruence" by unfold_locales (rule subset contained.additive_congruence)+ text ‹Only the multiplicative part needs some work.› text ‹p 106, ll 27--30› sublocale induced: ring_homomorphism additive.induced "R // I" "([+])" "([⋅])" "contained.additive.Class 𝟬" "contained.additive.Class 𝟭" using contained.multiplicative.Class_commutes_with_composition by unfold_locales (auto elim!: contained.additive.Left_CosetE simp: contained.additive.Class_is_Left_Coset multiplicative.commutes_with_composition multiplicative.commutes_with_unit) text ‹p 106, l 30; p 107, ll 1--3› text ‹ @{term additive.induced} denotes Jacobson's $\bar{\eta}$. We have the commutativity of the diagram, where @{term additive.induced} is unique: @{thm [display] additive.factorization} @{thm [display] additive.uniqueness} › end (* ideal_in_kernel *) text ‹Fundamental Theorem of Homomorphisms of Rings› text ‹p 107, l 6› locale ring_homomorphism_fundamental = ring_homomorphism begin text ‹p 107, l 6› notation kernel.additive.quotient_composition (infixl ‹[+]› 65) notation kernel.multiplicative.quotient_composition (infixl ‹[⋅]› 70) text ‹p 107, l 6› sublocale ideal_in_kernel where I = additive.Ker by unfold_locales rule text ‹p 107, ll 8--9› sublocale natural: ring_epimorphism where η = kernel.additive.Class and R' = "R // additive.Ker" and addition' = "kernel.additive.quotient_composition" and multiplication' = "kernel.multiplicative.quotient_composition" and zero' = "kernel.additive.Class 𝟬" and unit' = "kernel.additive.Class 𝟭" .. text ‹p 107, l 9› sublocale induced: ring_monomorphism where η = additive.induced and R = "R // additive.Ker" and addition = "kernel.additive.quotient_composition" and multiplication = "kernel.multiplicative.quotient_composition" and zero = "kernel.additive.Class 𝟬" and unit = "kernel.additive.Class 𝟭" by unfold_locales (simp add: additive.induced_inj_on) end (* ring_homomorphism_fundamental *) text ‹p 107, l 11› locale ring_isomorphism = ring_homomorphism + bijective_map η R R' begin text ‹p 107, l 11› sublocale ring_monomorphism .. sublocale ring_epimorphism .. text ‹p 107, l 11› lemma inverse_ring_isomorphism: "ring_isomorphism (restrict (inv_into R η) R') R' (+') (⋅') 𝟬' 𝟭' R (+) (⋅) 𝟬 𝟭" using additive.commutes_with_composition [symmetric] additive.commutes_with_unit multiplicative.commutes_with_composition [symmetric] multiplicative.commutes_with_unit surjective by unfold_locales auto end (* ring_isomorphsim *) text ‹p 107, l 11› definition isomorphic_as_rings (infixl ‹≅⇩_{R}› 50) where "ℛ ≅⇩_{R}ℛ' ⟷ (let (R, addition, multiplication, zero, unit) = ℛ; (R', addition', multiplication', zero', unit') = ℛ' in (∃η. ring_isomorphism η R addition multiplication zero unit R' addition' multiplication' zero' unit'))" text ‹p 107, l 11› lemma isomorphic_as_rings_symmetric: "(R, addition, multiplication, zero, unit) ≅⇩_{R}(R', addition', multiplication', zero', unit') ⟹ (R', addition', multiplication', zero', unit') ≅⇩_{R}(R, addition, multiplication, zero, unit)" by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism) context ring_homomorphism begin text ‹Corollary› text ‹p 107, ll 11--12› theorem image_is_isomorphic_to_quotient_ring: "∃K add mult zero one. ideal K R (+) (⋅) 𝟬 𝟭 ∧ (η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩_{R}(R // K, add, mult, zero, one)" proof - interpret image: ring_homomorphism_fundamental where R' = "η ` R" by unfold_locales (auto simp: target.additive.commutative additive.commutes_with_composition multiplicative.commutes_with_composition target.distributive multiplicative.commutes_with_unit) have "ring_isomorphism image.additive.induced (R // additive.Ker) ([+]) ([⋅]) (kernel.additive.Class 𝟬) (kernel.additive.Class 𝟭) (η ` R) (+') (⋅') 𝟬' 𝟭'" by unfold_locales (simp add: image.additive.induced_image bij_betw_def) then have "(η ` R, (+'), (⋅'), 𝟬', 𝟭') ≅⇩_{R}(R // additive.Ker, ([+]), ([⋅]), kernel.additive.Class 𝟬, kernel.additive.Class 𝟭)" by (simp add: isomorphic_as_rings_def) (meson ring_isomorphism.inverse_ring_isomorphism) moreover have "ideal additive.Ker R (+) (⋅) 𝟬 𝟭" .. ultimately show ?thesis by blast qed end (* ring_homomorphism *) end