@ARTICLE{GROUP_23.MIZ,
  AUTHOR = {Nelson, Alexander M.},
  TITLE = {Internal Direct Products and the Universal Property of Direct Product Groups},
  SECTION1 = {Sequences of Group Elements under Homomorphisms},
  SECTION2 = {Preliminary Work about Group-Families and Group-Yielding Many Sorted Sets},
  SECTION3 = {Subgroup-Family of a Family of Groups},
  SECTION4 = {Inclusion Morphism},
  SECTION5 = {Families of Homomorphisms},
  SECTION6 = {Projection Morphisms from Product Group to Direct Factors},
  SECTION7 = {Universal Property of Direct Products of Groups},
  SECTION8 = {Commutator Subgroup and Center of Product Groups},
  SECTION9 = {Quotients of Product Groups},
  SECTION10 = {Internal Direct Products},
  MSC2020 = {20E22},
  DAY = {30},
  MONTH = {June},
  YEAR = {2023},
  ADDRESS1 = {Los Angeles, California, United States of America},
  SUMMARY = {This is a ``quality of life'' article concerning product
  groups. Like a Sonata, this article consists of three movements.\par
  The first act, the slowest of the three, builds the infrastructure
  necessary for the rest of the article. We prove group homomorphisms map
  arbitrary finite products to arbitrary finite products, introduce a notion
  of ``group yielding'' families, as well as families of homomorphisms.
  We close the first act with defining the inclusion morphism of a
  subgroup into its parent group, and the projection morphism of a product
  group onto one of its factors.\par
  The second act introduces the universal property of products and its
  consequences as found in, e.g., Kurosh~\cite{kurosh:1955}.
  Specifically, for the product of an arbitrary family of groups,
  we prove the center of a product group is the product of centers.
  More exciting, we prove for a product of a finite family groups, the
  commutator subgroup of the product is the product of commutator
  subgroups, but this is because in general: the direct sum of commutator
  subgroups is the subgroup of the commutator subgroup of the product group,
  and the commutator subgroup of the product is a subgroup of the product
  of derived subgroups. We conclude this act by proving a few theorems
  concerning the image and kernel of morphisms between product groups, as found in
  Hungerford~\cite{HUNGERFORD}, as well as quotients of product groups.\par
  The third act introduces the notion of an internal direct product.
  Isaacs~\cite{isaacs:2008} points out (paraphrasing with Mizar terminology)
  that the internal direct product is a predicate but the external
  direct product is a [Mizar] functor. To our delight, we find the bulk of the
  ``recognition theorem'' (as stated by Dummit and Foote~\cite{dummit-foote:2004},
  Aschbacher~\cite{aschbacher2000finite}, and Robison~\cite{robinson2012course})
  are already formalized in the heroic work of
  Nakasho, Okazaki, Yamazaki, and Shimada~\cite{GROUP_19.ABS,GROUP_20.ABS}.
  We generalize the notion of an internal product to a set of subgroups,
  proving it is equivalent to the internal product of a family of subgroups.}}

@book{kurosh:1955,
  title={The Theory of Groups},
  author={Kurosh, Aleksandr Gennadievich},
  volume={1},
  year={1955},
  publisher={Chelsea publishing company}
}

@book{dummit-foote:2004,
  title={{Abstract Algebra}},
  author={Dummit, David S and Foote, Richard M},
  edition={{Third}},
  year={2004},
  publisher={Wiley and Sons}
}
@book{isaacs:2008,
  author={Isaacs, I.~Martin},
  title={{Finite Group Theory}},
  year={2008},
  publisher={American Mathematical Society},
  series={Graduate Studies in Mathematics},
  volume={92}
}
@book{aschbacher2000finite,
  title={{Finite Group Theory}},
  author={Aschbacher, Michael},
  volume={10},
  year={2000},
  publisher={Cambridge University Press}
}
