Theorems · Definition · group theory

FreeAbelianGroup

Type u → Type u

If α is a type, then FreeAbelianGroup α is the free abelian group generated by α. This is an abelian group equipped with a function FreeAbelianGroup.of : α → FreeAbelianGroup α which has the following universal property: if G is any abelian group, and f : α → G is any function, then this function is the composite of FreeAbelianGroup.of and a unique group homomorphism FreeAbelianGroup.lift f : FreeAbelianGroup α →+ G. A typical element of FreeAbelianGroup α is a formal sum of elements of α and their formal inverses. For example if x and y are terms of type α then x + x + x - y is a "typical" element of FreeAbelianGroup α. In particular if α is empty then FreeAbelianGroup α is isomorphic to the trivial group, and if α has one term then FreeAbelianGroup α is isomorphic to ℤ. One can think of FreeAbelianGroup α as the functions α →₀ ℤ with finite support, and addition given pointwise. TODO: rename to FreeAddCommGroup and introduce a multiplicative version

Defined in

Mathlib.GroupTheory.FreeAbelianGroup

Cited by

82 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound