Theory Ring

(* Title:  ZF/ex/Ring.thy

*)

section ‹Rings›

theory Ring imports Group begin

no_notation
  cadd  (infixl ‹⊕› 65) and
  cmult  (infixl ‹⊗› 70)

(*First, we must simulate a record declaration:
record ring = monoid +
  add :: "[i, i] ⇒ i" (infixl "⊕ı" 65)
  zero :: i ("𝟬ı")
*)

definition
  add_field :: "i ⇒ i" where
  "add_field(M) = fst(snd(snd(snd(M))))"

definition
  ring_add :: "[i, i, i] ⇒ i" (infixl ‹⊕ı› 65) where
  "ring_add(M,x,y) = add_field(M) ` ⟨x,y⟩"

definition
  zero :: "i ⇒ i" (‹𝟬ı›) where
  "zero(M) = fst(snd(snd(snd(snd(M)))))"


lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
  by (simp add: add_field_def)

lemma add_eq [simp]: "ring_add(<C,M,I,A,z>, x, y) = A ` ⟨x,y⟩"
  by (simp add: ring_add_def)

lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
  by (simp add: zero_def)


text ‹Derived operations.›

definition
  a_inv :: "[i,i] ⇒ i" (‹⊖ı _› [81] 80) where
  "a_inv(R) ≡ m_inv (<carrier(R), add_field(R), zero(R), 0>)"

definition
  minus :: "[i,i,i] ⇒ i" (‹(_ ⊖ı _)› [65,66] 65) where
  "⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹ x ⊖⇘R⇙ y = x ⊕⇘R⇙ (⊖⇘R⇙ y)"

locale abelian_monoid = fixes G (structure)
  assumes a_comm_monoid:
    "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"

text ‹
  The following definition is redundant but simple to use.
›

locale abelian_group = abelian_monoid +
  assumes a_comm_group:
    "comm_group (<carrier(G), add_field(G), zero(G), 0>)"

locale ring = abelian_group R + monoid R for R (structure) +
  assumes l_distr: "⟦x ∈ carrier(R); y ∈ carrier(R); z ∈ carrier(R)⟧
      ⟹ (x ⊕ y) ⋅ z = x ⋅ z ⊕ y ⋅ z"
    and r_distr: "⟦x ∈ carrier(R); y ∈ carrier(R); z ∈ carrier(R)⟧
      ⟹ z ⋅ (x ⊕ y) = z ⋅ x ⊕ z ⋅ y"

locale cring = ring + comm_monoid R

locale "domain" = cring +
  assumes one_not_zero [simp]: "𝟭 ≠ 𝟬"
    and integral: "⟦a ⋅ b = 𝟬; a ∈ carrier(R); b ∈ carrier(R)⟧ ⟹
                  a = 𝟬 | b = 𝟬"


subsection ‹Basic Properties›

lemma (in abelian_monoid) a_monoid:
     "monoid (<carrier(G), add_field(G), zero(G), 0>)"
apply (insert a_comm_monoid)
apply (simp add: comm_monoid_def)
done

lemma (in abelian_group) a_group:
     "group (<carrier(G), add_field(G), zero(G), 0>)"
apply (insert a_comm_group)
apply (simp add: comm_group_def group_def)
done


lemma (in abelian_monoid) l_zero [simp]:
     "x ∈ carrier(G) ⟹ 𝟬 ⊕ x = x"
apply (insert monoid.l_one [OF a_monoid])
apply (simp add: ring_add_def)
done

lemma (in abelian_monoid) zero_closed [intro, simp]:
     "𝟬 ∈ carrier(G)"
by (rule monoid.one_closed [OF a_monoid, simplified])

lemma (in abelian_group) a_inv_closed [intro, simp]:
     "x ∈ carrier(G) ⟹ ⊖ x ∈ carrier(G)"
by (simp add: a_inv_def  group.inv_closed [OF a_group, simplified])

lemma (in abelian_monoid) a_closed [intro, simp]:
     "⟦x ∈ carrier(G); y ∈ carrier(G)⟧ ⟹ x ⊕ y ∈ carrier(G)"
