Theory Ring_Family_Product

section ‹The direct product of an indexed family of rings›

theory Ring_Family_Product
  imports Ring_Theory
begin

text ‹The external direct product of a family of rings @{term "R i"} (@{term "i ∈ I"}): the carrier is the
  extensional dependent function space @{term "Pi⇩E I R"}, with pointwise addition, multiplication, zero and
  one.  This mirrors the indexed group product but for rings; its commutative and field-of-components
  refinements follow.  (A product of fields is ∗‹not› a field in general --- it has zero divisors as soon as
  @{term I} has more than one element --- so only the commutative-ring refinement is offered.)›

subsection ‹The product locale›

locale ring_family =
  fixes I :: "'i set"
    and R :: "'i ⇒ 'a set"
    and add :: "'i ⇒ 'a ⇒ 'a ⇒ 'a"
    and mult :: "'i ⇒ 'a ⇒ 'a ⇒ 'a"
    and zero :: "'i ⇒ 'a"
    and one :: "'i ⇒ 'a"
  assumes ring: "⋀i. i ∈ I ⟹ Ring (R i) (add i) (mult i) (zero i) (one i)"
begin

lemma comp_ring: "i ∈ I ⟹ Ring (R i) (add i) (mult i) (zero i) (one i)"
  by (rule ring)

subsection ‹Carrier and operations›

definition Pcarrier :: "('i ⇒ 'a) set"
  where "Pcarrier = (Π⇩E i∈I. R i)"

definition Padd :: "('i ⇒ 'a) ⇒ ('i ⇒ 'a) ⇒ ('i ⇒ 'a)" (infixl ‹⊕⇩Π› 65)
  where "x ⊕⇩Π y = (λi∈I. add i (x i) (y i))"

definition Pmult :: "('i ⇒ 'a) ⇒ ('i ⇒ 'a) ⇒ ('i ⇒ 'a)" (infixl ‹⊙⇩Π› 70)
  where "x ⊙⇩Π y = (λi∈I. mult i (x i) (y i))"

definition Pzero :: "'i ⇒ 'a" (‹𝟬⇩Π›)
  where "𝟬⇩Π = (λi∈I. zero i)"

definition Pone :: "'i ⇒ 'a" (‹𝟭⇩Π›)
  where "𝟭⇩Π = (λi∈I. one i)"

lemma Pcarrier_memI:
  "⟦ ⋀i. i ∈ I ⟹ x i ∈ R i; x ∈ extensional I ⟧ ⟹ x ∈ Pcarrier"
  by (auto simp: Pcarrier_def PiE_iff)

lemma Pcarrier_component: "⟦ x ∈ Pcarrier; i ∈ I ⟧ ⟹ x i ∈ R i"
  by (auto simp: Pcarrier_def PiE_iff)

lemma Pcarrier_extensional: "x ∈ Pcarrier ⟹ x ∈ extensional I"
  by (auto simp: Pcarrier_def PiE_iff)

lemma Pcarrier_eqI:
  "⟦ x ∈ Pcarrier; y ∈ Pcarrier; ⋀i. i ∈ I ⟹ x i = y i ⟧ ⟹ x = y"
  by (metis Pcarrier_extensional extensionalityI)

lemma Padd_apply: "i ∈ I ⟹ (x ⊕⇩Π y) i = add i (x i) (y i)" by (simp add: Padd_def)
lemma Pmult_apply: "i ∈ I ⟹ (x ⊙⇩Π y) i = mult i (x i) (y i)" by (simp add: Pmult_def)
lemma Pzero_apply: "i ∈ I ⟹ 𝟬⇩Π i = zero i" by (simp add: Pzero_def)
lemma Pone_apply: "i ∈ I ⟹ 𝟭⇩Π i = one i" by (simp add: Pone_def)

lemma Padd_closed [intro, simp]:
  assumes "x ∈ Pcarrier" "y ∈ Pcarrier" shows "x ⊕⇩Π y ∈ Pcarrier"
