Given natural numbers , we could construct integers by considering the equivalence relation on as follows,
- if for some
Obviously, it’s a equivalence relation from properties of commutativity. Thus we have equivalence class where . Then, , and . This construction from a commutative monoid to abelian group is called Grothendieck group.
Consider , where for some set . Let with , . Let and , and . We also write as . We could find that is a initial -algebra.
Define “plus” with respect to on as follows,
where and . We will abuse the notation instead of and use as . Acturally, is a monoid. Though, it’s not commutative, and we can’t apply the construction of Grothendieck group.
We could define an inverse element to extend the . Let , we define as its reverse list which could be defined in functional programming like Haskell as
foldl (flip (:)) , as the last element of xs, as the initial element of xs, as the list without the initial element of xs, as the list without the last element.
Finally, define elements on with one more field, that is, where and . We could extend the “plus” as
- if ,
- otherwise. the later “plus” ignores the sign field.
However, we could show that every element in has an inverse element and this new type is a free group generated by elements of . Thus, is , and is where is a unit type has only one element. Note that for , there is no difference with .
Is there any differences between and constructed by Grothendieck group ?