<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under automorphisms from its parent group. Along the way, we formalize notions of Automorphism and results concerning centralizers. Much of what we formalize may be found sprinkled throughout the literature, in particular Gorenstein [4] and Isaacs [5]. We show all our favorite subgroups turn out to be characteristic: the center, the derived subgroup, the commutator subgroup generated by characteristic subgroups, and the intersection of all subgroups satisfying a generic group property.</p>
</abstract>

We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under automorphisms from its parent group. Along the way, we formalize notions of Automorphism and results concerning centralizers. Much of what we formalize may be found sprinkled throughout the literature, in particular Gorenstein [4] and Isaacs [5]. We show all our favorite subgroups turn out to be characteristic: the center, the derived subgroup, the commutator subgroup generated by characteristic subgroups, and the intersection of all subgroups satisfying a generic group property.

Characteristic Subgroups

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Characteristic Subgroups"}

We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under...

Characteristic Subgroups

Data publikacji: 24 gru 2022

Zakres stron: 79 - 91

Przyjęty: 23 lip 2022

DOI: https://doi.org/10.2478/forma-2022-0007

Słowa kluczowe
group theory, inner automorphisms, characteristic subgroups

© 2022 Alexander M. Nelson, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Characteristic Subgroups

Data publikacji: 24 gru 2022

Zakres stron: 79 - 91

Przyjęty: 23 lip 2022

DOI: https://doi.org/10.2478/forma-2022-0007

Słowa kluczowegroup theory, inner automorphisms, characteristic subgroups

© 2022 Alexander M. Nelson, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
group theory, inner automorphisms, characteristic subgroups