# Topos

Na matemática, topos elementares (ou brevemente topos) podem ser analisados à base de diversas perspectivas. Do ponto de vista da teoria das categorias, um topos é uma categoria com limites finitos e "objetos de potência". Do ponto de vista da geometria algébrica, topos assemelham-se a categorias de feixes, e, sendo "espaços generalizados", admitem conceitos de "pontos" e "morfismos geométricos". Do ponto de vista da lógica matemática, topos são universos da lógica intuicionista de ordem superior, satisfazendo possíveis axiomas adicionais. Do ponto de vista da álgebra universal, existem "topos classificadores", para teorias como a dos anéis.
O conceito de topos elementar surgiu a partir de uma generalização de topos de Grothendieck, como parte da pesquisa por William Lawvere e Myles Tierney em busca de uma fundação natural para matemática baseada em categorias.

## Definição

Antes de estudar topos, é necessário conhecimento em teoria das categorias.

### Classificador de subobjetos

O classificador de subobjetos é uma generalização do conceito de função característica de subconjunto.
Seja E uma categoria com produtos fibrados. Define-se functor de subobjetos Sub : E$^{op}$ → Conj por:
    Sub E é a coleção dos subobjetos de E,
    Sub (f : F → E) leva um subobjeto m : A → E ao subobjeto f$^*$ m : B → F, onde
${\begin{matrix}&B&\to &A\\f^{*}m&\downarrow &&\downarrow &m\\&F&{\underset {f}{\to }}&E\end{matrix}}$ é diagrama de produto fibrado.
Um classificador de subobjetos para E é um morfismo vero : 1 → Ω (onde 1 é o objeto terminal), tal que para cada monomorfismo m : A → E, existe único morfismo car m : E → Ω, chamado morfismo característico, tal que ${\begin{matrix}&A&{\overset {}{\to }}&1\\m&\downarrow &&\downarrow &\mathrm {vero} \\&E&{\underset {\mathrm {car} m}{\to }}&\Omega \end{matrix}}$ é diagrama de produto fibrado. (Noutras palavras, para cada morfismo x : X → E, vale que car m ∘ x = vero ∘ se e só se existe x′ : X → A tal que x = m ∘ x′.)
Uma categoria E com produtos fibrados admite classificador de subobjetos se e só se existe isomorfismo natural
    Sub(–) ≅ hom$_E$(–, Ω).

### Topos elementar

Um topos elementar (ou brevemente topos) é uma categoria E que
* é finitamente completa,
* admite objetos exponenciais,
* e admite classificador de subobjetos.
Pode-se mostrar que, se E é finitamente completa, e admite objetos de potência, isto é, existe functor P : E$^{op}$ → E tal que há isomorfismo natural
    hom$_E$(A, P B) ≅ Sub(A × B)
em A, B, então E é um topos (isto é, também admite exponenciais); com efeito, assim como funções em teoria dos conjuntos são definidas como certas relações, o exponencial B$^A$ pode ser definido com um certo subobjeto de P(A × B). Num topos, P(A) := Ω$^A$ define os objetos de potência.

### Exemplos

* A categoria dos conjuntos pequenos Conj é um topos elementar. Mais geralmente, todo topos de Grothendieck é topos elementar.
* O produto de dois topos é um topos.
* A categoria dos conjuntos finitos é um topos elementar que não é topos de Grothendieck.
* O topos efetivo, essencialmente consistindo de "funções computáveis", é um topos elementar que não é topos de Grothendieck.

## Propriedades

Topos gerais satisfazem várias propriedades similares a um "universo construtivo de conjuntos".
Para cada objeto A de um topos E, existe monomorfismo (id, id) : A → A × A, admitindo logo morfismo característico
    [=] := car (id, id) : A × A → Ω,
que é um análogo à relação de igualdade, no aspecto de que, dados morfismos x, y : X → A, vale que
    [=] ∘ (x, y) = vero ∘ se e só se x = y.
