子对象构成有界格

说明

证明。 「子对象」是单态射 $X' \rightarrowtail X$ 的同构类。

• 交取拉回：$X_{1} \cap X_{2} := X_{1} \times_{X} X_{2}$。单态射的拉回仍是单态射 ✓；泛性给出「同时分解过 $X_{1}$ 与 $X_{2}$」$\iff$「分解过拉回」，即它恰是两个子对象的最大下界 ✓。
• 并取像：$X_{1} \cup X_{2} := \operatorname{im}(X_{1} \coprod X_{2} \to X)$。余积的泛性给出「同时被 $X_{1}, X_{2}$ 包含的态射 $\iff$ 从余积出发的态射」，而取像正是把它变成单态射：$X_{1} \to X$ 与 $X_{2} \to X$ 都分解过它，且任何同时包含两者的子对象都被它分解过（像的泛性）—— 恰是最小上界 ✓。（像的存在来自预拓扑斯里余等化子 / 商的存在。）
• 有界：最小元是始对象到 $X$ 的唯一态射（预拓扑斯里始对象到任何对象都是单态射），最大元是 $1_{X}$ ✓。
• 分配律：$X_{1} \cap (X_{2}\cup X_{3}) = (X_{1}\cap X_{2}) \cup (X_{1}\cap X_{3})$ —— 沿单态射的拉回保余积（预拓扑斯里余积不交且万有），把两边都算成同一个拉回 ✓。
• 拉回是格同态：$f^{*}(-) := -\times_{Y} X$ 保拉回（是极限），故保交、保上下界；而它保余积（万有性）与像（像的计算可以搬到拉回里做），故保并 ✓。∎

「有界」指的是这个格有最小元（始对象出发的那个子对象）与最大元（$X$ 自己）。把「子对象」当成一个格来看，后面讲拓扑斯内部逻辑时用的就是它 —— 这里的交、并分别是逻辑的「且」与「或」。