Grundläggande teorem för topos teori

Inom matematiken säger topos teorins grundläggande sats att skivan E $\displaystyle \mathbf {E} /X}$ av en topos $\mathbf {E}$ över något av dess objekt $X$ är i sig en topos. Dessutom, om det finns en morfism $f:A\rightarrow B$ i $\mathbf {E}$ så finns det en funktion ${\ displaystyle f^{*}:\mathbf {E} /B\rightarrow \mathbf {E} /A}$ som bevarar exponentialer och subobjektsklassificeraren .

Tillbakadragningsfunktionen

För varje morfism f i $\mathbf {E}$ finns det en associerad "pullback functor" $f^{*}:=-\mapsto f\times -\rightarrow f$ som är nyckeln i beviset för satsen. För alla andra morfism g i $\mathbf {E}$ som delar samma koddomän som f , är deras produkt $f\times g$ diagonalen för deras tillbakadragningsruta och morfismen som går från domänen för $f\ gånger g$ till domänen för f är motsatt till g i pullback-rutan, så det är pullbacken av g längs f , som kan betecknas som $f^{*}g$ .

Observera att en topos $\mathbf {E}$ är isomorf till skivan över sitt eget terminalobjekt, dvs $\mathbf {E} \cong \mathbf {E} /1$ , så för alla objekt A i $\mathbf {E}$ finns en morfism $f:A\rightarrow 1$ och därmed en pullback-funktion ${\ displaystyle f^{*}:\mathbf {E} \rightarrow \mathbf {E} /A} ,$ vilket är anledningen till att varje skiva $\mathbf {E} /A$ också är en topos.

För en given skiva $\mathbf {E} /B$ låt $X \over B$ beteckna ett objekt av det, där X är ett objekt i baskategorin. Då $B^{*}$ en funktion som mappar: $-\mapsto {B\times - \over B}$ . Tillämpa nu $f^{*}$ på $B^{*}$ . Detta ger

f^{*}B^{*}:-\mapsto {B\times - \over B}\mapsto {{A \over B}\times {B\times - \over B} \over {A \ över 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^{*}

så det här är hur pullback-funktionen $f^{*}$ mappar objekt av $\mathbf {E} /B$ till $\mathbf {E} /A$ . Observera vidare att alla element C i bastoposen är isomorft till ${\displaystyle {1\times C \over 1}=1^{*}C} ,$ därför om $f:A\rightarrow 1$ sedan $f^{*}:1^{*}\rightarrow A^{*}$ och $f^{*}:C\mapsto A^{*}C$ så att $f^{*}$ verkligen är en funktor från bastoposen $\mathbf {E}$ till dess skiva $\mathbf {E} /A$ .

Logisk tolkning

Betrakta ett par grundformler $\phi }$ $[\_|\phi ]$ och $\psi$ vars tillägg och $[\_|\psi ]$ (där understrecket här betecknar nollkontexten) är objekt av bastopos. Då innebär $\phi$ $\psi$ om och endast om det finns en monic från $[\_|\phi ]$ till $[\_|\psi ]$ . Om dessa är fallet är formeln $\psi$ sann i segmentet $\mathbf {E} /[\_|\phi ]$ , eftersom terminalobjektet $[\_|\phi ] \över [\_|\phi ]$ av segmentet faktorer genom dess förlängning $[\_|\psi ]$ . I logiska termer skulle detta kunna uttryckas som

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

så att skärning av $\mathbf {E}$ med förlängningen av $\phi$ skulle motsvara att anta $\phi$ som en hypotes. Då skulle teoremet säga att att göra ett logiskt antagande inte ändrar reglerna för toposlogik.

Se även

McLarty, Colin (1992). "§17.3 Grundsatsen" . Elementära kategorier, elementära ämnen . Oxford Logic Guides. Vol. 21. Oxford University Press. sid. 158. ISBN 978-0-19-158949-2 .