proof (rule Pcarrier_memI)
  fix i assume i: "i ∈ I"
  interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
  show "(x ⊕⇩Π y) i ∈ R i" using assms i by (simp add: Padd_apply Pcarrier_component)
qed (auto simp: Padd_def)

lemma Pmult_closed [intro, simp]:
  assumes "x ∈ Pcarrier" "y ∈ Pcarrier" shows "x ⊙⇩Π y ∈ Pcarrier"
proof (rule Pcarrier_memI)
  fix i assume i: "i ∈ I"
  interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
  show "(x ⊙⇩Π y) i ∈ R i" using assms i by (simp add: Pmult_apply Pcarrier_component)
qed (auto simp: Pmult_def)

lemma Pzero_closed [intro, simp]: "𝟬⇩Π ∈ Pcarrier"
proof (rule Pcarrier_memI)
  fix i assume i: "i ∈ I"
  interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
  show "𝟬⇩Π i ∈ R i" using i by (simp add: Pzero_apply)
qed (auto simp: Pzero_def)

lemma Pone_closed [intro, simp]: "𝟭⇩Π ∈ Pcarrier"
proof (rule Pcarrier_memI)
  fix i assume i: "i ∈ I"
  interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
  show "𝟭⇩Π i ∈ R i" using i by (simp add: Pone_apply)
qed (auto simp: Pone_def)

subsection ‹The additive abelian group›

lemma additive_group: "Group Pcarrier (⊕⇩Π) 𝟬⇩Π"
proof (intro GroupI Pzero_closed Padd_closed)
  fix x y z assume xyz: "x ∈ Pcarrier" "y ∈ Pcarrier" "z ∈ Pcarrier"
  show "(x ⊕⇩Π y) ⊕⇩Π z = x ⊕⇩Π (y ⊕⇩Π z)"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "((x ⊕⇩Π y) ⊕⇩Π z) i = (x ⊕⇩Π (y ⊕⇩Π z)) i"
      using xyz i by (simp add: Padd_apply Pcarrier_component Ri.additive.associative)
  qed (use xyz in auto)
next
  fix x assume x: "x ∈ Pcarrier"
  show "𝟬⇩Π ⊕⇩Π x = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "(𝟬⇩Π ⊕⇩Π x) i = x i"
      by (simp add: Padd_apply Pcarrier_component Pzero_def i x)
  qed (use x in auto)
  show "x ⊕⇩Π 𝟬⇩Π = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "(x ⊕⇩Π 𝟬⇩Π) i = x i"
      using x i by (simp add: Padd_apply Pzero_apply Pcarrier_component)
  qed (use x in auto)
next
  fix x assume x: "x ∈ Pcarrier"
  note [[unify_search_bound=10]]  ―‹for the two following meson calls›
  have "∃v. v i ∈ R i ∧ add i (x i) (v i) = zero i ∧ add i (v i) (x i) = zero i" if i: "i ∈ I" for i
  proof -
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show ?thesis
      by (meson Pcarrier_component Ri.additive.invertible Ri.additive.invertibleE i x)
  qed
  then obtain v where v: "⋀i. i ∈ I ⟹ v i ∈ R i
          ∧ add i (x i) (v i) = zero i ∧ add i (v i) (x i) = zero i" by meson
  define y where "y = (λi∈I. v i)"
  have "x ⊕⇩Π y = 𝟬⇩Π ∧ y ⊕⇩Π x = 𝟬⇩Π"
    using Padd_def Pzero_def ‹y ≡ restrict v I› v by auto
  then show "∃y ∈ Pcarrier. x ⊕⇩Π y = 𝟬⇩Π ∧ y ⊕⇩Π x = 𝟬⇩Π"
    using Pcarrier_def v y_def by auto
qed

