The Synthetic Sierpinski Cone

1. Declaração do Problema

O artigo aborda uma tensão fundamental na matemática sintética (especificamente dentro da Teoria dos Tipos de Homotopia, ou HoTT) regarding a relação entre construções geométricas e classificação lógica de mapas parciais.

• A Coincidência Clássica: Na teoria das categorias clássica e na teoria de domínios, o cone de Sierpi´nski ($X_\perp$), construído colando um ponto fechado universal abaixo de um espaço $X$, é equivalente ao classificador de mapas parciais ($L^\circ(X)$). Este último classifica mapas parciais definidos em subespaços abertos. Esta equivalência é uma pedra angular da dualidade entre lógica e geometria nestes campos.
• O Obstáculo Sintético: Em contextos sintéticos baseados em HoTT com um intervalo genérico $I$, afirmar que $X_\perp \simeq L^\circ(X)$ para todos os tipos $X$ leva a uma degeneração da teoria. Especificamente, se esta equivalência valer universalmente, força o intervalo $I$ a ser "codiscreto" (trivial), colapsando a distinção entre subespaços abertos e fechados e tornando todos os espaços sintéticos triviais.
• A Questão Central: É possível identificar um subuniverso não trivial de tipos onde o cone de Sierpi´nski de fato classifica mapas parciais, e como isso se relaciona com noções existentes de completude na teoria sintética de categorias superiores (especificamente a completude de Segal)?

2. Metodologia

Os autores trabalham dentro dos Fundamentos Univalentes (HoTT) sem assumir axiomas fortes sobre o intervalo $I$ (como ser uma ordem linear estrita) ou usar modalidades globalmente, exceto onde necessário para argumentos específicos. Eles utilizam:

• Retículos Distributivos: Eles parametrizam sua teoria sobre um retículo distributivo limitado $\Sigma$ (representando o "intervalo" $I$) em vez de fixar um modelo específico.
• Teoria de Localização: Eles empregam a teoria de localizações reflexivas acessíveis (seguindo Rijke et al.) para definir subuniversos de tipos "completos".
• Ortogonalidade: Eles definem completude via ortogonalidade a classes específicas de mapas (inclusões de chifres, cones, etc.).
• Cilindros de Mapeamento: Eles generalizam o cone de Sierpi´nski para cilindros de mapeamento abertos (ou cilindros de exibição abertos) para lidar com famílias dependentes de tipos.
• Modalidades (Limitadas): Eles usam brevemente uma modality de "pontos globais" ($\flat$) para analisar a exponenciabilidade de pontos globais sem colapsar a lógica interna.

3. Contribuições e Definições Principais

A. Hierarquia de Completude

O artigo estabelece uma hierarquia estrita de condições de completude para tipos, refinando o trabalho de Pugh e Sterling:

1. Completude de Segal: Ortogonal à inclusão de chifre interno $\Lambda^2_1 \hookrightarrow \Delta^2$. Esta é a condição padrão para $\infty$-categorias sintéticas.
2. Completude de Segal Baseada: Ortogonal à família de inclusões $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$. Esta é uma condição mais forte.
3. Completude de Sierpi´nski Pequena: Ortogonal aos mapas de comparação "pequenos" $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$.
4. Completude de Sierpi´nski: Ortogonal à família completa de mapas de comparação $\sigma_X: X_\perp \to L^\circ(X)$ para todos os $X$.

B. A Equivalência Principal

Os autores provam que a Completude de Sierpi´nski Pequena é equivalente à Completude de Sierpi´nski.

• Significado: Pugh e Sterling haviam mostrado anteriormente esta equivalência apenas para tipos 0-truncados (conjuntos). Este artigo estende-a para tipos não truncados (grupos superiores/$\infty$-categorias), provando que verificar a ortogonalidade contra os mapas "pequenos" é suficiente para garantir a ortogonalidade contra todos os mapas.

C. Separação entre Completude de Segal e Completude de Segal Baseada

O artigo resolve uma conjectura de Ulrik Buchholtz, provando que a completude de Segal não implica completude de Segal baseada em contextos não triviais.