Adjunção exponencial leva a morfismo
    [] : A → Ω$^A$
análogo à formação de subconjuntos unitários, no aspecto de que
    ap ∘ ([] ∘ x, y) = vero ∘ se e só se x = y, para quaisquer x, y : X → A.
Também, é possível definir [∧] : Ω × Ω → Ω como o morfismo característico do monomorfismo (vero, vero) : 1 → Ω × Ω; assim, [∧] é análogo à operação de conjunção em valores lógicos.
Dado monomorfismo m : A → B, existe transformação natural
    Sub(– × A) → Sub(– × B)
dada por composição com id × m, que induz transformação natural
    hom(–, Ω$^A$) → hom(–, Ω$^B$)
e consequentemente morfismo ∃$_m$ : Ω$^A$ → Ω$^B$, com propriedades similares à operação de imagem de subconjuntos.
A condição de Beck–Chevalley interna diz que, dados monomorfismos k : B′ → B e m : C′ → C, de modo que ${\begin{matrix}&C'&{\overset {g'}{\to }}&B'\\m&\downarrow &&\downarrow &k\\&C&{\underset {g}{\to }}&B\end{matrix}}$ é diagrama de produto fibrado, então o diagrama ${\begin{matrix}&\Omega ^{B'}&{\overset {\Omega ^{g'}}{\to }}&\Omega ^{C'}\\\exists _{k}&\downarrow &&\downarrow &\exists _{m}\\&\Omega ^{B}&{\underset {\Omega ^{g}}{\to }}&\Omega ^{C}\end{matrix}}$ é comutativo, isto é,
    Ω$^g$ ∘ ∃$_k$ = ∃$_m$ ∘ Ω$^{g′}$.

### Teorema de Paré

Dado topos E, o teorema de monadicidade de Beck implica que o functor P = Ω$^{(–)}$ : E$^{op}$ → E é monádico. Em particular, topos também admitem todos os colimites finitos.
Com isso é possível fatorar setas em topos, similarmente à fatoração de uma função como uma função sobrejetiva seguida de função injetiva (inclusão da imagem no contradomínio). Para seta f : A → B, seja x : B → B′ com y : B → B′ o pushout de f com f, que é colimite finito; seja m : M → B equalizador de x com y. Então, f = m ∘ e para único morfismo e : A → M, com e sendo epimorfismo; ainda mais, m é a imagem de f, isto é, o menor subobjeto de B pelo qual f se fatora.
Como aplicação, existem uniões (supremos) de subobjetos. Com efeito, dados monomorfismos m : M → A e n : N → A, o morfismo ⟨m, n⟩ : M + N → A admite alguma imagem p : P → A. Vale que p é o supremo de m e n na ordem de subobjetos de A. Esta definição induz morfismo
    [∨] : Ω × Ω → Ω
análogo à operação de disjunção em valores lógicos.

### Topos de morfismos

Dado topos E, e objeto X seu, denote por E/X a categoria de setas em E de contradomínio A. (Noutras palavras, é a categoria vírgula id$_E$ ↓ (• ↦ X).)
Então, E/X é um topos. Para cada f : Y → X em E/X, objeto de potência P f : D → X pode ser construído como o pullback ${\begin{matrix}D&\longrightarrow &X\\\downarrow &&\downarrow &[\{\}]\\X\times \mathbf {P} Y&{\underset {[\{\}]\times \exists _{f}}{\to }}\mathbf {P} X\times \mathbf {P} X{\underset {\vee }{\to }}&\mathbf {P} X\end{matrix}}$ onde ∨ : P X × P X → P X é induzido pela união de subobjetos, e onde ∃$_f$ (sendo que f não precisa ser monomorfismo) é análogo à operação de imagem de subconjuntos. (Para melhor entendimento, é útil tratar objetos de E/X como "famílias X-indexadas de objetos de E".)
Em particular, cada E/X é cartesiana fechada, logo E é localmente cartesiana fechada. Isto implica, para cada k : Y → X, a existência de adjunções
    Σ$_k$ ⊣ k$^*$ ⊣ Π$_k$
onde k$^*$ : E/X → E/Y é functor de pullback por k : Y → X. Por sua vez, isto implica que pullbacks num topos preservam epimorfismos e se distribuem em coprodutos, por exemplo.

## Linguagem de Mitchell–Bénabou

A linguagem de Mitchell–Bénabou é uma linguagem formal que permite facilitar a demonstração de propriedades de topos. Com ela é possível tratar os objetos e morfismos de um topos como se fossem conjuntos e funções num universo satisfazendo as regras da lógica intuicionista de ordem superior.
Como um exemplo básico, dados morfismos f : A → C e g : B → C num topos E, a fórmula
    x : A, y : B ⊢ (f x = g y) : Ω
é interpretada como um morfismo A × B → Ω, que é precisamente o morfismo característico da inclusão do produto fibrado A ×$_C$ B → A × B.

## Modalidade de Lawvere–Tierney

Uma modalidade (ou topologia) de Lawvere–Tierney num topos E é um morfismo j : Ω → Ω em E tal que j ∘ vero = vero, j ∘ j = j e j ∘ [∧] = [∧] ∘ (j × j).
Num topos de pré-feixes Conj$^{Cop}$, as modalidades de Lawvere–Tierney estão em correspondência biunívoca com as topologias de Grothendieck. Com efeito, uma topologia de Grothendieck J pode ser levada a j : Ω → Ω tal que j$_C$(S) é o J-fecho de S, isto é, a família das setas g : D → C tais que g$^*$ S ∈ J(D); por outro lado, uma modalidade j : Ω → Ω pode ser levada a J tal que J(C) consiste precisamente das peneiras S (isto é, membros de Ω(C)) tais que j$_C$(S) é a peneira máxima. Esta equivalência sugere as definições abaixo.
Cada subobjeto A → E admite fecho A$^−$ → E, dado por ser subobjeto caracterizado por j ∘ χ, onde χ : E → Ω é morfismo característico de A → E. Esta operação de fecho tem as propriedades A ⊆ A$^−$, (A$^−$)$^−$ = A$^−$ e (A ∩ B)$^−$ = A$^−$ ∩ B$^−$. Um monomorfismo A → E é dito ser denso quando o fecho A$^−$ é o maior subobjeto de E.
Um objeto G ∈ E é dito ser separado (respectivamente, feixe) para a modalidade j quando, para cada monomorfismo denso m : A → E, composição com m induz função
    hom(E, F) → hom(A, F)
que é uma injeção (respectivamente bijeção). Denota-se por Fx$_j$ E a subcategoria plena de E consistindo dos feixes.
Como no caso de topos de Grothendieck, Fx$_j$ E é fechada em limites finitos, e também exponenciações (_)$^E$, para E ∈ E qualquer. Também, Fx$_j$ E é um topos, cujo classificador de subobjetos é r ∘ vero : 1 → Ω$_j$, onde Ω → Ω$_j$ → Ω é a fatoração de j em epimorfismo seguido de monomorfismo.
Também, é possível provar a existência de feixificação a : E → Fx$_j$ E (o adjunto esquerdo da inclusão Fx$_j$ E → E). Para cada objeto E ∈ E, a fórmula
    f : E → Ω$_j$ ⊢ j (∃ (e : E), ∀ (x : E), f x = r (x = e))
na linguagem de Mitchell–Bénabou é interpretada como um morfismo χ : (Ω$_j$)$^E$ → Ω, classificando subobjeto F → (Ω$_j$)$^E$; assim, F é feixificação de E. (A aplicação de j a valores lógicos indica sua relação com a lógica modal.)
Um exemplo de modalidade é a dupla negação j = [¬] ∘ [¬], também chamada de modalidade densa. Neste caso, Fx$_{¬¬}$ E é sempre um topos satisfazendo a lógica clássica. (Compare com a tradução da dupla negação.)