En la teoría de categorías , una rama abstracta de las matemáticas , y en sus aplicaciones a la lógica y la informática teórica , un objeto de lista es una definición abstracta de una lista , es decir, una secuencia ordenada finita .
Sea C una categoría con productos finitos y un objeto terminal 1. Un objeto de lista sobre un objeto A de C es:
tal que para cualquier objeto B de C con aplicaciones b : 1 → B y t : A × B → B , existe una única f : L A → B tal que el siguiente diagrama conmuta :
donde 〈id A , f〉denota la flecha inducida por la propiedad universal del producto cuando se aplica a id A (la identidad en A ) y f . La notación A * ( estrella al estilo de Kleene ) se utiliza a veces para indicar listas sobre A. [1]
En una categoría con un objeto terminal 1, coproductos binarios (denotados por +) y productos binarios (denotados por ×), un objeto de lista sobre A se puede definir como el álgebra inicial del endofunctor que actúa sobre los objetos por X ↦ 1 + ( A × X ) y en las flechas por f ↦ [id 1 ,〈id A , f〉]. [2]
Como todas las construcciones definidas por una propiedad universal , las listas sobre un objeto son únicas hasta el isomorfismo canónico .
El objeto L 1 (listado sobre el objeto terminal) tiene la propiedad universal de un objeto de número natural . En cualquier categoría con listas, se puede definir la longitud de una lista L A como el morfismo único l : L A → L 1 que hace que el siguiente diagrama conmute: [3]
