Theory Jacobson_Basic_Algebra.Ring_Theory

(*
  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