Основная теорема теории топоса

В математике Фундаментальная теорема теории топоса гласит, что срез $\mathbf {E} /X$ топоса $\mathbf {E}$ над любым из своих объектов $X$ само по себе является топосом. Более того, если существует морфизм $f:A\rightarrow B$ в $\mathbf {E}$ тогда существует функтор $f^{*}:\mathbf {E} /B\rightarrow \mathbf {E} /A$ который сохраняет экспоненты и классификатор подобъектов .

Функтор обратного движения [ править ]

Для любого морфизма f в $\mathbf {E}$ существует связанный с ним «функтор обратного хода» $f^{*}:=-\mapsto f\times -\rightarrow f$ что является ключевым в доказательстве теоремы. Для любого другого морфизма g из $\mathbf {E}$ который имеет тот же кодомен, что и f , их произведение $f\times g$ - диагональ их квадрата обратного образа, а морфизм, выходящий из области определения $f\times g$ в область определения f противоположна g в обратном квадрате, поэтому это возврат g вдоль f , который можно обозначить как $f^{*}g$ .

Обратите внимание, что топос $\mathbf {E}$ изоморфен срезу над собственным терминальным объектом, т.е. $\mathbf {E} \cong \mathbf {E} /1$ , поэтому для любого объекта A в $\mathbf {E}$ есть морфизм $f:A\rightarrow 1$ и, следовательно, функтор обратного хода $f^{*}:\mathbf {E} \rightarrow \mathbf {E} /A$ , поэтому любой фрагмент $\mathbf {E} /A$ тоже топос.

Для заданного кусочка $\mathbf {E} /B$ позволять $X \over B$ обозначают его объект, где X — объект базовой категории. Затем $B^{*}$ является функтором, который отображает: $-\mapsto {B\times - \over B}$ . Теперь подайте заявку $f^{*}$ к $B^{*}$ . Это дает

f^{*}B^{*}:-\mapsto {B\times - \over B}\mapsto {{A \over B}\times {B\times - \over B} \over {A \over B}}\cong {{\Big (}{A\times _{B}\,B\times - \over B}{\Big )} \over {A \over B}}\cong {A\times _{B}B\times - \over A}\cong {A\times - \over A}=A^{*}

вот как действует функтор обратного отсчета $f^{*}$ отображает объекты $\mathbf {E} /B$ к $\mathbf {E} /A$ . Кроме того, заметим, что любой элемент C базового топоса изоморфен ${1\times C \over 1}=1^{*}C$ , поэтому, если $f:A\rightarrow 1$ затем $f^{*}:1^{*}\rightarrow A^{*}$ и $f^{*}:C\mapsto A^{*}C$ так что $f^{*}$ действительно является функтором базового топоса $\mathbf {E}$ на свой кусочек $\mathbf {E} /A$ .

Логическая интерпретация [ править ]

Рассмотрим пару основных формул $\phi$ и $\psi$ чьи расширения $[\_|\phi ]$ и $[\_|\psi ]$ (здесь подчеркивание обозначает нулевой контекст) являются объектами базового топоса. Затем $\phi$ подразумевает $\psi$ тогда и только тогда, когда существует моника из $[\_|\phi ]$ к $[\_|\psi ]$ . Если это так, то по теореме формула $\psi$ это правда в срезе $\mathbf {E} /[\_|\phi ]$ , потому что терминальный объект $[\_|\phi ] \over [\_|\phi ]$ факторов среза посредством его расширения $[\_|\psi ]$ . Логически это можно выразить так:

\vdash \phi \rightarrow \psi  \over \phi \vdash \psi

так что нарезка $\mathbf {E}$ путем расширения $\phi$ будет соответствовать предположению $\phi$ как гипотеза. Тогда теорема будет говорить, что логические предположения не меняют правил топосной логики.

См. также [ править ]

Ссылки [ править ]

МакЛарти, Колин (1992). «§17.3 Основная теорема» . Элементарные категории, элементарные топосы . Оксфордские руководства по логике. Том. 21. Издательство Оксфордского университета. п. 158. ИСБН 978-0-19-158949-2 .