Apéndice D — Cobertura Lean y obligaciones pendientes

Fecha de última modificación

1 de octubre de 2026

Índice del tratado

D.1. Qué certifica esta tabla

Este apéndice reúne el estado formal acreditado del tratado. Se cotejaron los enunciados canónicos, los informes de formalización y el código de siete módulos con sus PR y ejecuciones de CI. La correspondencia matemática es una revisión manual; el compilador verifica las declaraciones Lean. Ninguna de ambas verificaciones sustituye a la otra.

Inventario de los 133 teoremas: 5 C, 11 P y 117 N. C = cobertura completa del enunciado en el marco indicado; P = fragmento o instancia comprobada; N = sin correspondencia acreditada en los módulos e informes auditados. N no afirma que el resultado sea falso ni que no exista en Mathlib. Además hay un criterio auxiliar A de TF-DEF-00051 y un fragmento P de TF-CEX-00022: 18 nodos editoriales con alguna correspondencia, de los cuales 16 son teoremas. No se transforma este conteo en porcentaje global de formalización.

Los 269 nodos editoriales, sus hipótesis y el grafo conservan su identidad. Los rótulos C/P/N son estados formales, independientes del estado editorial closed. No se acredita automáticamente un capítulo entero, sus ejemplos o sus axiomas a partir de una declaración.

D.2. Evidencia de integración y compilación

Instantánea consultada de main: 4ccf72865c214f40d301731bd57956d3cd569ac9. Los siete archivos coinciden byte a byte con los de sus respectivas cabezas verificadas y están importados por lean/MatematicaAbierta.lean tanto en cada cabeza como en la instantánea. Esto acredita persistencia del código; no una recompilación de main actual.

Módulo / PR SHA de cabeza SHA de merge Lean CI Quarto CI
Diagonalizacion.lean · #101 f776929d2707cdc299233da3950364b69c695e27 f8c0be7009ed44b01a5476a9abac6d525b6a2f90 success 35486201835 success 35486201836
Reindexacion.lean · #108 b53bc45772e5347e97eade49091aa3c659e387b1 d28a2feedac8f0472ef2a4eedfe2a9ffcf83dffd success 35487512884 success 35487512833
Correspondencias.lean · #111 463e8c9dd8ebedba0eeda49e94b85b2d37c117be 30ca459c90d74dbcdfd1742e531ec937c61e956e success 35489487022 success 35489487026
SemanticaEquivalencia.lean · #118 9541a9d8115a7ee3629abd1b60fcff1befa65fc8 a89e73c153ca110a0d1e5794f67b59194f00fddb success 35551153957 success 35551153969
NaturalidadSondas.lean · #122 c3eae9d97db95473a126c79faccbc9ce047e219f b8e3119d4b7c837beefbd8b0de72a6ae7bd3883d success 35553293424 success 35553293436
DensidadTerminal.lean · #125 e1aed9bc7157d1124beab58db393017656737707 537e64460a898f25fda7d670a28faf51b0ae0fec success 35557164969 success 35557164973
GraficasEstructurales.lean · #144 f0882e31d635565016427d35810c2c5d48f9d992 9dba276e63884f73e130143589f294054e3becb0 success 35633391492 success 35633391498

Las 14 ejecuciones terminaron completed/success y su head_sha coincide con la cabeza de la PR correspondiente. En los siete jobs Lean, verify finalizó correctamente, incluidos el rechazo de marcadores de pruebas incompletas y la construcción de la biblioteca. Los workflows coinciden: lean-action@v1, directorio lean, build=true, test=false, lint=false, build-args=–wfail, dependencias fijadas y caché Mathlib. No hay un paso de auditoría #print axioms. No se ejecutaron compilación local, CI nueva ni publicación; Quarto Check satisfactorio no equivale a publicación.

D.3. Correspondencias matemáticas y límites

Las formulaciones literales, variables, imports y cuerpos de prueba se conservan en D.5; los enlaces de declaración fijan SHA y línea. «Propio» significa argumento desarrollado en el módulo usando la infraestructura lógica habitual; «Mathlib» indica resolución esencial por resultados o instancias de la biblioteca; «mixto» combina ambos. No es una clasificación de independencia axiomática.

TF-THM-00004 — C · Gráfica monomórfica

Original: La flecha gráfica ⟨id,f⟩ es un monomorfismo. Localizador 1.3.3.

Declaraciones: graphStructural_mono.

Método y dependencias: Mathlib: despliegue de graphStructural e infer_instance; producto binario y categoría dados.

Alcance y obligación pendiente: Correspondencia reconocida en esta auditoría sobre código ya compilado en PR #144; no es una prueba nueva.

TF-THM-00005 — C · Caracterización de gráficas

Original: Un mono representa una gráfica exactamente cuando su primera proyección es iso; recuperación y unicidad. Localizador 1.3.4.

Declaraciones: tf_thm_00005, tf_thm_00005_recover, tf_thm_00005_unique, tf_thm_00005_invariant.

Método y dependencias: Mixto: desarrollo propio con Subobject.isoOfMkEqMk, ofMkLEMk_comp, mk_eq_mk_of_comm, prod.hom_ext e inversas.

Alcance y obligación pendiente: Igualdad de clases de subobjetos; no igualdad literal de representantes. Auditoría de axiomas metateóricos pendiente.

TF-THM-00088 — C · Lema diagonal para familias totales

Original: La diagonal torcida difiere de cada sección si el endomapa carece de puntos fijos. Localizador 11.1.2.

Declaraciones: diagonal_ne_section, no_surjective_sections.

Método y dependencias: Propio: argumento diagonal, congrFun y el lema local de punto fijo.

Alcance y obligación pendiente: Sin conclusión efectiva ni sustitución de sobreyectividad por epi categórico.

TF-THM-00089 — C · Punto fijo a partir de enumeración exhaustiva

Original: La sobreyectividad de las secciones implica que cada endomapa tiene un punto fijo. Localizador 11.1.3.

Declaraciones: fixedPoint_of_surjective_sections.

Método y dependencias: Propio: especializar la sección de la diagonal torcida.

Alcance y obligación pendiente: U : A → A → B; cuantificación sobre funciones de tipos.

TF-THM-00090 — P · Teorema de Cantor por diagonalización

Original: Obstrucción de Cantor a enumerar la potencia. Localizador 11.1.4.

Declaraciones: cantor_predicate.

Método y dependencias: Propio: negación diagonal en Prop y transporte de igualdad.

Alcance y obligación pendiente: Falta el puente explícito entre predicados y el objeto potencia del enunciado; no acredita una versión general en topoi.

TF-THM-00098 — C · No sobreyectividad bajo reindexación sobreyectiva

Original: Obstrucción diagonal bajo reindexación sobreyectiva q : A → P. Localizador 12.2.2.

Declaraciones: reindexed_diagonal_ne_section, reindexed_no_surjective_sections.

Método y dependencias: Propio: testigo de sobreyectividad y contradicción diagonal.

