Theory Ring_Theory
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)"
end
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
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
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 "(+)" 𝟬
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
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
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" .
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" .
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
qed
text ‹p 101, ll 23--24›
sublocale ring_congruence where E = Ring_Congruence by unfold_locales rule
end
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
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
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
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
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
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
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
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
end