Semidirect Products of Groups

Alexander M. Nelson

doi:10.2478/forma-2025-0006

.blurhash-client-img { display: none !important; }

Semidirect Products of Groups

Formalized Mathematics

Volume 33 (2025): Issue 1 (September 2025)

By: Alexander M. Nelson

Open Access

|Dec 2025

Abstract

We formalize the semidirect product of groups in Mizar, following §10 of Aschbacher’s Finite Group Theory [2]. We also prove the universal property for semidirect products as found in Bourbaki [5, III §2.10] Proposition 27. In an appendix, we define the dihedral group of the regular n-gon and the infinite dihedral group.

References

Goulnara Arzhantseva and Światosław R. Gal. On approximation properties of semidirect products of groups. Annales Mathématiques Blaise Pascal, 27(1):1–24, 2020. doi:10.5802/ambp.386.
Search in Google Scholar Back to article
Michael Aschbacher. Finite Group Theory, volume 10. Cambridge University Press, 2000.
Search in Google Scholar Back to article
Clia Borlido and Mai Gehrke. Substitution principle and semidirect products. Mathematical Structures in Computer Science, 33(6):486–535, 2023. doi:10.1017/S0960129523000294.
Search in Google Scholar Back to article
Nicolas Bourbaki. Elements of Mathematics. Algebra I. Chapters 1-3. Springer-Verlag, Berlin, Heidelberg, New York, London, Paris, Tokyo, 1989.
Search in Google Scholar Back to article
Nicolas Bourbaki. General Topology: Chapters 1–4. Springer Science and Business Media, 2013.
Search in Google Scholar Back to article
Peteris Daugulis. Nonuniqueness of semidirect decompositions for semidirect products with directly decomposable factors and applications for dihedral groups. Algebra and Discrete Mathematics, 23(2):204–215, 2017.
Search in Google Scholar Back to article
David S. Dummit and Richard M. Foote. Abstract Algebra. Wiley and Sons, Third edition, 2004.
Search in Google Scholar Back to article
Wolfgang Gaschütz. Zu einem von B. H. und H. Neumann gestellten Problem. Mathematische Nachrichten, 14(4–6):249–252, 1955. doi:10.1002/mana.19550140406.
Search in Google Scholar Back to article
Craig R. Guilbault, Brendan Burns Healy, and Brian Pietsch. Group boundaries for semi-direct products with ℤ. Groups, Geometry, and Dynamics, 2024. doi:10.4171/GGD/750.
Search in Google Scholar Back to article
Scott Harper and Peiran Wu. Classifying the groups of order pq in Lean. arXiv preprint arXiv:2501.09769, 2025.
Search in Google Scholar Back to article
I. Martin Isaacs. Finite Group Theory, volume 92 of Graduate Studies in Mathematics. American Mathematical Society, 2008.
Search in Google Scholar Back to article
Vipul Kakkar and Ratan Lal. Automorphisms of semidirect products fixing the non-normal subgroup. Jordan Journal of Mathematics and Statistics, 17(2):241–248, 2024. doi:10.47013/17.2.5.
Search in Google Scholar Back to article
Artur Korniłowicz. On the group of inner automorphisms. Formalized Mathematics, 5 (1):43–45, 1996.
Search in Google Scholar Back to article
Artur Korniłowicz. The product of the families of the groups. Formalized Mathematics, 7(1):127–134, 1998.
Search in Google Scholar Back to article
Alexander M. Nelson. Internal direct products and the universal property of direct product groups. Formalized Mathematics, 31(1):101–120, 2023. doi:10.2478/forma-2023-0010.
Search in Google Scholar Back to article
Colin Rothgang, Artur Korniłowicz, and Florian Rabe. A new export of the Mizar Mathematical Library. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 205–210, Cham, 2021. Springer International Publishing. doi:10.1007/978-3-030-81097-9 17.
Search in Google Scholar Back to article