Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/15427
Tytuł: | Internal Direct Products and the Universal Property of Direct Product Groups |
Autorzy: | Nelson, Alexander M. |
Słowa kluczowe: | direct product of groups |
Data wydania: | 2023 |
Data dodania: | 30-paź-2023 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 31, Issue 1, Pages 101-120 |
Abstrakt: | This is a “quality of life” article concerning product groups, using the Mizar system [2], [4]. Like a Sonata, this article consists of three movements. 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. The second act introduces the universal property of products and its consequences as found in, e.g., Kurosh [7]. 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 [5], as well as quotients of product groups. The third act introduces the notion of an internal direct product. Isaacs [6] 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 [3], Aschbacher [1], and Robinson [11]) are already formalized in the heroic work of Nakasho, Okazaki, Yamazaki, and Shimada [9], [8]. 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 [10]. |
Afiliacja: | Los Angeles, California, United States of America |
URI: | http://hdl.handle.net/11320/15427 |
DOI: | 10.2478/forma-2023-0010 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2023 The Author(s) CC BY-SA 3.0 license |
Występuje w kolekcji(ach): | Formalized Mathematics, 2023, Volume 31, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2023-0010.pdf | 313,83 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL