Theory Group_Family_Product

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

theory Group_Family_Product
  imports Group_Theory
begin

text ‹The external direct product of a family of groups @{term "G i"} (@{term "i ∈ I"}): the carrier is
  the ∗‹extensional› dependent function space @{term "PiE I G"} --- functions defined on @{term I} with
  @{term "x i ∈ G i"} for each index --- with pointwise composition and unit.  This generalises the binary
  external direct product of theory ‹Group_Product› to an arbitrary index set, mirroring ‹product_group› of
  ‹HOL-Algebra.Product_Groups› but in the locale idiom.›

subsection ‹The product locale›

text ‹A family of groups indexed by @{term I}: for each @{term "i ∈ I"} a carrier @{term "G i"} with
  composition @{term "comp i"} and unit @{term "unit i"} forming a ‹comp_group›.›
locale group_family =
  fixes I :: "'i set"
    and G :: "'i ⇒ 'a set"
    and comp :: "'i ⇒ 'a ⇒ 'a ⇒ 'a"
    and unit :: "'i ⇒ 'a"
  assumes comp_group: "⋀i. i ∈ I ⟹ Group (G i) (comp i) (unit i)"
begin

subsection ‹Carrier, composition and unit›

text ‹The product carrier: extensional functions @{term x} on @{term I} with @{term "x i ∈ G i"}.›
definition Pcarrier :: "('i ⇒ 'a) set" (‹∏G›)
  where "∏G = (ΠE i∈I. G i)"

text ‹Pointwise composition (extensional on @{term I}).›
definition Pcomp :: "('i ⇒ 'a) ⇒ ('i ⇒ 'a) ⇒ ('i ⇒ 'a)" (infixl ‹⊗Π› 70)
  where "x ⊗Π y = (λi∈I. comp i (x i) (y i))"

text ‹The pointwise unit.›
definition Punit :: "'i ⇒ 'a" (‹𝟭Π›)
  where "𝟭Π = (λi∈I. unit i)"

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

lemma Pcarrier_mem_component: "⟦ x ∈ ∏G; i ∈ I ⟧ ⟹ x i ∈ G i"      
  by (auto simp: Pcarrier_def PiE_iff)

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

lemma Pcomp_closed [intro, simp]:
  assumes "x ∈ ∏G" and "y ∈ ∏G" shows "x ⊗Π y ∈ ∏G"
proof (rule Pcarrier_memI)
  fix i assume i: "i ∈ I"
  interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
  show "(x ⊗Π y) i ∈ G i"
    using assms i by (auto simp: Pcomp_def Pcarrier_mem_component)
qed (auto simp: Pcomp_def)

lemma Punit_closed [iff]: "𝟭Π ∈ ∏G"
  using Group_def Monoid.unit_closed Pcarrier_def Punit_def comp_group by fastforce

lemma Pcomp_apply: "i ∈ I ⟹ (x ⊗Π y) i = comp i (x i) (y i)"
  by (simp add: Pcomp_def)

lemma Punit_apply: "i ∈ I ⟹ 𝟭Π i = unit i"
  by (simp add: Punit_def)

subsection ‹The product is a group›

text ‹Two members of the product agree iff they agree componentwise on @{term I} (both being
  extensional).›
lemma Pcarrier_eqI:
  assumes "x ∈ ∏G" and "y ∈ ∏G" and "⋀i. i ∈ I ⟹ x i = y i"
  shows "x = y"
  using assms by (metis Pcarrier_extensional extensionalityI)

theorem Group_Pcarrier: "Group ∏G (⊗Π) 𝟭Π"
proof (rule GroupI)
  show "⋀x y. x ∈ ∏G ⟹ y ∈ ∏G ⟹ x ⊗Π y ∈ ∏G" by (rule Pcomp_closed)
  show "𝟭Π ∈ ∏G" by (rule Punit_closed)
next
  fix x y z assume xyz: "x ∈ ∏G" "y ∈ ∏G" "z ∈ ∏G"
  show "(x ⊗Π y) ⊗Π z = x ⊗Π (y ⊗Π z)"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
    show "((x ⊗Π y) ⊗Π z) i = (x ⊗Π (y ⊗Π z)) i"
      using xyz i by (simp add: Pcomp_apply Pcarrier_mem_component Gi.associative)
  qed (use xyz in auto)
next
  fix x assume x: "x ∈ ∏G"
  show "𝟭Π ⊗Π x = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
    show "(𝟭Π ⊗Π x) i = x i"
      using x i by (simp add: Pcomp_apply Punit_apply Pcarrier_mem_component)
  qed (use x in auto)