by (rule monoid.m_closed [OF a_monoid,
                  simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) minus_closed [intro, simp]:
     "⟦x ∈ carrier(G); y ∈ carrier(G)⟧ ⟹ x ⊖ y ∈ carrier(G)"
by (simp add: minus_def)

lemma (in abelian_group) a_l_cancel [simp]:
     "⟦x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)⟧
      ⟹ (x ⊕ y = x ⊕ z) ⟷ (y = z)"
by (rule group.l_cancel [OF a_group,
             simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) a_r_cancel [simp]:
     "⟦x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)⟧
      ⟹ (y ⊕ x = z ⊕ x) ⟷ (y = z)"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_assoc:
  "⟦x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)⟧
   ⟹ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_group) l_neg:
     "x ∈ carrier(G) ⟹ ⊖ x ⊕ x = 𝟬"
by (simp add: a_inv_def
     group.l_inv [OF a_group, simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_comm:
     "⟦x ∈ carrier(G); y ∈ carrier(G)⟧ ⟹ x ⊕ y = y ⊕ x"
by (rule comm_monoid.m_comm [OF a_comm_monoid,
    simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) a_lcomm:
     "⟦x ∈ carrier(G); y ∈ carrier(G); z ∈ carrier(G)⟧
      ⟹ x ⊕ (y ⊕ z) = y ⊕ (x ⊕ z)"
by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
    simplified, simplified ring_add_def [symmetric]])

lemma (in abelian_monoid) r_zero [simp]:
     "x ∈ carrier(G) ⟹ x ⊕ 𝟬 = x"
  using monoid.r_one [OF a_monoid]
  by (simp add: ring_add_def [symmetric])

lemma (in abelian_group) r_neg:
     "x ∈ carrier(G) ⟹ x ⊕ (⊖ x) = 𝟬"
  using group.r_inv [OF a_group]
  by (simp add: a_inv_def ring_add_def [symmetric])

lemma (in abelian_group) minus_zero [simp]:
     "⊖ 𝟬 = 𝟬"
  by (simp add: a_inv_def
    group.inv_one [OF a_group, simplified ])

lemma (in abelian_group) minus_minus [simp]:
     "x ∈ carrier(G) ⟹ ⊖ (⊖ x) = x"
  using group.inv_inv [OF a_group, simplified]
  by (simp add: a_inv_def)

lemma (in abelian_group) minus_add:
     "⟦x ∈ carrier(G); y ∈ carrier(G)⟧ ⟹ ⊖ (x ⊕ y) = ⊖ x ⊕ ⊖ y"
  using comm_group.inv_mult [OF a_comm_group]
  by (simp add: a_inv_def ring_add_def [symmetric])

lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm

text ‹
  The following proofs are from Jacobson, Basic Algebra I, pp.¬88--89
›

context ring
begin

lemma l_null [simp]: "x ∈ carrier(R) ⟹ 𝟬 ⋅ x = 𝟬"
proof -
  assume R: "x ∈ carrier(R)"
  then have "𝟬 ⋅ x ⊕ 𝟬 ⋅ x = (𝟬 ⊕ 𝟬) ⋅ x"
    by (blast intro: l_distr [THEN sym])
  also from R have "... = 𝟬 ⋅ x ⊕ 𝟬" by simp
  finally have "𝟬 ⋅ x ⊕ 𝟬 ⋅ x = 𝟬 ⋅ x ⊕ 𝟬" .
  with R show ?thesis by (simp del: r_zero)
qed

lemma r_null [simp]: "x ∈ carrier(R) ⟹ x ⋅ 𝟬 = 𝟬"
proof -
  assume R: "x ∈ carrier(R)"
  then have "x ⋅ 𝟬 ⊕ x ⋅ 𝟬 = x ⋅ (𝟬 ⊕ 𝟬)"
    by (simp add: r_distr del: l_zero r_zero)
  also from R have "... = x ⋅ 𝟬 ⊕ 𝟬" by simp
  finally have "x ⋅ 𝟬 ⊕ x ⋅ 𝟬 = x ⋅ 𝟬 ⊕ 𝟬" .
  with R show ?thesis by (simp del: r_zero)
qed

lemma l_minus:
  "⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹ ⊖ x ⋅ y = ⊖ (x ⋅ y)"
proof -
  assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
  then have "(⊖ x) ⋅ y ⊕ x ⋅ y = (⊖ x ⊕ x) ⋅ y" by (simp add: l_distr)
  also from R have "... = 𝟬" by (simp add: l_neg)
  finally have "(⊖ x) ⋅ y ⊕ x ⋅ y = 𝟬" .
  with R have "(⊖ x) ⋅ y ⊕ x ⋅ y ⊕ ⊖ (x ⋅ y) = 𝟬 ⊕ ⊖ (x ⋅ y)" by simp
  with R show ?thesis by (simp add: a_assoc r_neg)
qed

lemma r_minus:
  "⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹ x ⋅ ⊖ y = ⊖ (x ⋅ y)"
proof -
  assume R: "x ∈ carrier(R)" "y ∈ carrier(R)"
  then have "x ⋅ (⊖ y) ⊕ x ⋅ y = x ⋅ (⊖ y ⊕ y)" by (simp add: r_distr)
  also from R have "... = 𝟬" by (simp add: l_neg)
  finally have "x ⋅ (⊖ y) ⊕ x ⋅ y = 𝟬" .
  with R have "x ⋅ (⊖ y) ⊕ x ⋅ y ⊕ ⊖ (x ⋅ y) = 𝟬 ⊕ ⊖ (x ⋅ y)" by simp
  with R show ?thesis by (simp add: a_assoc r_neg)
qed

lemma minus_eq:
  "⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹ x ⊖ y = x ⊕ ⊖ y"
  by (simp only: minus_def)

end


subsection ‹Morphisms›

definition
  ring_hom :: "[i,i] ⇒ i" where
  "ring_hom(R,S) ≡
    {h ∈ carrier(R) -> carrier(S).
      (∀x y. x ∈ carrier(R) ∧ y ∈ carrier(R) ⟶
        h ` (x ⋅⇘R⇙ y) = (h ` x) ⋅⇘S⇙ (h ` y) ∧
        h ` (x ⊕⇘R⇙ y) = (h ` x) ⊕⇘S⇙ (h ` y)) ∧
      h ` 𝟭⇘R⇙ = 𝟭⇘S⇙}"

lemma ring_hom_memI:
  assumes hom_type: "h ∈ carrier(R) → carrier(S)"
    and hom_mult: "⋀x y. ⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹
      h ` (x ⋅⇘R⇙ y) = (h ` x) ⋅⇘S⇙ (h ` y)"
    and hom_add: "⋀x y. ⟦x ∈ carrier(R); y ∈ carrier(R)⟧ ⟹
      h ` (x ⊕⇘R⇙ y) = (h ` x) ⊕⇘S⇙ (h ` y)"
    and hom_one: "h ` 𝟭⇘R⇙ = 𝟭⇘S⇙"
  shows "h ∈ ring_hom(R,S)"
by (auto simp add: ring_hom_def assms)

lemma ring_hom_closed:
     "⟦h ∈ ring_hom(R,S); x ∈ carrier(R)⟧ ⟹ h ` x ∈ carrier(S)"
by (auto simp add: ring_hom_def)

lemma ring_hom_mult:
     "⟦h ∈ ring_hom(R,S); x ∈ carrier(R); y ∈ carrier(R)⟧
      ⟹ h ` (x ⋅⇘R⇙ y) = (h ` x) ⋅⇘S⇙ (h ` y)"
by (simp add: ring_hom_def)

lemma ring_hom_add:
     "⟦h ∈ ring_hom(R,S); x ∈ carrier(R); y ∈ carrier(R)⟧
      ⟹ h ` (x ⊕⇘R⇙ y) = (h ` x) ⊕⇘S⇙ (h ` y)"
by (simp add: ring_hom_def)

lemma ring_hom_one: "h ∈ ring_hom(R,S) ⟹ h ` 𝟭⇘R⇙ = 𝟭⇘S⇙"
by (simp add: ring_hom_def)

locale ring_hom_cring = R: cring R + S: cring S
  for R (structure) and S (structure) and h +
  assumes homh [simp, intro]: "h ∈ ring_hom(R,S)"
  notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
    and hom_mult [simp] = ring_hom_mult [OF homh]
    and hom_add [simp] = ring_hom_add [OF homh]
    and hom_one [simp] = ring_hom_one [OF homh]

lemma (in ring_hom_cring) hom_zero [simp]:
     "h ` 𝟬⇘R⇙ = 𝟬⇘S⇙"
proof -
  have "h ` 𝟬⇘R⇙ ⊕⇘S⇙ h ` 𝟬 = h ` 𝟬⇘R⇙ ⊕⇘S⇙ 𝟬⇘S⇙"
    by (simp add: hom_add [symmetric] del: hom_add)
  then show ?thesis by (simp del: S.r_zero)
qed

lemma (in ring_hom_cring) hom_a_inv [simp]:
     "x ∈ carrier(R) ⟹ h ` (⊖⇘R⇙ x) = ⊖⇘S⇙ h ` x"
proof -
  assume R: "x ∈ carrier(R)"
  then have "h ` x ⊕⇘S⇙ h ` (⊖ x) = h ` x ⊕⇘S⇙ (⊖⇘S⇙ (h ` x))"
    by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
  with R show ?thesis by simp
qed

lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) ∈ ring_hom(R,R)"
apply (rule ring_hom_memI)
apply (auto simp add: id_type)
done

end