Glosario de conceptos definidos
Este glosario reúne las 73 definiciones formales del tratado y nueve voces articuladoras que remiten a su uso principal. Cada entrada sintetiza el texto definitorio y remite a su localizador canónico; las hipótesis y demostraciones se consultan en el capítulo de origen. No constituye un sistema de definiciones nuevo. Para voces que no tienen una definición independiente, véase el índice de conceptos.
Voces articuladoras
Estas síntesis explican usos centrales del libro; no crean definiciones formales ni resultados nuevos.
Función y flecha
En el recorrido categórico, las flechas, sus extremos, identidades y composición son datos iniciales. Su identificación con funciones conjuntistas requiere declarar el modelo; las comparaciones posteriores distinguen flecha, gráfica y código. Fuente: 1.1.1.
Gráfica
En una categoría con productos binarios, la flecha gráfica de \(f:A\to B\) es \(\langle1_A,f\rangle:A\to A\times B\). Es monomórfica; la identificación de una relación con una gráfica requiere las condiciones del capítulo 1. Fuente: 1.3.3.
Imagen
En el marco regular, la parte monomórfica de una factorización regular-epi/mono determina el menor subobjeto por el que factoriza la flecha. No se atribuye esta operación a límites finitos sin el paquete adicional. Fuente: 4.2.3.
Clasificador de subobjetos
Objeto \(\Omega\) con un mono desde el terminal que clasifica cada subobjeto mediante una única característica y un producto fibrado. No se identifica con el conjunto externo de dos valores en una categoría arbitraria. Fuente: 3.3.1.
Elección regular categórica
Hipótesis opcional que exige que todo epimorfismo regular admita una sección. Se distingue de la selección única en ZF, que no requiere AC, y de un algoritmo de elección. Fuente: 5.2.5.
Extensionalidad
La igualdad de flechas se compara con su coincidencia sobre sondas: los elementos globales bastan si el terminal es generador; sin esa hipótesis la coincidencia global no implica igualdad. Fuente: 2.1.3.
Yoneda
La correspondencia natural entre transformaciones desde un representable y elementos del funtor recupera la transformación evaluando en la identidad. Deben conservarse la varianza y las condiciones de tamaño. Fuente: 15.2.2.
Densidad de Yoneda
Para una categoría base pequeña, cada prehaz es el colímite canónico de representables indexado por su categoría de elementos. Ser ese colímite no significa que el propio prehaz sea representable. Fuente: 16.2.3.
Diagonalización
A partir de una familia evaluable y de un endomapa sin puntos fijos, la diagonal torcida construye una función que difiere de cada sección correspondiente. La evaluación, la universalidad y la reindexación son datos distintos. Fuente: 11.1.2.
Definiciones formales
Aplicación parcial
Clase de spans con brazo izquierdo monomórfico, identificados mediante isomorfismos compatibles con ambos brazos. Fuente: Definición 6.1.1.
Categoría de elementos de un prehaz
Categoría cuyos objetos son pares de un objeto de la base y un elemento del prehaz; una flecha satisface la ecuación contravariante de los valores indicada. Fuente: Definición 16.1.3.
Categoría de endomorfismos totales computables
Categoría de un único objeto cuyos endomorfismos son las funciones totales computables sobre los naturales, identificadas extensionalmente, con identidad y composición ordinarias. Fuente: Definición 13.5.1.
Categoría de prehaces
Categoría de funtores contravariantes desde la categoría base hacia conjuntos, con transformaciones naturales como flechas y condiciones de tamaño explícitas. Fuente: Definición 16.1.1.
Clasificador de aplicaciones parciales con codominio \(B\)
Objeto con un mono desde el codominio que convierte cada mapa parcial en una única flecha total mediante un cuadrado de producto fibrado. Fuente: Definición 8.1.1.
Cociente de índices por denotación
Conjunto cociente que identifica índices precisamente cuando tienen la misma denotación, sin atribuir una comparación efectiva general. Fuente: Definición 14.4.1.
Coincidencia en elementos globales
Dos flechas coinciden en los elementos globales cuando sus composiciones con cada flecha desde el terminal son iguales. Fuente: Definición 2.1.1.
Comparación canónica entre suma y levantamiento
Flecha desde la suma del codominio con el terminal hacia su objeto de levantamiento, que compara valor definido e indefinición. Fuente: Definición 8.4.1.
Complementación y decidibilidad interna de un dominio
En un topos elemental, un subobjeto \(U\) está complementado cuando \(U\vee\neg U=\top\) en su álgebra de Heyting; esto no equivale a decidir algorítmicamente pertenencia sobre nombres. Fuente: Definición 7.5.1.
Composición categórica
Composición de relaciones mediante el producto fibrado de sus representantes y la imagen de la flecha hacia el producto de extremos, en el marco regular. Fuente: Definición 4.3.1.
Composición de aplicaciones parciales
Composición de spans parciales construida mediante el producto fibrado del brazo de valores del primero y el brazo de dominio del segundo. Fuente: Definición 6.2.1.
Composición de relaciones en \(\mathbf{Set}\)
Relación que asocia dos extremos cuando existe un testigo intermedio relacionado con ambos. Fuente: Definición 3.5.1.
Comprensión relativa frente a comprensión irrestricta
La comprensión relativa separa dentro de un conjunto dado; la comprensión irrestricta pretende formar una totalidad sin esa base delimitada. Fuente: Definición 12.5.1.
Conjuntos semidecidibles y decidibles
Un conjunto es semidecidible si la máquina correspondiente termina exactamente en sus miembros; es decidible si hay una decisión total de pertenencia. Fuente: Definición 9.1.2.
Contrato de correspondencia fundacional
Datos y obligaciones que precisan qué se transporta entre marcos fundacionales y qué igualdad o equivalencia se conserva. Fuente: Definición 13.1.1.
Contrato de equivalencia de funciones
Contrato que distingue igualdad extensional, isomorfismo de presentaciones, equivalencia categórica y equivalencia efectiva de representaciones, con sus datos de transporte y recuperación. Fuente: Definición 14.1.1.
Denominación débilmente sobreyectiva por puntos
En una categoría cartesianamente cerrada, flecha \(A\to B^A\) tal que cada flecha \(A\to B\) es exactamente la sección de su familia evaluable asociada a algún punto global \(1\to A\); no se identifica con epimorfía categórica. Fuente: Definición 11.2.1.
Diagrama de representables y cocono elemental
Diagrama de objetos representables indexado por la categoría de elementos y cocono hacia el prehaz dado. Fuente: Definición 16.2.1.
Dominio efectivo y totalidad parcial
El dominio efectivo de un span parcial es la clase de su brazo monomórfico; el mapa parcial es total cuando ese brazo es un isomorfismo. Fuente: Definición 6.1.3.
El terminal como generador
El objeto terminal es generador cuando la coincidencia en todos sus puntos permite concluir igualdad de flechas. Fuente: Definición 2.1.2.
Elemento exponencial asociado a una flecha
Elemento global del exponencial obtenido al transponer una flecha mediante su propiedad universal. Fuente: Definición 2.5.1.
Elemento generalizado
Flecha hacia un objeto desde una fuente arbitraria, utilizada como parámetro o sonda. Fuente: Definición 2.4.1.
Elemento global
Flecha desde un objeto terminal hacia el objeto considerado. Fuente: Definición 1.2.2.
Epimorfismo regular
Flecha que es coigualador de algún par de flechas paralelas. Fuente: Definición 4.1.2.
Equivalencia semántica de índices totales
Relación entre índices totales que denotan la misma función; su cociente expresa identificación semántica. Fuente: Definición 12.3.1.
Espacio representado y realizador
Una representación es una aplicación parcial sobreyectiva desde nombres de Baire; un realizador transforma todos los nombres válidos de argumentos pertenecientes al dominio de la función en nombres de sus imágenes, sin imponer comportamiento fuera de esa promesa. Fuente: Definición 9.4.1.
Evaluación tipada de un exponencial
Flecha de evaluación del exponencial, definida únicamente para el par de tipos que determina su dominio y codominio. Fuente: Definición 12.1.4.
Evaluador universal parcial efectivo
Evaluador parcial computable que simula la función con el índice suministrado, conservando tanto sus valores como su dominio. Fuente: Definición 11.3.1.
Extensión total computable
Función total computable que coincide con la función parcial dada en todo su dominio efectivo. Fuente: Definición 9.2.1.
Familia con índices y argumentos de tipos distintos
Familia evaluable cuyos índices y argumentos pertenecen a tipos distintos; la reindexación debe declararse para construir la diagonal correspondiente. Fuente: Definición 12.2.1.
Familia conjuntista y sección sobre una base
En ZF, familia de fibras de una relación \(R\subseteq A\times B\), codificada por su proyección sobre \(A\); una sección suministra un elemento de cada fibra. Fuente: Definición 13.4.1.
Familia de observadores y separación
Familia especificada de flechas desde el codominio que separa flechas paralelas cuando la coincidencia de todas sus poscomposiciones permite concluir igualdad. Fuente: Definición 14.5.1.
Familia evaluable y sus secciones
Familia total evaluable con parámetros y argumentos, cuyas secciones se obtienen fijando un parámetro. Fuente: Definición 11.1.1.
Familia generadora de sondas
Familia de sondas que detecta la igualdad de flechas mediante todas las precomposiciones pertinentes. Fuente: Definición 15.3.1.
Función parcial computable sobre los naturales
Función parcial sobre los naturales computada por una máquina que termina exactamente en su dominio y devuelve allí sus valores. Fuente: Definición 9.1.1.
Función parcial etiquetada y composición de Kleisli
Codificación conjuntista de un mapa parcial mediante valores etiquetados e indefinición; su composición se expresa por la operación de Kleisli indicada. Fuente: Definición 14.2.1.
Funtor covariante y contravariante
Asignación de objetos y flechas que conserva identidades y composición; en el caso contravariante se invierte la dirección de las flechas. Fuente: Definición 15.1.1.
Funtor de elementos globales
Funtor que asigna a un objeto sus elementos globales y a una flecha la operación de poscomposición. Fuente: Definición 2.2.1.
Funtores Hom representables
Funtores dados por conjuntos de flechas desde o hacia un objeto; constituyen las sondas representables de Yoneda. Fuente: Definición 15.2.1.
Idempotente de dominio
Aplicación parcial que actúa como identidad sobre el dominio efectivo del mapa considerado. Fuente: Definición 6.3.3.
Igualdad de objetos bajo representación y nombres rápidos
La igualdad bajo representación compara los objetos denotados por nombres; los nombres rápidos de reales cumplen las cotas de aproximación fijadas. Fuente: Definición 10.5.1.
Igualdad sintáctica y equivalencia extensional
La igualdad sintáctica compara códigos; la equivalencia extensional compara dominios y valores de las funciones que denotan. Fuente: Definición 10.1.1.
Imagen directa de subobjetos
Imagen de la composición de una inclusión de subobjeto con la flecha considerada. Fuente: Definición 4.4.1.
Interpretación del fragmento funcional simplemente tipado
Interpretación de tipos y términos del fragmento simplemente tipado en una categoría cartesianamente cerrada elegida; los tipos flecha se interpretan mediante exponenciales y los juicios mediante flechas. Fuente: Definición 13.2.1.
Interpretación existencial por imagen
Cuantificación existencial de un subobjeto interpretada mediante su imagen a lo largo de una flecha en la categoría regular. Fuente: Definición 7.4.1.
Isomorfismo
Flecha que admite una inversa bilateral respecto de las identidades de dominio y codominio. Fuente: Definición 1.1.4.
Monomorfismo
Flecha cancelable por la izquierda: dos flechas con destino en su dominio son iguales si sus composiciones con ella coinciden. Fuente: Definición 1.3.2.
Numeración aceptable y especialización efectiva
Numeración efectiva dotada de universalidad y de un algoritmo de especialización con la ley s-m-n explícita. Fuente: Definición 12.4.1.
Objeto de subsingletons \(L(B)\)
Subobjeto del objeto potencia cuyos predicados tienen a lo sumo un miembro, construido mediante el igualador declarado; incluye el predicado vacío. Fuente: Definición 8.2.1.
Objeto inyectivo respecto de monomorfismos
Objeto que permite extender cualquier flecha hacia él a lo largo de un monomorfismo, bajo el contrato del capítulo. Fuente: Definición 6.4.1.
Objeto potencia, cuando existe
Exponencial \(\Omega^A\), cuando existe; su papel clasificador de subobjetos no lo identifica por definición con un conjunto de partes. Fuente: Definición 3.4.2.
Objeto proyectivo respecto de coberturas regulares
Objeto desde el que toda flecha hacia el codominio de una cobertura regular puede levantarse a su dominio. Fuente: Definición 5.2.3.
Orden de extensión
Un mapa parcial extiende a otro cuando su dominio y sus valores contienen los del segundo mediante la factorización compatible indicada. Fuente: Definición 6.3.1.
Predicado característico del dominio
Flecha hacia el clasificador de subobjetos que clasifica el mono de dominio de un mapa parcial. Fuente: Definición 7.1.1.
Predicado de coincidencia
Característica del igualador de dos flechas totales, construido por producto fibrado de la diagonal; el clasificador se requiere para expresarlo como predicado. Fuente: Definición 7.3.1.
Preimagen de un subobjeto
Subobjeto obtenido al cambiar de base un monomorfismo por el producto fibrado pertinente. Fuente: Definición 3.2.2.
Presentación finita certificada
Datos suministrados: lista exhaustiva y efectiva del conjunto de entrada, decisores totales de ambos dominios y procedimientos que calculan cada valor definido. Fuente: Definición 10.4.1.
Presentación por coextremo conjuntista
Presentación conjuntista por coextremo, construida como cociente de pares bajo la relación generada por las acciones de las flechas de la base. Fuente: Definición 16.3.1.
Problema de equivalencia de índices y semidecisión
Problema de reconocer si dos índices denotan la misma función parcial; la semidecisión exige la conducta de parada declarada para el conjunto de pares. Fuente: Definición 10.2.1.
Propiedad extensional de índices
Propiedad de índices cuyo valor depende sólo de la función parcial denotada y se conserva al reemplazar un programa por otro extensionalmente equivalente. Fuente: Definición 10.3.2.
Reducibilidad y equivalencia computable de representaciones
Una representación se reduce computablemente a otra si todo nombre válido de la primera puede traducirse a uno de la segunda del mismo objeto; la equivalencia exige traductores en ambos sentidos. Fuente: Definición 14.3.2.
Relación de \(A\) en \(B\)
Subobjeto del producto de los objetos que actúan como dominio y codominio de la relación. Fuente: Definición 3.1.3.
Restricción a un subobjeto
Mapa parcial obtenido al limitar el dominio a su intersección con el subobjeto indicado. Fuente: Definición 7.2.1.
Selector de una relación
Flecha cuya gráfica está contenida en la relación; proporciona una selección compatible con cada argumento. Fuente: Definición 5.2.1.
Sistema de nombres naturales
Representación mediante nombres naturales válidos y su aplicación de denotación, con las condiciones declaradas de dominio. Fuente: Definición 14.3.1.
Sondas representables y familias naturales
Familias de acciones sobre las sondas representables que respetan la naturalidad; no una selección de componentes independientes. Fuente: Definición 13.3.1.
Subobjeto
Clase de monomorfismos hacia un objeto, identificados mediante isomorfismos compatibles con sus inclusiones. Fuente: Definición 3.1.1.
Testigo dependiente frente a existencia proposicional
Un término en un producto de sumas dependientes suministra valores y pruebas; la mera existencia proposicional, especialmente truncada, no suministra la misma operación de extracción. Fuente: Definición 13.4.3.
Tipos simples y juicio de tipado
Gramática de tipos simples y reglas del juicio que asigna un tipo a una expresión en un contexto. Fuente: Definición 12.1.1.
Totalidad regular
Una relación es regularmente total cuando su primera proyección es un epimorfismo regular. Fuente: Definición 5.1.1.
Traductor computable entre representaciones
Operador computable que transforma todo nombre válido de una representación en un nombre del mismo objeto para otra representación. Fuente: Definición 9.4.3.
Transformación natural
Familia especificada de componentes entre funtores que satisface los cuadrados de naturalidad para cada flecha del índice. Fuente: Definición 15.1.2.
Univaluación
Una relación es univaluada cuando su primera proyección es un monomorfismo; esto expresa a lo sumo un valor por argumento. Fuente: Definición 5.1.2.