¿Existe una prueba constructiva de que, en cuatro dimensiones, la categoría PL y la categoría lisa son equivalentes?

Question

Resumen

Como es sabido, las categorías de variedades suaves de 4 dimensiones y de variedades lineales a trozos de 4 dimensiones son equivalentes. ¿Existe una prueba constructiva para este teorema o depende del axioma de elección?

Antecedentes

Una variedad suave es una variedad con un atlas suave, es decir, un atlas con funciones de transición suaves. Éstas deberían ser bastante conocidas. Colectores lineales a trozos son un poco menos familiares. Se pueden definir como colectores con funciones de transición lineales a trozos.

La prueba convencional

Según tengo entendido, la demostración convencional del teorema pasa por una tercera categoría: El categoría de variedades suaves a trozos . La prueba es la siguiente:

1. Hay funtores fieles obvios desde las variedades suaves, y las variedades lineales a trozos, a las variedades suaves a trozos. Al fin y al cabo, toda función suave es parcialmente suave y toda función lineal es suave (por tanto, toda función parcialmente lineal es parcialmente suave).
2. Para demostrar que los dos funtores son completos y esencialmente suryectivos, hay que demostrar que toda función suave a trozos es globalmente suavizable, y linealizable a trozos, respectivamente.
3. Ambos funtores son completos, fieles y esencialmente suryentes, por lo tanto son equivalencias. Componiendo dos equivalencias se obtiene de nuevo una equivalencia.

La pregunta

El último y pequeño tercer paso de la prueba no es constructivo. Una equivalencia constructiva viene dada por un funtor, un inverso débil y los isomorfismos naturales que atestiguan las leyes inversas. Para definir dicho inverso débil para un funtor completo, fiel y esencialmente suryectivo, se necesita típicamente el axioma de elección, que no está disponible en la matemática constructiva.

¿Se puede seguir demostrando el teorema de forma constructiva? Esto sería algo raro porque, al final, te daría un algoritmo (aunque sea enrevesado) de cómo construir una estructura PL a partir de una estructura lisa, y viceversa.

Pero la otra opción parece aún más alarmante: ¿Es posible que no haya una prueba constructiva? ¿Es el teorema tal vez equivalente al axioma de elección, o es más débil? ¿Existen modelos matemáticos constructivos en los que el teorema es falso?

Answer 1

En esto, como en gran parte del análisis constructivo/álgebra, las cuestiones se dividen en dos aspectos:

1. las formalidades generales de la creación de las estructuras en cuestión;

2. el contenido constructivo específico del problema en cuestión.

Esta es una respuesta a medias, que aborda sólo el primer aspecto. Si ya tienes experiencia con las matemáticas constructivas, probablemente esto te resulte familiar y tenga menos interés que el segundo aspecto (que se aborda un poco en los comentarios). Por otro lado, si estás familiarizado con el análisis algorítmico/computacional, pero menos con el desarrollo general de las matemáticas en la lógica constructiva, esto es probablemente útil.

Básicamente, al desarrollar las matemáticas de forma constructiva, casi siempre se quiere seguir el principio de diseño No tome cocientes, y no imponga meras condiciones de existencia; incluya datos/testigos adicionales en las definiciones, y luego, si es necesario, lleve explícitamente la relación de equivalencia por la que clásicamente habría cotizado (o asegúrese de que se mantiene como, por ejemplo, isomorfismos en una categoría). Si sigues este principio, entonces si tienes algoritmos para calcular las construcciones que tienes en mente, normalmente serás capaz de juntar los algoritmos en funciones/homorfismos/functores como desees.

En su caso concreto, esto ocurre, por ejemplo, en las definiciones de una colector suave. Hay varias definiciones clásicas, pero la condición de existencia clave que todas contienen es que el atlas está cubriendo es decir, que para cada punto hay un gráfico alrededor de ese punto. Si se utiliza esta definición, será difícil (probablemente imposible) obtener una función que lleve a una variedad tan suave a su linealización a trozos, ya que, en primer lugar, habrá que elegir alguna carta alrededor de cada punto y, en segundo lugar, diferentes elecciones pueden producir linealizaciones a trozos diferentes (incluso no isomórficas).

Sin embargo, si se toma la definición de colector liso para incluir un elección de gráfico alrededor de cada punto (y de forma similar para las otras nociones de colector, y de forma similar establecer todas las definiciones de prerrequisitos de forma convenientemente constructiva), entonces parece probable que los algoritmos mencionados en los comentarios deberían ensamblar en la deseada equivalencia de categorías. En particular, los funtores "inversos" cuya existencia te preocupa no serán problemáticos, porque la prueba de la "subjetividad esencial" no será sólo una prueba de existencia, sino una construcción de un colector lineal a trozos equivalente a un colector suave a trozos dado.

Obsérvese que tales definiciones, con datos extra incluidos, son clásicamente equivalentes a las definiciones clásicas, en el sentido de producir categorías equivalentes de variedades, ya que dos variedades-con-datos-extra que difieren sólo en los datos extra terminarán siendo isomorfas en la categoría de variedades-con-datos-extra.

(Un enfoque totalmente diferente, bastante menos consolidado, sería trabajar en teoría de los tipos de homotopía/fundamentos equivalentes donde a menudo se pueden utilizar cocientes sin dejar de ser constructivos, esencialmente porque se puede cotizar todo. El problema con los cocientes/existencia en la matemática constructiva tradicional puede verse como el hecho de que no se puede "salir de un cociente" usando AC, como se puede en la matemática clásica, y por tanto si se toma un cociente de un conjunto/clase, habrá que tomar cocientes de otros conjuntos/clases a los que se pretende mapear - pero entonces no siempre se puede hacer eso, porque a menudo para la clase de objetos de una categoría, el cociente que se necesita sería un cociente de homotopía, que no existe a nivel de conjuntos/clases. En el entorno univalente, esto se arregla porque realmente puede tomar el cociente de homotopía de un tipo - y así realmente se pueden tomar cocientes en todas partes. En tu ejemplo, esto se vería en las construcciones de las categorías de homotopía de las variedades: serían Rezk-completions Así pues, los colectores equivalentes serían iguales como objetos de estas categorías; dicho con más cuidado, las igualdades entre objetos de estas categorías corresponderían a equivalencias de colectores. Así, puesto que la linealización a trozos es (como clásicamente) única hasta la equivalencia canónica, sería literalmente única en este entorno, y así daría un mapa bien definido de las variedades (a trozos) suaves a las lineales a trozos).