Alcance y obligación pendiente: Se conservan explícitas la sobreyectividad de q y la ausencia de puntos fijos de s.

TF-THM-00102 — P · Compatibilidad exacta de gráficas con sustitución y composición

Original: Compatibilidad y recuperación de funciones mediante sus gráficas. Localizador 13.1.2.

Declaraciones: graph13_precompose, graph13_compose.

Método y dependencias: Propio: igualdad definicional y eliminación/introducción del testigo existencial.

Alcance y obligación pendiente: Sólo precomposición y composición de predicados de gráficas. Faltan identidad, proyección biyectiva, recuperación en ambas direcciones y puente explícito a las relaciones del manuscrito (F3).

TF-THM-00103 — P · Ley beta categórica para la abstracción y la aplicación

Original: Identidad beta de currificación en el marco cartesiano cerrado. Localizador 13.2.2.

Declaraciones: set_beta_uncurry_curry.

Método y dependencias: Propio: extensionalidad de funciones y reducción.

Alcance y obligación pendiente: Instancia Set; no la formulación en una categoría cartesiana cerrada arbitraria.

TF-THM-00104 — P · Ley eta categórica y recuperación de la abstracción

Original: Identidad eta de currificación en el marco cartesiano cerrado. Localizador 13.2.3.

Declaraciones: set_eta_curry_uncurry.

Método y dependencias: Propio: extensionalidad de funciones y reducción.

Alcance y obligación pendiente: Instancia Set; no la formulación categórica general.

TF-THM-00111 — P · Las equivalencias de nombres transportan la computabilidad

Original: Transporte de realizadores bajo equivalencia de representaciones. Localizador 14.3.3.

Declaraciones: names14_transport.

Método y dependencias: Propio: sustitución de igualdades de denotación.

Alcance y obligación pendiente: Sólo funciones totales Nat → Nat y conmutación semántica suministrada. No formaliza computabilidad ni dominios parciales.

TF-THM-00113 — P · Criterio exacto de recuperación por observadores

Original: Detección de igualdad mediante observadores. Localizador 14.5.2.

Declaraciones: observer14_injective.

Método y dependencias: Propio: inyectividad y congrFun.

Alcance y obligación pendiente: Un único observador inyectivo; falta el criterio general de familias conjuntamente separadoras.

TF-THM-00114 — P · El cambio de coordenadas transporta funciones, pero no por sí solo algoritmos

Original: Transporte por biyecciones, igualdad y compatibilidad con composición. Localizador 14.5.4.

Declaraciones: transport14_inverse, transport14_comp.

Método y dependencias: Mixto: desarrollo propio y simplificación de Equiv.

Alcance y obligación pendiente: El original ya es conjuntista. Se prueban una orientación de la inversa y composición; no se declara el paquete completo de biyección, reflexión de igualdad y alcance efectivo.

TF-THM-00120 — P · El encaje de Yoneda es pleno y fiel

Original: Reconstrucción de flechas a partir de familias naturales de sondas. Localizador 15.2.5.

Declaraciones: yoneda15_map_natural, yoneda15_recover, yoneda15_full, yoneda15_faithful.

Método y dependencias: Propio: naturalidad especializada en la identidad y extensionalidad.

Alcance y obligación pendiente: Sólo tipos y funciones; no Yoneda en categoría arbitraria ni auditoría de tamaño.

TF-THM-00123 — P · Las transformaciones naturales entre productos son funciones

Original: Las transformaciones naturales X×A → X×B en Set corresponden a funciones A → B. Localizador 15.4.1.

Declaraciones: product15_natural, product15_recover.

Método y dependencias: Propio: especialización a PUnit y naturalidad.

Alcance y obligación pendiente: El original ya está en Set: ésa no es la brecha. Se construye la familia y se recupera su fórmula, pero faltan declaraciones explícitas de unicidad y correspondencia en ambas direcciones.

TF-THM-00127 — P · Densidad de Yoneda: todo prehaz es un colímite canónico de representables

Original: Densidad: reconstrucción mediante el colímite de representables. Localizador 16.2.3.

Declaraciones: density16Equiv, density16_universal.

Método y dependencias: Mixto: Equiv con inversas explícitas y desarrollo propio de universalidad.

Alcance y obligación pendiente: Sólo categoría base terminal: Σ s:S, PUnit ≃ S; no categoría de elementos ni colímite general.

TF-THM-00131 — P · Los representables detectan conjuntamente transformaciones

Original: Detección de igualdad mediante la presentación densa. Localizador 16.4.2.

Declaraciones: density16_detect.

Método y dependencias: Propio: evaluar inclusiones de PUnit.

Alcance y obligación pendiente: Sólo funciones de conjuntos detectadas por inclusiones unitarias.

TF-DEF-00051 — A · Equivalencia semántica de índices

Original: Extensionalidad de las secciones de una presentación. Localizador 12.3.1.

Declaraciones: extensional_sections_iff.

Método y dependencias: Propio: funext y congrFun.

Alcance y obligación pendiente: Sólo criterio puntual (∀ a, U p a = U r a) ↔︎ U p = U r. No formaliza cociente ni decisión de igualdad.

TF-CEX-00022 — P · Densidad no significa que cada prehaz sea representable

Original: Límite de la representabilidad en el caso terminal. Localizador 16.5.1.

Declaraciones: density16_bool_not_unit.

Método y dependencias: Propio: incompatibilidad de Bool y PUnit mediante inyectividad.

Alcance y obligación pendiente: Sólo ¬Nonempty (Bool ≃ PUnit); falta el modelo categórico completo del contraejemplo.

Dos precisiones de esta auditoría

TF-THM-00004 se reconoce ahora en graphStructural_mono. Bajo Category y HasBinaryProduct A B, la definición es prod.lift (𝟙 A) f y la instancia prueba Mono de esa flecha: coincide con el enunciado 1.3.3. La PR #144 y su compilación preceden a esta correspondencia documental. El informe F1 histórico conserva su alcance declarado sobre TF-THM-00005.

TF-THM-00123 permanece P por las obligaciones declarativas explicitadas arriba. Su enunciado original ya es en Set; describir su brecha como falta de generalidad categórica sería incorrecto. La misma precaución se aplica al transporte por biyecciones de TF-THM-00114.

D.4. Inventario exhaustivo de teoremas

Cada ID del registro aparece exactamente una vez en esta tabla. Los nombres son los del registro; el localizador remite al manuscrito canónico.