lemma additive_abelian_group: "Abelian_Group Pcarrier (⊕⇩Π) 𝟬⇩Π"
proof (intro Abelian_Group.intro additive_group)
  show "commutative_monoid Pcarrier (⊕⇩Π) 𝟬⇩Π"
  proof (rule commutative_monoid.intro)
    show "Monoid Pcarrier (⊕⇩Π) 𝟬⇩Π"
    proof 
      fix x y z assume xyz: "x ∈ Pcarrier" "y ∈ Pcarrier" "z ∈ Pcarrier"
      show "(x ⊕⇩Π y) ⊕⇩Π z = x ⊕⇩Π (y ⊕⇩Π z)"
        using Group_def Monoid.associative additive_group xyz by fastforce
    next
      fix x assume x: "x ∈ Pcarrier"
      show "𝟬⇩Π ⊕⇩Π x = x"
        by (meson Group_def Monoid.left_unit additive_group x)
      show "x ⊕⇩Π 𝟬⇩Π = x"
        by (meson Group_def Monoid.right_unit additive_group x)
    qed auto
    show "commutative_monoid_axioms Pcarrier (⊕⇩Π)"
    proof 
      fix x y assume xy: "x ∈ Pcarrier" "y ∈ Pcarrier"
      show "x ⊕⇩Π y = y ⊕⇩Π x"
      proof (rule Pcarrier_eqI)
        fix i assume i: "i ∈ I"
        interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
        show "(x ⊕⇩Π y) i = (y ⊕⇩Π x) i"
          using xy i by (simp add: Padd_apply Pcarrier_component Ri.additive.commutative)
      qed (use xy in auto)
    qed
  qed
qed

subsection ‹The multiplicative monoid›

lemma multiplicative_monoid: "Monoid Pcarrier (⊙⇩Π) 𝟭⇩Π"
proof (unfold_locales)
  show "⋀x y. x ∈ Pcarrier ⟹ y ∈ Pcarrier ⟹ x ⊙⇩Π y ∈ Pcarrier" by (rule Pmult_closed)
  show "𝟭⇩Π ∈ Pcarrier" by (rule Pone_closed)
next
  fix x y z assume xyz: "x ∈ Pcarrier" "y ∈ Pcarrier" "z ∈ Pcarrier"
  show "(x ⊙⇩Π y) ⊙⇩Π z = x ⊙⇩Π (y ⊙⇩Π z)"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "((x ⊙⇩Π y) ⊙⇩Π z) i = (x ⊙⇩Π (y ⊙⇩Π z)) i"
      using xyz i by (simp add: Pmult_apply Pcarrier_component Ri.multiplicative.associative)
  qed (use xyz in auto)
next
  fix x assume x: "x ∈ Pcarrier"
  show "𝟭⇩Π ⊙⇩Π x = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "(𝟭⇩Π ⊙⇩Π x) i = x i"
      using x i by (simp add: Pmult_apply Pone_apply Pcarrier_component)
  qed (use x in auto)
next
  fix x assume x: "x ∈ Pcarrier"
  show "x ⊙⇩Π 𝟭⇩Π = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
    show "(x ⊙⇩Π 𝟭⇩Π) i = x i"
      using x i by (simp add: Pmult_apply Pone_apply Pcarrier_component)
  qed (use x in auto)
qed

subsection ‹The product is a ring›

