## Definition ## For [[abelian group]]s $(A, 0_A, +_A, -_A)$ and $(B, 0_B, +_B, -_B)$ and a function $f:A \to B$, let us define the types $$preservesUnit(f) \coloneqq f(0_A) =_B 0_b$$ $$preservesAddition(f) \coloneqq \prod_{a:A} \prod_{b:A} f(a +_A b) =_B f(a) +_B f(b)$$ $$preservesNegation(f) \coloneqq \prod_{a:A} f(-_A(a)) =_B -_B(f(a))$$ $$isAbGrpHom(f) \coloneqq preservesUnit(f) \times preservesAddition(f) \times preservesNegation(f)$$ $f$ is an __abelian group homomorphism__ if $isAbGrpHom(f)$ has a term. Since an abelian group is a [[set]], the identity types are [[proposition]]s and thus preserved in an abelian group homomorphism. The type of abelian group homomorphisms between abelian groups $A$ and $B$ is defined as $$Hom_{Ab}(A, B) \coloneqq \prod_{f:A\to B} isAbGrpHom(f)$$ ## See also ## * [[abelian group]] * [[Z-algebra]] * [[module]] * [[bilinear function]] category: not redirected to nlab yet