# 交换化　`prop.abelianization`
交换化 $G \mapsto G^{\mathrm{ab}}$ 是左伴随
layer 10 · 命题 · 代数结构 · 抽象代数
[在星图里打开](../#n=prop.abelianization)　·　[节点索引](../index.md)

**交换化**函子

$$(-)^{\mathrm{ab}} : \mathbf{Grp} \longrightarrow \mathbf{Ab}, \qquad G \longmapsto G^{\mathrm{ab}} := G / [G, G]$$

是含入函子 $\mathbf{Ab} \hookrightarrow \mathbf{Grp}$ 的**左伴随**。

## 为什么成立（入边，证明在 proofs/）
- [`def.quotient-group`](../nodes/def.quotient-group.md) 商群：用到了定义 商群　[proofs/def-dep.abelianization-quotient.md](../proofs/def-dep.abelianization-quotient.md)

- …另有入边，续页见 [nodes/prop.abelianization.2.md](./prop.abelianization.2.md)

refs: Le Stum, Exercise 1.9

> 说明见 `notes/prop.abelianization.md`

引用：`prop.abelianization`（内容 v0.9.0）· 条款见 [LICENSE.txt](../LICENSE.txt)