# 全忠实函子本质单射　`prop.fully-faithful-injective`
命题：$F$ 全忠实 $\implies$ $F(X) \cong F(Y)$ 则 $X \cong Y$
layer 10 · 命题 · 函子与自然变换 · 范畴论
[在星图里打开](../#n=prop.fully-faithful-injective)　·　[节点索引](../index.md)

若 $F : \mathcal{C} \to \mathcal{D}$ **全忠实**，则它**本质单射**：

$$F(X) \cong F(Y) \implies X \cong Y.$$

## 为什么成立（入边，证明在 proofs/）
- [`def.ff-faithful`](../nodes/def.ff-faithful.md) 忠实 / 满 / 全忠实：用到了定义 忠实 / 满 / 全忠实　[proofs/def-link.ffinj-ff.md](../proofs/def-link.ffinj-ff.md)

refs: Le Stum, An introduction to condensed mathematics, Exercise 1.17

> 说明见 `notes/prop.fully-faithful-injective.md`

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