ID Enunciado / nombre registrado Localizador Estado Evidencia
TF-THM-00001 Unicidad identidad 1.1.3 N Sin correspondencia acreditada
TF-THM-00002 Unicidad inversa 1.1.5 N Sin correspondencia acreditada
TF-THM-00003 Terminal único salvo isomorfismo único 1.2.3 N Sin correspondencia acreditada
TF-THM-00004 Gráfica monomórfica 1.3.3 C graphStructural_mono
TF-THM-00005 Caracterización de gráficas 1.3.4 C tf_thm_00005
TF-THM-00006 Representación por elementos globales del exponencial 1.4.2 N Sin correspondencia acreditada
TF-THM-00007 Extensionalidad por puntos 2.1.3 N Sin correspondencia acreditada
TF-THM-00008 Generador si y sólo si funtor fiel 2.2.2 N Sin correspondencia acreditada
TF-THM-00009 Separación por elementos generalizados 2.4.2 N Sin correspondencia acreditada
TF-THM-00010 Evaluación en un punto 2.5.2 N Sin correspondencia acreditada
TF-THM-00011 Igualdad de transpuestas 2.5.3 N Sin correspondencia acreditada
TF-THM-00012 Extensionalidad de evaluación parametrizada 2.5.4 N Sin correspondencia acreditada
TF-THM-00013 Orden parcial de subobjetos 3.1.2 N Sin correspondencia acreditada
TF-THM-00014 Gráfica como relación 3.1.4 N Sin correspondencia acreditada
TF-THM-00015 Preimagen monomórfica 3.2.3 N Sin correspondencia acreditada
TF-THM-00016 Leyes de la preimagen 3.2.4 N Sin correspondencia acreditada
TF-THM-00017 Intersección por producto fibrado 3.2.5 N Sin correspondencia acreditada
TF-THM-00018 Representación de subobjetos 3.3.2 N Sin correspondencia acreditada
TF-THM-00019 Naturalidad de características 3.3.3 N Sin correspondencia acreditada
TF-THM-00020 Igualdad por características gráficas 3.4.1 N Sin correspondencia acreditada
TF-THM-00021 Representación por objeto potencia 3.4.3 N Sin correspondencia acreditada
TF-THM-00022 Asociatividad relacional en Set 3.5.3 N Sin correspondencia acreditada
TF-THM-00023 Productos y pullbacks dan límites finitos 4.1.1 N Sin correspondencia acreditada
TF-THM-00024 Ortogonalidad, composición y mono regular epi 4.2.2 N Sin correspondencia acreditada
TF-THM-00025 Unicidad y estabilidad de imágenes 4.2.3 N Sin correspondencia acreditada
TF-THM-00026 Independencia de representantes 4.3.2 N Sin correspondencia acreditada
TF-THM-00027 Identidades relacionales 4.3.3 N Sin correspondencia acreditada
TF-THM-00028 Asociatividad relacional regular 4.3.4 N Sin correspondencia acreditada
TF-THM-00029 Inclusión fiel por gráficas 4.3.5 N Sin correspondencia acreditada
TF-THM-00030 Totalidad regular y unicidad implican gráfica 4.3.6 N Sin correspondencia acreditada
TF-THM-00031 Adjunción imagen/preimagen 4.4.2 N Sin correspondencia acreditada
TF-THM-00032 Beck-Chevalley para imágenes 4.4.3 N Sin correspondencia acreditada
TF-THM-00033 Criterio estructural de función total 5.1.3 N Sin correspondencia acreditada
TF-THM-00034 Selector si y sólo si sección 5.2.2 N Sin correspondencia acreditada
TF-THM-00035 Caracterización relacional de los objetos proyectivos 5.2.4 N Sin correspondencia acreditada
TF-THM-00036 Equivalencias del axioma de elección regular 5.2.6 N Sin correspondencia acreditada
TF-THM-00037 Elección única y naturalidad por cambio de base 5.3.1 N Sin correspondencia acreditada
TF-THM-00038 Tres formulaciones equivalentes de AC en ZF 5.3.2 N Sin correspondencia acreditada
TF-THM-00039 La existencia única define una función en ZF, sin AC 5.3.3 N Sin correspondencia acreditada
TF-THM-00040 La elección ya realizada es estable por sustitución 5.4.1 N Sin correspondencia acreditada
TF-THM-00041 Equivalencia con relaciones univaluadas 6.1.2 N Sin correspondencia acreditada
TF-THM-00042 Recuperación de flechas totales 6.1.4 N Sin correspondencia acreditada
TF-THM-00043 Construcción de Par(C) 6.2.2 N Sin correspondencia acreditada
TF-THM-00044 Inclusión fiel de aplicaciones totales 6.2.3 N Sin correspondencia acreditada
TF-THM-00045 Orden parcial y compatibilidad con composición 6.3.2 N Sin correspondencia acreditada
TF-THM-00046 Leyes del operador de restricción 6.3.4 N Sin correspondencia acreditada
TF-THM-00047 Inyectividad y extensión total universal 6.4.2 N Sin correspondencia acreditada
TF-THM-00048 Criterio de extensión en ZF sin AC 6.4.3 N Sin correspondencia acreditada
TF-THM-00049 Conjuntos inyectivos si y sólo si habitados 6.4.4 N Sin correspondencia acreditada
TF-THM-00050 Extensión restringida equivalente a AC 6.4.5 N Sin correspondencia acreditada
TF-THM-00051 Representación por B más indefinición en Set 6.6.1 N Sin correspondencia acreditada
TF-THM-00052 Verdad parametrizada y equivalencia de dominios 7.1.2 N Sin correspondencia acreditada
TF-THM-00053 Leyes de restricción y maximalidad 7.2.2 N Sin correspondencia acreditada
TF-THM-00054 Dominio exacto de composición parcial 7.2.3 N Sin correspondencia acreditada
TF-THM-00055 Sustitución por aplicación total 7.2.4 N Sin correspondencia acreditada
TF-THM-00056 Igualdad por dominio y valores 7.3.2 N Sin correspondencia acreditada
TF-THM-00057 Conjunción clasifica intersección 7.3.3 N Sin correspondencia acreditada
TF-THM-00058 Cuantificación existencial sucesiva 7.4.2 N Sin correspondencia acreditada
TF-THM-00059 Dominio como proyección existencial de gráfica 7.4.3 N Sin correspondencia acreditada
TF-THM-00060 Totalidad y comparación lógica de dominios 7.4.4 N Sin correspondencia acreditada
TF-THM-00061 Unicidad esencial del clasificador 8.1.2 N Sin correspondencia acreditada
TF-THM-00062 Existencia y universalidad de \(L(B)\) en todo topos elemental 8.2.2 N Sin correspondencia acreditada
TF-THM-00063 \(L(1)\) es el clasificador de subobjetos 8.2.3 N Sin correspondencia acreditada
TF-THM-00064 Modelo clásico \(L(B)\cong B\sqcup1\) 8.3.1 N Sin correspondencia acreditada
TF-THM-00065 En un topos booleano, \(c_B\) es isomorfismo 8.4.2 N Sin correspondencia acreditada
TF-THM-00066 Caracterización lógica por \(c_1\) 8.4.3 N Sin correspondencia acreditada
TF-THM-00067 Funtorialidad del levantamiento 8.5.1 N Sin correspondencia acreditada
TF-THM-00068 Composición parcial como composición de mapas totales levantados 8.5.2 N Sin correspondencia acreditada
TF-THM-00069 Dominio semidecidible 9.1.3 N Sin correspondencia acreditada
TF-THM-00070 Criterio efectivo por la gráfica 9.1.4 N Sin correspondencia acreditada
TF-THM-00071 Cualquier conjunto c.e. puede ser un dominio 9.1.5 N Sin correspondencia acreditada
TF-THM-00072 Dominio decidible permite extensión computable 9.2.2 N Sin correspondencia acreditada
TF-THM-00073 Criterio exacto para la totalización etiquetada 9.2.4 N Sin correspondencia acreditada
TF-THM-00074 Composición de funciones parciales computables 9.3.1 N Sin correspondencia acreditada
TF-THM-00075 Los nombres pueden diferir sin alterar el valor 9.4.2 N Sin correspondencia acreditada
TF-THM-00076 Transporte correcto de computabilidad 9.4.4 N Sin correspondencia acreditada
TF-THM-00077 Puente para los naturales discretamente representados, con una advertencia 9.4.5 N Sin correspondencia acreditada
TF-THM-00078 Los programas parciales de parada forman una categoría efectiva 9.4.7 N Sin correspondencia acreditada
TF-THM-00079 Cociente extensional y composición 10.1.2 N Sin correspondencia acreditada
TF-THM-00080 La equivalencia parcial no es c.e. ni co-c.e. 10.2.2 N Sin correspondencia acreditada
TF-THM-00081 Ninguna batería finita de entradas certifica la igualdad universal 10.2.3 N Sin correspondencia acreditada
TF-THM-00082 Igualdad de programas totales bajo promesa 10.3.1 N Sin correspondencia acreditada
TF-THM-00083 Rice, reconstrucción con la función vacía 10.3.3 N Sin correspondencia acreditada
TF-THM-00084 Decisión por comparación exhaustiva certificada 10.4.2 N Sin correspondencia acreditada
TF-THM-00085 Desigualdad semidecidible, igualdad real indecidible 10.5.2 N Sin correspondencia acreditada
TF-THM-00086 No existe normalizador computable universal de índices extensionales 10.5.4 N Sin correspondencia acreditada
TF-THM-00087 Clasificar igualdad no equivale a decidirla 10.6.1 N Sin correspondencia acreditada
TF-THM-00088 Lema diagonal para familias totales 11.1.2 C diagonal_ne_section
TF-THM-00089 Punto fijo a partir de enumeración exhaustiva 11.1.3 C fixedPoint_of_surjective_sections
TF-THM-00090 Teorema de Cantor por diagonalización 11.1.4 P cantor_predicate
TF-THM-00091 Teorema del punto fijo de Lawvere 11.2.2 N Sin correspondencia acreditada
TF-THM-00092 Existencia de simulador universal parcial 11.3.2 N Sin correspondencia acreditada
TF-THM-00093 Imposibilidad de enumeración total computable universal 11.3.3 N Sin correspondencia acreditada
TF-THM-00094 La diagonal parcial fuerza una indefinición 11.3.4 N Sin correspondencia acreditada
TF-THM-00095 Indecidibilidad del conjunto diagonal de parada 11.3.5 N Sin correspondencia acreditada
TF-THM-00096 Autoaplicación de variable imposible en tipos simples 12.1.2 N Sin correspondencia acreditada
TF-THM-00097 Diagonal categórica sin autoaplicación 12.1.5 N Sin correspondencia acreditada
TF-THM-00098 No sobreyectividad bajo reindexación sobreyectiva 12.2.2 C reindexed_diagonal_ne_section
TF-THM-00099 Factorización por cociente extensional 12.3.2 N Sin correspondencia acreditada
TF-THM-00100 Teorema de recursión extensional de programas 12.4.2 N Sin correspondencia acreditada
TF-THM-00101 Inexistencia de conjunto universal en ZF 12.5.2 N Sin correspondencia acreditada
TF-THM-00102 Compatibilidad exacta de gráficas con sustitución y composición 13.1.2 P graph13_precompose
TF-THM-00103 Ley beta categórica para la abstracción y la aplicación 13.2.2 P set_beta_uncurry_curry
TF-THM-00104 Ley eta categórica y recuperación de la abstracción 13.2.3 P set_eta_curry_uncurry
TF-THM-00105 Recuperación natural de una flecha (Yoneda elemental) 13.3.2 N Sin correspondencia acreditada
TF-THM-00106 Secciones y selección de valores: correspondencia sin elección 13.4.2 N Sin correspondencia acreditada
TF-THM-00107 Extraer un selector de un testigo dependiente explícito 13.4.4 N Sin correspondencia acreditada
TF-THM-00108 El olvido de la computabilidad es fiel pero no pleno 13.5.2 N Sin correspondencia acreditada
TF-THM-00109 Criterio de equivalencia categórica con representantes suministrados 14.1.2 N Sin correspondencia acreditada
TF-THM-00110 Correspondencia exacta entre aplicaciones parciales y flechas etiquetadas 14.2.2 N Sin correspondencia acreditada
TF-THM-00111 Las equivalencias de nombres transportan la computabilidad 14.3.3 P names14_transport
TF-THM-00112 No existe un cociente universal efectivo con igualdad decidible 14.4.2 N Sin correspondencia acreditada
TF-THM-00113 Criterio exacto de recuperación por observadores 14.5.2 P observer14_injective
TF-THM-00114 El cambio de coordenadas transporta funciones, pero no por sí solo algoritmos 14.5.4 P transport14_inverse
TF-THM-00115 Categoría de funtores y transformaciones naturales 15.1.3 N Sin correspondencia acreditada
TF-THM-00116 Invertibilidad componente a componente 15.1.4 N Sin correspondencia acreditada
TF-THM-00117 Lema de Yoneda contravariante con reconstrucción explícita 15.2.2 N Sin correspondencia acreditada
TF-THM-00118 Yoneda covariante 15.2.3 N Sin correspondencia acreditada
TF-THM-00119 Naturalidad de la biyección de Yoneda 15.2.4 N Sin correspondencia acreditada
TF-THM-00120 El encaje de Yoneda es pleno y fiel 15.2.5 P yoneda15_map_natural
TF-THM-00121 Criterio de fidelidad por sondas 15.3.2 N Sin correspondencia acreditada
TF-THM-00122 Monomorfismos de diagramas conjuntistas detectados por componentes 15.3.4 N Sin correspondencia acreditada
TF-THM-00123 Las transformaciones naturales entre productos son funciones 15.4.1 P product15_natural
TF-THM-00124 Los colímites pequeños de prehaces se calculan por componentes 16.1.2 N Sin correspondencia acreditada
TF-THM-00125 Categoría bien definida, pequeña y proyectada 16.1.4 N Sin correspondencia acreditada
TF-THM-00126 Compatibilidad del cocono 16.2.2 N Sin correspondencia acreditada
TF-THM-00127 Densidad de Yoneda: todo prehaz es un colímite canónico de representables 16.2.3 P density16Equiv
TF-THM-00128 Fórmula puntual, clases y forma normal de cada elemento 16.2.4 N Sin correspondencia acreditada
TF-THM-00129 Fórmula co-Yoneda sin elección 16.3.2 N Sin correspondencia acreditada
TF-THM-00130 La reconstrucción es natural respecto del prehaz 16.4.1 N Sin correspondencia acreditada
TF-THM-00131 Los representables detectan conjuntamente transformaciones 16.4.2 P density16_detect
TF-THM-00132 Criterio exacto de representabilidad por objeto terminal de elementos 16.4.3 N Sin correspondencia acreditada
TF-THM-00133 Correspondencia entre transformaciones y familias compatibles 16.4.4 N Sin correspondencia acreditada

