# 拓扑空间上的常层就是离散空间的层　`prop.constant-sheaf-top`
命题：$\widetilde{E}_{\mathbf{Top}} \cong \underline{E^{\mathrm{disc}}}$
layer 17 · 命题 · 层与拓扑 · 范畴论
[在星图里打开](../#n=prop.constant-sheaf-top)　·　[节点索引](../index.md)

设 $E$ 是集合。则 $\mathbf{Top}$ 上的**常层**就是**离散空间** $E$ 所给出的层：

$$\widetilde{E}_{\mathbf{Top}} \;\cong\; \underline{E^{\mathrm{disc}}},$$

并且 $\widetilde{E}_{\mathbf{Top}}(X) = E$ $\iff$ $X$ **连通**。

## 它能推出什么 / 谁在用它
- ⇒ [`prop.topos-morphism-final-map`](../nodes/prop.topos-morphism-final-map.md) 终映射给出的拓扑斯态射

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

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

> 说明见 `notes/prop.constant-sheaf-top.md`

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