# 满-单分解　`prop.pretopos-factorization`
预拓扑斯中的满-单分解
layer 16 · 命题 · 拓扑斯 · 范畴论
[在星图里打开](../#n=prop.pretopos-factorization)　·　[节点索引](../index.md)

设 $\mathcal{C}$ 是预拓扑斯。则

1. $\mathcal{C}$ 是**平衡的**：既单又满的态射一定是同构；
2. 每个态射都是**严格的**：$\operatorname{im} f \cong \operatorname{coim} f$；
3. 每个态射都有**唯一**的满-单分解
> 陈述续见 [nodes/prop.pretopos-factorization.2.md](./prop.pretopos-factorization.2.md)


## 为什么成立（入边，证明在 proofs/）
- …另有入边，续页见 [nodes/prop.pretopos-factorization.3.md](./prop.pretopos-factorization.3.md)

refs: Le Stum, An introduction to condensed mathematics, §3.3

## 说明
这三条在 $\mathbf{Set}$ 里都理所当然，但在一般范畴里都要证。它们合起来说：「**预拓扑斯里的像 = 商**」，与集合里「像就是按核对取商」完全一致。证明见边上那条推导。

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