Theory Module_Family_Product

section ‹The direct product and direct sum of a family of modules›

theory Module_Family_Product
  imports Module_Homomorphism
begin

no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax

text ‹The external direct product of a family of @{term R}-modules @{term "Mod i"} (@{term "i ∈ I"}): the
  carrier is the extensional dependent function space @{term "Pi⇩E I Mod"} with pointwise addition and
  scaling.  As with the homomorphism locale, the scalar ring @{term R} is fixed ∗‹once› and shared by all
  the modules.  We show the product is an @{term R}-module, the projections are module homomorphisms, and
  the direct ∗‹sum› (elements of finite support) is a submodule of the product.›

subsection ‹The product locale›

locale module_family =
  base: Ring R "(+)" "(⋅)" 𝟬 𝟭
  for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›) +
  fixes I :: "'i set"
    and Mod :: "'i ⇒ 'b set"
    and madd :: "'i ⇒ 'b ⇒ 'b ⇒ 'b"
    and mzero :: "'i ⇒ 'b"
    and scale :: "'i ⇒ 'a ⇒ 'b ⇒ 'b"
  assumes mod: "⋀i. i ∈ I ⟹
      Module R (+) (⋅) 𝟬 𝟭 (madd i) (mzero i) (Mod i) (scale i)"
begin

lemma comp_module: "i ∈ I ⟹ Module R (+) (⋅) 𝟬 𝟭 (madd i) (mzero i) (Mod i) (scale i)"
  by (rule mod)

subsection ‹Carrier and operations›

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

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

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

definition Pscale :: "'a ⇒ ('i ⇒ 'b) ⇒ ('i ⇒ 'b)" (infixr ‹⊙⇩Π› 75)
  where "a ⊙⇩Π x = (λi∈I. scale i a (x i))"

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

lemma Pcarrier_component: "⟦ x ∈ Pcarrier; i ∈ I ⟧ ⟹ x i ∈ Mod 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 = madd i (x i) (y i)" 
  by (simp add: Padd_def)

lemma Pzero_apply: "i ∈ I ⟹ 𝟬⇩Π i = mzero i" 
  by (simp add: Pzero_def)

