The Mislin genus G(N) of a finitely generated nilpotent group N with finite commutator subgroup admits an abelian group structure. If N satisfies some additional conditions -we say that N belongs to N1- we know exactly the structure of G(N). Considering a direct product N1 x ... x Nk of groups in N1 takes us virtually always out of N1. We here calculate the Mislin genus of such a direct product.
In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.
All crossed products of two cyclic groups are explicitly described using generators and relations. A necessary and sufficient condition for an extension of a group by a group to be a cyclic group is given.