Theory 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)
no_notation uminus ("- _" [81] 80)
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