<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal direct sum is proved. We referred to [23], [22], [8] and [18] in the formalization.</p></abstract>

In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal direct sum is proved. We referred to [23], [22], [8] and [18] in the formalization.

Definition and Properties of Direct Sum Decomposition of Groups<xref ref-type="fn" rid="fn1_w2aab2b8b6b1b7b1ab1aaAa"><sup>1</sup></xref>

Formalized Mathematics

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

Definition and Properties of Direct Sum Decomposition of Groups

In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its...

Definition and Properties of Direct Sum Decomposition of Groups¹

Data publikacji: 31 mar 2015

Zakres stron: 15 - 27

Otrzymano: 31 gru 2014

DOI: https://doi.org/10.2478/forma-2015-0002

Słowa kluczowe
group theory, direct sum decomposition

© Kazuhisa Nakasho et al.

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

Definition and Properties of Direct Sum Decomposition of Groups1

Data publikacji: 31 mar 2015

Zakres stron: 15 - 27

Otrzymano: 31 gru 2014

DOI: https://doi.org/10.2478/forma-2015-0002

Słowa kluczowegroup theory, direct sum decomposition

© Kazuhisa Nakasho et al.

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

Definition and Properties of Direct Sum Decomposition of Groups¹

Słowa kluczowe
group theory, direct sum decomposition