lemma Pscale_apply: "i ∈ I ⟹ (a ⊙⇩Π x) i = scale i a (x i)" 
  by (simp add: Pscale_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 Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
    using i by (rule mod)
  show "(x ⊕⇩Π y) i ∈ Mod i" using assms i by (simp add: Padd_apply Pcarrier_component)
qed (auto simp: Padd_def)

lemma Pzero_closed [intro, simp]: "𝟬⇩Π ∈ Pcarrier"
  using Pcarrier_def Pzero_def mod Module.mzero_closed by fastforce

lemma Pscale_closed [intro, simp]:
  assumes "a ∈ R" and "x ∈ Pcarrier" shows "a ⊙⇩Π x ∈ Pcarrier"
  using Pcarrier_def Pscale_def mod Module.scale_closed assms by fastforce

subsection ‹The additive abelian group of the product›

lemma Padd_abelian_group: "Abelian_Group Pcarrier (⊕⇩Π) 𝟬⇩Π"
proof (rule Abelian_Group.intro)
  show 0: "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 Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
        using i by (rule mod)
      show "((x ⊕⇩Π y) ⊕⇩Π z) i = (x ⊕⇩Π (y ⊕⇩Π z)) i"
        using xyz i by (simp add: Padd_apply Pcarrier_component Mi.madd.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 Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
        using i by (rule mod)
      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"
    show "x ⊕⇩Π 𝟬⇩Π = x"
    proof (rule Pcarrier_eqI)
      fix i assume i: "i ∈ I"
      interpret Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
        using i by (rule mod)
      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"
    have "∃v. ∀i∈I. v i ∈ Mod i ∧ madd i (x i) (v i) = mzero i ∧ madd i (v i) (x i) = mzero i"
    proof (rule bchoice, intro ballI)
      fix i assume i: "i ∈ I"
      interpret Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
        using i by (rule mod)
      show "∃v. v ∈ Mod i ∧ madd i (x i) v = mzero i ∧ madd i v (x i) = mzero i"
        using Mi.madd.Monoid_axioms Monoid.invertible_inverse_closed Pcarrier_component i x
        by fastforce
    qed
    then obtain v where v: "⋀i. i ∈ I ⟹ v i ∈ Mod i
          ∧ madd i (x i) (v i) = mzero i ∧ madd i (v i) (x i) = mzero i" by blast
    show "∃y ∈ Pcarrier. x ⊕⇩Π y = 𝟬⇩Π ∧ y ⊕⇩Π x = 𝟬⇩Π"
    proof
      define y where "y = (λi∈I. v i)"
      show yP: "y ∈ Pcarrier" by (rule Pcarrier_memI) (use v in ‹auto simp: y_def›)
      show "x ⊕⇩Π y = 𝟬⇩Π ∧ y ⊕⇩Π x = 𝟬⇩Π"
        using Padd_def Pzero_def y_def v by auto
    qed
  qed
  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 "0" Group_def Monoid.associative xyz by fastforce
    next
      fix x assume x: "x ∈ Pcarrier"
      show "𝟬⇩Π ⊕⇩Π x = x"
        by (meson "0" Group_def Monoid.left_unit x)
      show "x ⊕⇩Π 𝟬⇩Π = x"
        by (meson Group_def Monoid.right_unit 0 x)
    qed auto
    show "commutative_monoid_axioms Pcarrier (⊕⇩Π)"
    proof 
      fix x y assume xy: "x ∈ Pcarrier" "y ∈ Pcarrier"
      show "x ⊕⇩Π y = y ⊕⇩Π x"
      proof (intro Pcarrier_eqI)
        fix i assume i: "i ∈ I"
        interpret Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
          using i by (rule mod)
        show "(x ⊕⇩Π y) i = (y ⊕⇩Π x) i"
          using xy i by (simp add: Padd_apply Pcarrier_component Mi.madd.commutative)
      qed (use xy in auto)
    qed
  qed
qed

subsection ‹The product is a module›

theorem module_Pcarrier: "Module R (+) (⋅) 𝟬 𝟭 (⊕⇩Π) 𝟬⇩Π Pcarrier (⊙⇩Π)"
proof (intro Module.intro Module_axioms.intro base.Ring_axioms Padd_abelian_group)
    fix a x assume "a ∈ R" "x ∈ Pcarrier" then show "a ⊙⇩Π x ∈ Pcarrier" by (rule Pscale_closed)
  next
    fix a x y assume a: "a ∈ R" and xy: "x ∈ Pcarrier" "y ∈ Pcarrier"
    show "a ⊙⇩Π (x ⊕⇩Π y) = (a ⊙⇩Π x) ⊕⇩Π (a ⊙⇩Π y)"
    proof (rule Pcarrier_eqI)
      fix i assume i: "i ∈ I"
      interpret Mi: Module R "(+)" "(⋅)" 𝟬 𝟭 "madd i" "mzero i" "Mod i" "scale i"
        using i by (rule mod)
      show "(a ⊙⇩Π (x ⊕⇩Π y)) i = ((a ⊙⇩Π x) ⊕⇩Π (a ⊙⇩Π y)) i"
        using a xy i by (simp add: Pscale_apply Padd_apply Pcarrier_component Mi.scale_distrib_madd)
    qed (use a xy in auto)
  next
    fix a b x assume ab: "a ∈ R" "b ∈ R" and x: "x ∈ Pcarrier"
    then show "(a + b) ⊙⇩Π x = (a ⊙⇩Π x) ⊕⇩Π (b ⊙⇩Π x)"
      using Pcarrier_component Pscale_apply mod 
      by (fastforce intro!: Pcarrier_eqI simp: Padd_apply Module.scale_distrib_add)+
    show "(a ⋅ b) ⊙⇩Π x = a ⊙⇩Π (b ⊙⇩Π x)"
      using Pcarrier_component Pscale_apply ab mod Module.scale_scale x
      by (fastforce intro!: Pcarrier_eqI)
  next
    fix x assume "x ∈ Pcarrier"
    then show "𝟭 ⊙⇩Π x = x"
      using Pcarrier_component Pscale_apply mod Module.scale_one
      by (fastforce intro!: Pcarrier_eqI)
qed

sublocale product: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕⇩Π)" Pzero Pcarrier "(⊙⇩Π)"
  by (rule module_Pcarrier)

subsection ‹Projections›

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

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

text ‹Each projection is additive and commutes with scaling (it is a module homomorphism onto the
  factor @{term "Mod i"}); we record the two defining equations.›
lemma Pproj_add: "⟦ i ∈ I; x ∈ Pcarrier; y ∈ Pcarrier ⟧ ⟹ Pproj i (x ⊕⇩Π y) = madd i (Pproj i x) (Pproj i y)"
  by (simp add: Pproj_apply Padd_apply)

lemma Pproj_scale: "⟦ i ∈ I; a ∈ R; x ∈ Pcarrier ⟧ ⟹ Pproj i (a ⊙⇩Π x) = scale i a (Pproj i x)"
  by (simp add: Pproj_apply Pscale_apply)

subsection ‹The direct sum›

text ‹The ∗‹direct sum› consists of the product elements of ∗‹finite support›: those @{term x} equal to the
  zero element in all but finitely many factors.  It is a submodule of the product.›
definition Psum :: "('i ⇒ 'b) set"
  where "Psum = {x ∈ Pcarrier. finite {i ∈ I. x i ≠ mzero i}}"

lemma Psum_subset: "Psum ⊆ Pcarrier" 
  by (auto simp: Psum_def)

lemma Psum_memI:
  "⟦ x ∈ Pcarrier; finite {i ∈ I. x i ≠ mzero i} ⟧ ⟹ x ∈ Psum"
  by (simp add: Psum_def)

theorem Psum_submodule: "product.submodule Psum"
proof (rule product.submoduleI)
  show "Psum ⊆ Pcarrier" by (rule Psum_subset)
next
  show "𝟬⇩Π ∈ Psum" using Pzero_closed
    by (simp add: Psum_memI Pzero_def)
next
  fix x y assume x: "x ∈ Psum" and y: "y ∈ Psum"
  have xP: "x ∈ Pcarrier" and yP: "y ∈ Pcarrier" using x y by (auto simp: Psum_def)
      ― ‹The support of a sum is contained in the union of the supports.›
  have "⋀i. ⟦i ∈ I; y i = mzero i; x i = mzero i⟧ ⟹ (x ⊕⇩Π y) i = mzero i"
    by (metis Padd_apply Pzero_apply product.madd.left_unit xP)
  then have "{i ∈ I. (x ⊕⇩Π y) i ≠ mzero i} ⊆ {i ∈ I. x i ≠ mzero i} ∪ {i ∈ I. y i ≠ mzero i}"
    by auto
  moreover have "finite ({i ∈ I. x i ≠ mzero i} ∪ {i ∈ I. y i ≠ mzero i})"
    using x y by (auto simp: Psum_def)
  ultimately show "x ⊕⇩Π y ∈ Psum" using xP yP Psum_memI finite_subset by blast
next
  fix a x assume a: "a ∈ R" and x: "x ∈ Psum"
  have xP: "x ∈ Pcarrier" using x by (simp add: Psum_def)
  ― ‹Scaling can only shrink the support.›
  have "⋀i. ⟦i ∈ I; x i = mzero i⟧ ⟹ (a ⊙⇩Π x) i = mzero i"
    by (metis Pscale_apply Pzero_apply a product.scale_zero_elem)
  then have "{i ∈ I. (a ⊙⇩Π x) i ≠ mzero i} ⊆ {i ∈ I. x i ≠ mzero i}"
    by auto
  moreover have "finite {i ∈ I. x i ≠ mzero i}" using x by (simp add: Psum_def)
  ultimately have "finite {i ∈ I. (a ⊙⇩Π x) i ≠ mzero i}" by (rule finite_subset)
  then show "a ⊙⇩Π x ∈ Psum" using a xP by (auto intro: Psum_memI)
qed

end

end