The free abelian group on a type is the left adjoint of the forgetful functor from abelian groups to types.
The free functor Type u ⥤ AddCommGroup sending a type X to the
free abelian group with generators x : X.
Equations
- AddCommGroup.free = {obj := λ (α : Type u), AddCommGroup.of (free_abelian_group α), map := λ (X Y : Type u), free_abelian_group.map, map_id' := AddCommGroup.free._proof_1, map_comp' := AddCommGroup.free._proof_2}
@[simp]
@[simp]
theorem
AddCommGroup.free_map_coe
{α β : Type u}
{f : α → β}
(x : free_abelian_group α) :
⇑(AddCommGroup.free.map f) x = f <$> x
The free-forgetful adjunction for abelian groups.
Equations
- AddCommGroup.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Type u) (G : AddCommGroup), free_abelian_group.hom_equiv X ↥G, hom_equiv_naturality_left_symm' := AddCommGroup.adj._proof_1, hom_equiv_naturality_right' := AddCommGroup.adj._proof_2}