D.5. Formulación literal y dependencias de los módulos

Transcripción del código auditado en cada SHA de cabeza. Incluye auxiliares y pruebas para evitar perder hipótesis implícitas al aislar una firma. Los imports son dependencias de módulo; no constituyen un inventario transitivo de axiomas ni una atribución de todos los resultados importados al tratado.

Diagonalizacion.lean

Fuente inmutable. SHA-256 del archivo: 559e9289db5e5c3e83154b0d35f1c54158cdf3899f55251f4e0dd858e02a25ce.

import Mathlib

/-!
# TF-CAT-011: evaluación universal y diagonalización

La semántica formalizada aquí es la de familias de **funciones totales** entre tipos.
No se declara ningún intérprete de máquinas de Turing ni se identifica una
familia total con una familia de funciones parcialmente computables.

Correspondencia editorial:
* TF-THM-00088: `diagonal_ne_section` y `no_surjective_sections`.
* TF-THM-00089: `fixedPoint_of_surjective_sections`.
* TF-THM-00090: `cantor_predicate` (versión de predicados/subconjuntos).

Todas las pruebas sustanciales están desarrolladas aquí; Mathlib proporciona
los tipos de funciones, la noción `Function.Surjective` y la lógica de Lean.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u v

variable {A : Type u} {B : Type v}

