# 可表示性的下降　`lem.representable-quotient`
可表示性的下降引理
layer 14 · 引理 · 拓扑斯 · 范畴论
[在星图里打开](../#n=lem.representable-quotient)　·　[节点索引](../index.md)

设 $\mathcal{T}$ 是拓扑斯（配标准拓扑）。若层之间的满态射

$$\coprod_{i \in I} F_{i} \longrightarrow F$$

中每个 $F_{i}$ 以及每个 $F_{i} \times_{F} F_{j}$ 都**可表示**，则 $F$ 也可表示。

## 为什么成立（入边，证明在 proofs/）
- [`def.representable`](../nodes/def.representable.md) 表示函子：用到了定义 表示函子　[proofs/def-dep.representable-quotient.md](../proofs/def-dep.representable-quotient.md)

- …另有入边，续页见 [nodes/lem.representable-quotient.2.md](./lem.representable-quotient.2.md)

## 它能推出什么 / 谁在用它
- …另有出边，续页见 [nodes/lem.representable-quotient.3.md](./lem.representable-quotient.3.md)

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

> 说明见 `notes/lem.representable-quotient.md`

引用：`lem.representable-quotient`（内容 v0.9.0）· 条款见 [LICENSE.txt](../LICENSE.txt)