theorem Ring_Pcarrier: "Ring Pcarrier (⊕⇩Π) (⊙⇩Π) 𝟬⇩Π 𝟭⇩Π"
proof (rule Ring.intro)
  show "Abelian_Group Pcarrier (⊕⇩Π) 𝟬⇩Π" by (rule additive_abelian_group)
  show "Monoid Pcarrier (⊙⇩Π) 𝟭⇩Π" by (rule multiplicative_monoid)
  show "Ring_axioms Pcarrier (⊕⇩Π) (⊙⇩Π)"
  proof
    fix x y z assume xyz: "x ∈ Pcarrier" "y ∈ Pcarrier" "z ∈ Pcarrier"
    show "x ⊙⇩Π (y ⊕⇩Π z) = x ⊙⇩Π y ⊕⇩Π (x ⊙⇩Π z)"
    proof (rule Pcarrier_eqI)
      fix i assume i: "i ∈ I"
      interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
      show "(x ⊙⇩Π (y ⊕⇩Π z)) i = (x ⊙⇩Π y ⊕⇩Π (x ⊙⇩Π z)) i"
        using xyz i by (simp add: Pmult_apply Padd_apply Pcarrier_component Ri.distributive)
    qed (use xyz in auto)
    show "(y ⊕⇩Π z) ⊙⇩Π x = y ⊙⇩Π x ⊕⇩Π (z ⊙⇩Π x)"
    proof (rule Pcarrier_eqI)
      fix i assume i: "i ∈ I"
      interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
      show "((y ⊕⇩Π z) ⊙⇩Π x) i = (y ⊙⇩Π x ⊕⇩Π (z ⊙⇩Π x)) i"
        using xyz i by (simp add: Pmult_apply Padd_apply Pcarrier_component Ri.distributive)
    qed (use xyz in auto)
  qed
qed

sublocale product: Ring Pcarrier "(⊕⇩Π)" "(⊙⇩Π)" Pzero Pone
  by (rule Ring_Pcarrier)

subsection ‹Projections are ring homomorphisms›

definition Pproj :: "'i ⇒ ('i ⇒ 'a) ⇒ 'a"
  where "Pproj i = restrict (λx. x i) Pcarrier"

lemma Pproj_apply: "x ∈ Pcarrier ⟹ Pproj i x = x i"
  by (simp add: Pproj_def)

lemma Pproj_hom:
  assumes i: "i ∈ I"
  shows "ring_homomorphism (Pproj i) Pcarrier (⊕⇩Π) (⊙⇩Π) 𝟬⇩Π 𝟭⇩Π
                            (R i) (add i) (mult i) (zero i) (one i)"
proof -
  interpret Ri: Ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule ring)
  have graph: "Pproj i ∈ Pcarrier →⇩E R i"
    by (simp add: Pcarrier_component Pproj_def i)
  show ?thesis
  proof 
  qed (use i in ‹auto simp: graph Pproj_apply Pzero_apply Pone_apply Padd_apply Pmult_apply›)
qed

end

subsection ‹The product of a family of commutative rings is commutative›

locale commutative_ring_family = ring_family +
  assumes comm: "⋀i. i ∈ I ⟹ commutative_ring (R i) (add i) (mult i) (zero i) (one i)"
begin

theorem commutative_ring_Pcarrier: "commutative_ring Pcarrier (⊕⇩Π) (⊙⇩Π) 𝟬⇩Π 𝟭⇩Π"
proof (rule commutative_ring.intro)
  show "Ring Pcarrier (⊕⇩Π) (⊙⇩Π) 𝟬⇩Π 𝟭⇩Π" by (rule Ring_Pcarrier)
  ― ‹The multiplicative monoid is commutative.›
  show "commutative_monoid Pcarrier (⊙⇩Π) 𝟭⇩Π"
  proof (rule commutative_monoid.intro)
    show "Monoid Pcarrier (⊙⇩Π) 𝟭⇩Π" by (rule multiplicative_monoid)
    show "commutative_monoid_axioms Pcarrier (⊙⇩Π)"
    proof
      fix x y assume xy: "x ∈ Pcarrier" "y ∈ Pcarrier"
      show "x ⊙⇩Π y = y ⊙⇩Π x"
      proof (rule Pcarrier_eqI)
        fix i assume i: "i ∈ I"
        interpret Ri: commutative_ring "R i" "add i" "mult i" "zero i" "one i" using i by (rule comm)
        show "(x ⊙⇩Π y) i = (y ⊙⇩Π x) i"
          using xy i by (simp add: Pmult_apply Pcarrier_component Ri.multiplicative.commutative)
      qed (use xy in auto)
    qed
  qed
qed

end

end