/-- TF-THM-00088: la diagonal perturbada difiere de cada sección total. -/
theorem diagonal_ne_section (U : A → A → B) (s : B → B)
    (hs : ∀ b : B, s b ≠ b) (a : A) :
    (fun x : A => s (U x x)) ≠ U a := by
  intro h
  have hpoint : s (U a a) = U a a := congrFun h a
  exact hs (U a a) hpoint

/-- TF-THM-00089: una enumeración exhaustiva produce un punto fijo. -/
theorem fixedPoint_of_surjective_sections (U : A → A → B)
    (hU : Function.Surjective (fun a : A => U a)) (s : B → B) :
    ∃ b : B, s b = b := by
  obtain ⟨a, ha⟩ := hU (fun x : A => s (U x x))
  refine ⟨U a a, ?_⟩
  exact (congrFun ha a).symm

/-- TF-THM-00088: versión de imposibilidad de sobreyectividad. -/
theorem no_surjective_sections (U : A → A → B) (s : B → B)
    (hs : ∀ b : B, s b ≠ b) :
    ¬ Function.Surjective (fun a : A => U a) := by
  intro hU
  obtain ⟨b, hb⟩ := fixedPoint_of_surjective_sections U hU s
  exact hs b hb

/-- TF-THM-00090: Cantor para funciones con codominio de predicados. -/
theorem cantor_predicate (U : A → A → Prop) :
    ¬ Function.Surjective (fun a : A => U a) := by
  intro hU
  obtain ⟨a, ha⟩ := hU (fun x : A => ¬ U x x)
  have hdiag : U a a = (¬ U a a) := congrFun ha a
  have hn : ¬ U a a := by
    intro hp
    exact (Eq.mp hdiag hp) hp
  exact hn (Eq.mpr hdiag hn)

end MatematicaAbierta.TeoriaDeFunciones

Reindexacion.lean

Fuente inmutable. SHA-256 del archivo: bbc1d5612ec9c7f1708eb5f11cb2651c976ce2a40f54bc036ff1515459bf4d98.

import MatematicaAbierta.TeoriaDeFunciones.Diagonalizacion

/-!
# TF-CAT-012: reindexación de familias de funciones y extensionalidad

Correspondencia exacta:
* TF-THM-00098: `reindexed_diagonal_ne_section` y
  `reindexed_no_surjective_sections`.
* TF-DEF-00051: `extensional_sections_iff` comprueba la equivalencia
  entre igualdad funcional e igualdad puntual de secciones.

No se declara formalizado el teorema de recursión de Kleene, la sintaxis
completa del cálculo simplemente tipado ni el cociente extensional
`TF-THM-00099`. No se añaden axiomas ni marcadores de prueba incompleta.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u v w
variable {P : Type u} {A : Type v} {B : Type w}

/-- TF-THM-00098: la diagonal reindexada difiere de cada sección cuando
    la aplicación de argumentos a índices es sobreyectiva. -/
theorem reindexed_diagonal_ne_section (U : P → A → B) (q : A → P)
    (hq : Function.Surjective q) (s : B → B)
    (hs : ∀ b : B, s b ≠ b) (p : P) :
    (fun a : A => s (U (q a) a)) ≠ U p := by
  intro h
  obtain ⟨a, ha⟩ := hq p
  have hpoint : s (U p a) = U p a := by
    simpa only [ha] using congrFun h a
  exact hs (U p a) hpoint

/-- TF-THM-00098: no hay representación exhaustiva de todas las funciones
    mediante las secciones de una familia reindexada sobreyectivamente. -/
theorem reindexed_no_surjective_sections (U : P → A → B) (q : A → P)
    (hq : Function.Surjective q) (s : B → B)
    (hs : ∀ b : B, s b ≠ b) :
    ¬ Function.Surjective (fun p : P => U p) := by
  intro hU
  obtain ⟨p, hp⟩ := hU (fun a : A => s (U (q a) a))
  exact reindexed_diagonal_ne_section U q hq s hs p hp.symm

/-- TF-DEF-00051: criterio extensional de equivalencia semántica de índices.
    No se afirma decidibilidad de ninguno de los dos lados. -/
theorem extensional_sections_iff (U : P → A → B) (p r : P) :
    (∀ a : A, U p a = U r a) ↔ U p = U r := by
  constructor
  · intro h
    funext a
    exact h a
  · intro h a
    exact congrFun h a

end MatematicaAbierta.TeoriaDeFunciones

Correspondencias.lean

Fuente inmutable. SHA-256 del archivo: 658910c5de681361965a9675f4a7159020792387632acc1c566d9b26fefbf41c.

import MatematicaAbierta.TeoriaDeFunciones.Reindexacion

/-!
# TF-CAT-013: correspondencias entre funciones, gráficas y exponenciales en Set

Alcance exacto:
* `TF-THM-00102`: sustitución y composición de gráficas como predicados
  en conjuntos interpretados por tipos Lean.