• Eles mostram que, se todo tipo com completude de Segal também fosse com completude de Segal baseada, o intervalo $I$ tornaria-se inicial-quotiente (colapsando para um conjunto de dois elementos), o que contradiz as propriedades de modelos padrão como espaços simpliciais.
• Isso estabelece que a condição "Segal Baseada" é estritamente mais forte e necessária para que o cone de Sierpi´nski funcione como um classificador de mapas parciais.

D. Cilindros de Mapeamento e Classificadores de Mapas Parciais

Os autores estendem os resultados do cone de Sierpi´nski para cilindros de mapeamento abertos ($M^\circ_Y(f)$).

• Eles demonstram que, para tipos com completude de Sierpi´nski, o cilindro de mapeamento aberto de uma função $f: X \to Y$ é equivalente ao classificador de mapas parciais relativo $L^\circ_Y(f)$.
• Isso fornece uma nova propriedade universal "de mão direita" para cilindros de mapeamento dentro do subuniverso de tipos com completude de Sierpi´nski.

4. Resultados Chave

1. Teorema 64 & Corolário 66: Um tipo é com completude de Sierpi´nski se e somente se for com completude de Sierpi´nski pequena. Consequentemente, os tipos com completude de Sierpi´nski formam um subuniverso reflexivo acessível.
2. Corolário 48/49/50: Em modelos padrão (espaços simpliciais, espaços cúbicos de Dedekind), a completude de Segal baseada é estritamente mais forte que a completude de Segal.
3. Teorema 75 & Corolário 77: O subuniverso de tipos com completude de Sierpi´nski é fechado sob a formação de classificadores de mapas parciais abertos relativos. Dentro deste subuniverso, o cilindro de mapeamento aberto $M^\circ_Y(f)$ classifica pontos $y:Y$ equipados com elementos parciais abertos da fibra $\text{fib}_f(y)$.
4. Exponenciabilidade: O artigo analisa a exponenciabilidade de pontos globais. Mostra que, embora as inclusões de pontos globais sejam exponenciáveis no sentido clássico, elas não são $L_{Segal}$-exponenciáveis internamente a menos que o intervalo seja trivial. Isso destaca a distinção entre propriedades internas e externas na matemática sintética.

5. Significado e Aplicações

• Semântica Denotacional: Na teoria sintética de domínios, a parcialidade é frequentemente modelada via o monad de classificador de mapas parciais $L^\circ$. Os resultados esclarecem que, para definir funções preguiçosas (que dependem de se uma entrada está definida) por casos, o codomínio deve ser completamente de Sierpi´nski. Isso implica que qualquer domínio sintético que suporte tais funções preguiçosas deve satisfazer a condição de Segal (transitividade de caminhos) e, mais fortemente, a condição de Segal baseada.
• Teoria Sintética de Categorias Superiores: O trabalho esclarece a estrutura do cocompletamento livre por um objeto inicial. Em $\infty$-categorias sintéticas, o cone de Sierpi´nski $C_\perp$ não é automaticamente uma $\infty$-categoria. No entanto, dentro do subuniverso reflexivo de $\infty$-categorias com completude de Sierpi´nski, a reflexão $R(C_\perp)$ é equivalente ao classificador de mapas parciais $L^\circ(C)$. Isso fornece uma descrição computacionalmente tratável do cocompletamento livre nestes contextos específicos.
• Unificação de Campos: O artigo unifica com sucesso conceitos de topologia sintética, teoria de domínios e teoria de categorias superiores. Demonstra que a "coincidência" entre o cone geométrico de Sierpi´nski e o classificador lógico de mapas parciais não é uma lei universal, mas uma propriedade de um subuniverso específico e bem-comportado de tipos.
• Mecanização: Os autores notam que seus resultados principais foram mecanizados no assistente de prova Agda, garantindo a correção rigorosa dos argumentos da teoria dos tipos.

Em resumo, o artigo resolve uma ambiguidade crítica na matemática sintética ao identificar as condições precisas (completude de Sierpi´nski) sob as quais construções geométricas (cones/cilindros) se alinham com a classificação lógica (mapas parciais), provando simultaneamente que essas condições são estritamente mais fortes que os requisitos padrão para $\infty$-categorias sintéticas.