next
  fix x assume x: "x ∈ ∏G"
  show "x ⊗Π 𝟭Π = x"
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
    show "(x ⊗Π 𝟭Π) i = x i"
      using x i by (simp add: Pcomp_apply Punit_apply Pcarrier_mem_component)
  qed (use x in auto)
next
  fix x assume x: "x ∈ ∏G"
  ― ‹The inverse is the pointwise inverse.›
  ― ‹Choose a two-sided inverse in each factor.›
  have "∃v. ∀i∈I. v i ∈ G i ∧ comp i (x i) (v i) = unit i ∧ comp i (v i) (x i) = unit i"
  proof (intro bchoice ballI)
    fix i assume i: "i ∈ I"
    interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
    have xi: "x i ∈ G i" using x i by (rule Pcarrier_mem_component)
    then have "Gi.invertible (x i)" by simp
    then show "∃v. v ∈ G i ∧ comp i (x i) v = unit i ∧ comp i v (x i) = unit i"
      using xi by (auto simp: Gi.invertible_def)
  qed
  then obtain v where v: "⋀i. i ∈ I ⟹ v i ∈ G i
        ∧ comp i (x i) (v i) = unit i ∧ comp i (v i) (x i) = unit i" by blast
  show "∃y ∈ ∏G. x ⊗Π y = 𝟭Π ∧ y ⊗Π x = 𝟭Π"
  proof
    define y where "y = (λi∈I. v i)"
    have yi: "y i = v i" if "i ∈ I" for i using that by (simp add: y_def)
    show yG: "y ∈ ∏G"
      by (rule Pcarrier_memI) (use v in ‹auto simp: y_def›)
    have "x ⊗Π y = 𝟭Π ∧ y ⊗Π x = 𝟭Π"
    proof (intro conjI Pcarrier_eqI Punit_closed Pcomp_closed x yG)
      fix i assume i: "i ∈ I"
      show "(x ⊗Π y) i = 𝟭Π i" "(y ⊗Π x) i = 𝟭Π i"
        using v[OF i] i by (simp_all add: Pcomp_apply Punit_apply yi)
    qed
    then show "x ⊗Π y = 𝟭Π ∧ y ⊗Π x = 𝟭Π" .
  qed
qed

sublocale product: Group Pcarrier "(⊗Π)" Punit
  by (rule Group_Pcarrier)

subsection ‹Projections are homomorphisms›

text ‹The projection onto the @{term i}th factor is a ‹comp_group› homomorphism from the product onto
  @{term "G i"}.›
definition Pproj :: "'i ⇒ ('i ⇒ 'a) ⇒ 'a"
  where "Pproj i = restrict (λx. x i) ∏G"

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

lemma Pproj_hom:
  assumes i: "i ∈ I"
  shows "group_homomorphism (Pproj i) ∏G (⊗Π) 𝟭Π (G i) (comp i) (unit i)"
proof -
  interpret Gi: Group "G i" "comp i" "unit i" using i by (rule comp_group)
  have graph: "Pproj i ∈ ∏G →E G i"
    by (simp add: Pcarrier_def PiE_mem Pproj_def i)
  show ?thesis
  proof 
  qed (use i in ‹auto simp: graph Pproj_apply Punit_apply Pcomp_apply›)
qed

end

subsection ‹The product of a family of abelian groups is abelian›

locale abelian_group_family = group_family +
  assumes abelian: "⋀i. i ∈ I ⟹ Abelian_Group (G i) (comp i) (unit i)"
begin

theorem abelian_group_Pcarrier: "Abelian_Group ∏G (⊗Π) 𝟭Π"
proof (rule Abelian_Group.intro)
  show "Group ∏G (⊗Π) 𝟭Π" by (rule Group_Pcarrier)
  ― ‹The product operation is commutative, so the (already-established) monoid is commutative.›
  have comm: "x ⊗Π y = y ⊗Π x" if xy: "x ∈ ∏G" "y ∈ ∏G" for x y
  proof (rule Pcarrier_eqI)
    fix i assume i: "i ∈ I"
    interpret Gi: Abelian_Group "G i" "comp i" "unit i" using i by (rule abelian)
    show "(x ⊗Π y) i = (y ⊗Π x) i"
      using xy i by (simp add: Pcomp_apply Pcarrier_mem_component Gi.commutative)
  qed (use xy in auto)
  show "commutative_monoid ∏G (⊗Π) 𝟭Π"
    by (simp add: comm commutative_monoid_axioms.intro commutative_monoid_def product.Monoid_axioms)
qed

end

end