Homotopy Type Theory module > history (Rev #6)

Definiton

Let $A$ be an abelian group, let $R$ be a commutative ring. $A$ is an $R$-module if it comes with an abelian group homomorphism $\alpha:R \to (A \to A)$ such that

• $\alpha(1) = id_A$

• for all $a:R$ and $b:R$, $\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)$

Properties

Every abelian group is a $\mathbb{Z}$-module.

See also

• abelian group
• graded module