# 全忠实沿自身的 Kan 延拓　`prop.kan-extension-fully-faithful`
命题：$p$ 全忠实 $\implies p_{!}F \circ p \cong F$
layer 14 · 命题 · 伴随与反射 · 范畴论
[在星图里打开](../#n=prop.kan-extension-fully-faithful)　·　[节点索引](../index.md)

设 $p : \mathcal{C} \to \mathcal{C}'$ **全忠实**、$\mathcal{D}$ 有余极限。则对每个 $F : \mathcal{C} \to \mathcal{D}$，左 Kan 延拓满足

$$p_{!}F \circ p \;\cong\; F.$$

## 为什么成立（入边，证明在 proofs/）
- …另有入边，续页见 [nodes/prop.kan-extension-fully-faithful.2.md](./prop.kan-extension-fully-faithful.2.md)

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

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

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