* `TF-THM-00103`: instancia en `Set` de la ley beta de currificación.
* `TF-THM-00104`: instancia en `Set` de la ley eta de currificación.

No se declaran formalizados el teorema categórico en una CCC arbitraria,
Yoneda (`TF-THM-00105`), los tipos dependientes del manuscrito ni el
contraejemplo computacional (`TF-THM-00108`).
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u v w z
variable {A : Type u} {A' : Type v} {B : Type w} {C : Type z}

/-- Relación gráfica de una función en el modelo de conjuntos/tipos. -/
def graph13 (f : A → B) (a : A) (b : B) : Prop := b = f a

/-- TF-THM-00102, sustitución: la gráfica de una composición es la
    preimagen de la gráfica de la segunda función. -/
theorem graph13_precompose (f : A → B) (u : A' → A) (a : A') (b : B) :
    graph13 (fun x => f (u x)) a b ↔ graph13 f (u a) b := Iff.rfl

/-- TF-THM-00102, composición relacional de gráficas en Set. -/
theorem graph13_compose (f : A → B) (g : B → C) (a : A) (c : C) :
    (∃ b : B, graph13 f a b ∧ graph13 g b c) ↔
      graph13 (fun x => g (f x)) a c := by
  constructor
  · rintro ⟨b, hb, hc⟩
    dsimp [graph13] at hb hc ⊢
    calc
      c = g b := hc
      _ = g (f a) := congrArg g hb
  · intro h
    exact ⟨f a, rfl, h⟩

/-- TF-THM-00103: ley beta para la adjunción producto/exponencial en Set. -/
theorem set_beta_uncurry_curry (h : A × B → C) :
    (fun p : A × B => (fun x : A => fun y : B => h (x, y)) p.1 p.2) = h := by
  funext p
  rcases p with ⟨x, y⟩
  rfl

/-- TF-THM-00104: ley eta para la adjunción producto/exponencial en Set. -/
theorem set_eta_curry_uncurry (k : A → B → C) :
    (fun x : A => fun y : B => (fun p : A × B => k p.1 p.2) (x, y)) = k := by
  funext x y
  rfl

end MatematicaAbierta.TeoriaDeFunciones

SemanticaEquivalencia.lean

Fuente inmutable. SHA-256 del archivo: 32b2188fdf2948cd88e284075d6b8da4422a91bdb0486826db2bee1a5d1f3f2b.

import MatematicaAbierta.TeoriaDeFunciones.Correspondencias

/-!
# TF-CAT-014: semántica de nombres, observadores y cambios de coordenadas

Cobertura estricta:
* TF-THM-00111: sólo identidad de denotaciones bajo traductores TOTALES
  suministrados; no se formaliza su computabilidad ni dominios parciales.
* TF-THM-00113: criterio suficiente para un observador inyectivo en Set.
* TF-THM-00114: transporte e inversa de funciones mediante `Equiv` de tipos,
  y compatibilidad de los transportes con composición (modelo Set).

Ninguna de estas pruebas demuestra equivalencia de categorías arbitrarias,
Kleisli, computabilidad de traducciones ni indecidibilidad del cociente.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u v w x y z

/-- TF-THM-00111 (instancia semántica): composición correcta de nombres.
    No afirma que las funciones provistas sean computables. -/
theorem names14_transport
    {X : Type u} {Y : Type v}
    (δX δX' : Nat → X) (δY δY' : Nat → Y)
    (TX TY F : Nat → Nat) (f : X → Y)
    (hX : ∀ n, δX (TX n) = δX' n)
    (hY : ∀ n, δY' (TY n) = δY n)
    (hF : ∀ n, δY (F n) = f (δX n)) (n : Nat) :
    δY' (TY (F (TX n))) = f (δX' n) := by
  calc
    δY' (TY (F (TX n))) = δY (F (TX n)) := hY _
    _ = f (δX (TX n)) := hF _
    _ = f (δX' n) := congrArg f (hX n)

/-- TF-THM-00113 (instancia): un observador inyectivo separa dos funciones. -/
theorem observer14_injective
    {A : Type u} {B : Type v} {C : Type w}
    (t : B → C) (ht : Function.Injective t) (f g : A → B)
    (h : t ∘ f = t ∘ g) : f = g := by
  funext a
  exact ht (congrFun h a)

/-- Transporte de una flecha por equivalencias de tipos. -/
def transport14 {A : Type u} {A' : Type v} {B : Type w} {B' : Type x}
    (eA : A ≃ A') (eB : B ≃ B') (f : A → B) : A' → B' :=
  fun a' => eB (f (eA.symm a'))

/-- TF-THM-00114 (Set): el transporte inverso recupera la función. -/
theorem transport14_inverse
    {A : Type u} {A' : Type v} {B : Type w} {B' : Type x}
    (eA : A ≃ A') (eB : B ≃ B') (f : A → B) :
    transport14 eA.symm eB.symm (transport14 eA eB f) = f := by
  funext a
  simp [transport14]

/-- TF-THM-00114 (Set): compatibilidad de los cambios con composición. -/
theorem transport14_comp
    {A : Type u} {A' : Type v} {B : Type w} {B' : Type x}
    {C : Type y} {C' : Type z}
    (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃ C')
    (f : A → B) (g : B → C) :
    transport14 eA eC (g ∘ f) =
      (transport14 eB eC g) ∘ (transport14 eA eB f) := by
  funext a'
  simp [transport14]

end MatematicaAbierta.TeoriaDeFunciones

NaturalidadSondas.lean

Fuente inmutable. SHA-256 del archivo: 65ea525dedb3abbca1ebf383e6534fac97f28140e2d90bbc6d802483340947d8.

import MatematicaAbierta.TeoriaDeFunciones.SemanticaEquivalencia

/-!
# TF-CAT-015: naturalidad, Yoneda en Set y productos

Cobertura estricta: instancia Set de TF-THM-00120 mediante recuperación,
plenitud y fidelidad de transformaciones naturales de representables;
instancia Set de TF-THM-00123 para naturalidad y recuperación de productos.
No formaliza el lema de Yoneda para categorías arbitrarias, tamaño de
categorías de funtores ni decidibilidad o computabilidad.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u

/-- Acción sobre flechas de la representación contravariante en Set. -/
def yoneda15Map {A B : Type u} (f : A → B)
    (X : Type u) (g : X → A) : X → B := f ∘ g

/-- TF-THM-00120 (Set): la acción representable es natural. -/
theorem yoneda15_map_natural {A B X Y : Type u}
    (f : A → B) (g : X → A) (u : Y → X) :
    yoneda15Map f Y (g ∘ u) = (yoneda15Map f X g) ∘ u := by
  funext y
  rfl

/-- TF-THM-00120 (Set): recuperar una familia natural por su identidad. -/
theorem yoneda15_recover {A B : Type u}
    (α : (X : Type u) → (X → A) → (X → B))
    (hnat : ∀ (X Y : Type u) (u : Y → X) (g : X → A),
      α Y (g ∘ u) = (α X g) ∘ u)
    (X : Type u) (g : X → A) :
    α X g = (α A id) ∘ g := by
  have h := hnat A X g (id : A → A)
  change α X g = (α A id) ∘ g at h
  exact h

/-- TF-THM-00120 (Set): plenitud y unicidad del mapa recuperado. -/
theorem yoneda15_full {A B : Type u}
    (α : (X : Type u) → (X → A) → (X → B))
    (hnat : ∀ (X Y : Type u) (u : Y → X) (g : X → A),
      α Y (g ∘ u) = (α X g) ∘ u) :
    ∃! f : A → B, ∀ (X : Type u) (g : X → A),
      α X g = yoneda15Map f X g := by
  refine ⟨α A id, ?_, ?_⟩
  · intro X g
    exact yoneda15_recover α hnat X g
  · intro f hf
    have h := hf A (id : A → A)
    simpa [yoneda15Map] using h.symm

/-- TF-THM-00120 (Set): fidelidad de la representación. -/
theorem yoneda15_faithful {A B : Type u} (f g : A → B)
    (h : ∀ (X : Type u) (k : X → A),
      yoneda15Map f X k = yoneda15Map g X k) : f = g := by
  have hi := h A (id : A → A)
  simpa [yoneda15Map] using hi

/-- TF-THM-00123 (Set): familia natural asociada a h : A → B. -/
def product15 {A B : Type u} (h : A → B)
    (X : Type u) (p : X × A) : X × B := (p.1, h p.2)

/-- TF-THM-00123 (Set): la familia construida conmuta con parámetros. -/
theorem product15_natural {A B X Y : Type u}
    (h : A → B) (u : X → Y) (p : X × A) :
    product15 h Y (u p.1, p.2) =
      (u (product15 h X p).1, (product15 h X p).2) := by
  rfl

/-- TF-THM-00123 (Set): todo producto natural se recupera en PUnit. -/
theorem product15_recover {A B : Type u}
    (α : (X : Type u) → X × A → X × B)
    (hnat : ∀ (X Y : Type u) (u : X → Y) (p : X × A),
      α Y (u p.1, p.2) = (u (α X p).1, (α X p).2))
    (X : Type u) (p : X × A) :
    α X p = (p.1, (α PUnit.{u+1} (PUnit.unit, p.2)).2) := by
  rcases p with ⟨x, a⟩
  let c : PUnit.{u+1} → X := fun _ => x
  have h := hnat PUnit.{u+1} X c (PUnit.unit, a)
  simpa [c] using h

end MatematicaAbierta.TeoriaDeFunciones

DensidadTerminal.lean

Fuente inmutable. SHA-256 del archivo: a778d72394297a06218d81155683816ce4cd7be4eca10ab3136e716d3136e1df.

import MatematicaAbierta.TeoriaDeFunciones.NaturalidadSondas

/-!
# TF-CAT-016: instancia conjuntista sobre la categoría terminal

Cobertura estricta y parcial: para la categoría con un objeto y sólo su identidad,
un prehaz es un conjunto S, los representables son unitarios y su categoría de
elementos es discreta con objetos S. La descomposición de S como coproducto de
unitarios y su propiedad universal son instancias de TF-THM-00127; la separación
por las inclusiones es instancia de TF-THM-00131. También se comprueba la parte
finita del contraejemplo TF-CEX-00022. No se formalizan el teorema de densidad
para categorías generales, coextremos, categorías de elementos arbitrarias,
condiciones de tamaño o decidibilidad.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

universe u v

/-- La suma de copias del conjunto unitario indexada por S se evalúa en S. -/
def density16Eval {S : Type u} : (Σ _ : S, PUnit) → S := fun p => p.1

/-- La inclusión del sumando unitario asociado a cada s. -/
def density16Incl {S : Type u} (s : S) : PUnit → S := fun _ => s

/-- TF-THM-00127, instancia terminal: la suma de representables unitarios es S. -/
def density16Equiv (S : Type u) : (Σ _ : S, PUnit) ≃ S where
  toFun := density16Eval
  invFun := fun s => ⟨s, PUnit.unit⟩
  left_inv := by
    intro p
    rcases p with ⟨s, z⟩
    cases z
    rfl
  right_inv := by
    intro s
    rfl

/-- TF-THM-00127, instancia terminal: la familia de unitarios es colimitante. -/
theorem density16_universal (S : Type u) (T : Type v)
    (cocone : (s : S) → PUnit → T) :
    ∃! f : S → T, ∀ s : S, (fun z : PUnit => f (density16Incl s z)) = cocone s := by
  refine ⟨fun s => cocone s PUnit.unit, ?_, ?_⟩
  · intro s
    funext z
    cases z
    rfl
  · intro f hf
    funext s
    have h := congrFun (hf s) PUnit.unit
    simpa [density16Incl] using h

/-- TF-THM-00131, instancia terminal: las sondas unitarias separan funciones. -/
theorem density16_detect {S : Type u} {T : Type v} (f g : S → T)
    (h : ∀ s : S,
      (fun z : PUnit => f (density16Incl s z)) =
      (fun z : PUnit => g (density16Incl s z))) : f = g := by
  funext s
  have hs := congrFun (h s) PUnit.unit
  simpa [density16Incl] using hs

/-- TF-CEX-00022, caso de dos elementos: Bool no es un representable unitario. -/
theorem density16_bool_not_unit : ¬ Nonempty (Bool ≃ PUnit) := by
  rintro ⟨e⟩
  have h : (true : Bool) = false :=
    e.injective (Subsingleton.elim (e true) (e false))
  cases h

end MatematicaAbierta.TeoriaDeFunciones

GraficasEstructurales.lean

Fuente inmutable. SHA-256 del archivo: f29d512f0407fe0755db7ce407f5b8463d5574312a68c342148b727ec88aedaf.

import Mathlib.CategoryTheory.Subobject.Basic
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts

/-!
# TF-THM-00005: caracterización estructural de las gráficas

Marco: categoría arbitraria con un producto binario elegido para A y B.
Los subobjetos se comparan como clases de monomorfismos, no por igualdad
literal de sus flechas representantes. No se supone regularidad ni elección
en la teoría objeto. `inv`/`Subobject` pueden utilizar elección metateórica
para escoger representantes: la demostración categórica no postula AC.
-/

namespace MatematicaAbierta.TeoriaDeFunciones

open CategoryTheory CategoryTheory.Limits

-- La instancia local de invertibilidad es una prueba (Prop); `letI` es necesario
-- para que Lean pueda elaborar `inv` y `asIso`, incluso dentro de una prueba.
set_option linter.style.haveILetI false

universe v u
variable {C : Type u} [Category.{v} C]
variable {A B R : C} [HasBinaryProduct A B]

/-- Flecha gráfica `⟨𝟙 A, f⟩ : A ⟶ A ⨯ B`. -/
noncomputable def graphStructural (f : A ⟶ B) : A ⟶ A ⨯ B :=
  prod.lift (𝟙 A) f

instance graphStructural_mono (f : A ⟶ B) : Mono (graphStructural f) := by
  unfold graphStructural
  infer_instance

@[simp]
theorem graphStructural_fst (f : A ⟶ B) :
    graphStructural f ≫ prod.fst = 𝟙 A := prod.lift_fst _ _

@[simp]
theorem graphStructural_snd (f : A ⟶ B) :
    graphStructural f ≫ prod.snd = f := prod.lift_snd _ _

/-- La igualdad de subobjetos gráficos proporciona un isomorfismo de
representantes sobre el producto. -/
private theorem graphStructural_rep_witness (m : R ⟶ A ⨯ B) [Mono m]
    (f : A ⟶ B) (h : Subobject.mk m = Subobject.mk (graphStructural f)) :
    (Subobject.isoOfMkEqMk m (graphStructural f) h).hom ≫ graphStructural f = m := by
  change Subobject.ofMkLEMk m (graphStructural f) h.le ≫ graphStructural f = m
  exact Subobject.ofMkLEMk_comp h.le

/-- TF-THM-00005: un mono representa la gráfica de una flecha exactamente
cuando su primera proyección es un isomorfismo. -/
theorem tf_thm_00005 (m : R ⟶ A ⨯ B) [Mono m] :
    (∃ f : A ⟶ B, Subobject.mk m = Subobject.mk (graphStructural f)) ↔
      IsIso (m ≫ prod.fst) := by
  constructor
  · rintro ⟨f, h⟩
    let i : R ≅ A := Subobject.isoOfMkEqMk m (graphStructural f) h
    have wi : i.hom ≫ graphStructural f = m :=
      graphStructural_rep_witness m f h
    have hp : i.hom = m ≫ prod.fst := by
      calc
        i.hom = i.hom ≫ (𝟙 A) := by simp
        _ = (i.hom ≫ graphStructural f) ≫ prod.fst := by simp [Category.assoc]
        _ = m ≫ prod.fst := by rw [wi]
    rw [← hp]
    infer_instance
  · intro hi
    letI : IsIso (m ≫ prod.fst) := hi
    let p : R ⟶ A := m ≫ prod.fst
    let f : A ⟶ B := inv p ≫ (m ≫ prod.snd)
    refine ⟨f, ?_⟩
    apply Subobject.mk_eq_mk_of_comm m (graphStructural f) (asIso p)
    apply prod.hom_ext
    · simp [graphStructural, Category.assoc, p]
    · change (p ≫ graphStructural f) ≫ prod.snd = m ≫ prod.snd
      calc
        (p ≫ graphStructural f) ≫ prod.snd = p ≫ f := by
          simp [Category.assoc]
        _ = (p ≫ inv p) ≫ (m ≫ prod.snd) := by
          simp [f]
        _ = m ≫ prod.snd := by simp

/-- La recuperación usa una instancia explícita de `IsIso` únicamente para
que `inv` sea una expresión bien tipada. El teorema principal demuestra que
dicha instancia se obtiene de la condición gráfica, sin hipótesis axiomáticas. -/
theorem tf_thm_00005_recover (m : R ⟶ A ⨯ B) [Mono m]
    [IsIso (m ≫ prod.fst)]
    (f : A ⟶ B) (h : Subobject.mk m = Subobject.mk (graphStructural f)) :
    f = inv (m ≫ prod.fst) ≫ (m ≫ prod.snd) := by
  let i : R ≅ A := Subobject.isoOfMkEqMk m (graphStructural f) h
  have wi : i.hom ≫ graphStructural f = m :=
    graphStructural_rep_witness m f h
  have hp : i.hom = m ≫ prod.fst := by
    calc
      i.hom = i.hom ≫ (𝟙 A) := by simp
      _ = (i.hom ≫ graphStructural f) ≫ prod.fst := by simp [Category.assoc]
      _ = m ≫ prod.fst := by rw [wi]
  have hq : i.hom ≫ f = m ≫ prod.snd := by
    calc
      i.hom ≫ f = (i.hom ≫ graphStructural f) ≫ prod.snd := by
        simp [Category.assoc]
      _ = m ≫ prod.snd := by rw [wi]
  have hInv : inv (m ≫ prod.fst) = i.inv := by
    apply IsIso.inv_eq_of_hom_inv_id
    rw [← hp]
    exact i.hom_inv_id
  symm
  calc
    inv (m ≫ prod.fst) ≫ (m ≫ prod.snd) = i.inv ≫ (i.hom ≫ f) := by
      rw [hInv, ← hq]
    _ = (i.inv ≫ i.hom) ≫ f := (Category.assoc _ _ _).symm
    _ = f := by simp

/-- La función representada es única para el producto A ⨯ B fijado. -/
theorem tf_thm_00005_unique (m : R ⟶ A ⨯ B) [Mono m]
    (f g : A ⟶ B)
    (hf : Subobject.mk m = Subobject.mk (graphStructural f))
    (hg : Subobject.mk m = Subobject.mk (graphStructural g)) : f = g := by
  letI : IsIso (m ≫ prod.fst) := (tf_thm_00005 m).mp ⟨f, hf⟩
  calc
    f = inv (m ≫ prod.fst) ≫ (m ≫ prod.snd) := tf_thm_00005_recover m f hf
    _ = g := (tf_thm_00005_recover m g hg).symm

/-- Una sustitución isomorfa de representante no cambia la función recuperada.
Los dos testigos de `IsIso` indican explícitamente cuándo se define `inv`. -/
theorem tf_thm_00005_invariant {S : C} (m : R ⟶ A ⨯ B)
    (n : S ⟶ A ⨯ B) [Mono m] [Mono n]
    (e : R ≅ S) (he : e.hom ≫ n = m)
    [IsIso (m ≫ prod.fst)] [IsIso (n ≫ prod.fst)] :
    inv (m ≫ prod.fst) ≫ (m ≫ prod.snd) =
      inv (n ≫ prod.fst) ≫ (n ≫ prod.snd) := by
  obtain ⟨f, hf⟩ := (tf_thm_00005 m).mpr inferInstance
  obtain ⟨g, hg⟩ := (tf_thm_00005 n).mpr inferInstance
  have hmn : Subobject.mk m = Subobject.mk n :=
    Subobject.mk_eq_mk_of_comm m n e he
  have hfg : f = g := by
    have hgn : Subobject.mk m = Subobject.mk (graphStructural g) :=
      hmn.trans hg
    exact tf_thm_00005_unique m f g hf hgn
  calc
    inv (m ≫ prod.fst) ≫ (m ≫ prod.snd) = f :=
      (tf_thm_00005_recover m f hf).symm
    _ = g := hfg
    _ = inv (n ≫ prod.fst) ≫ (n ≫ prod.snd) :=
      tf_thm_00005_recover n g hg

end MatematicaAbierta.TeoriaDeFunciones

← Anterior · Índice del tratado · Siguiente →

Reutilización

GFDL-1.3-or-later