Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userPolygraphs of finite derivation type
157
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
Craig Squier proved that, if a monoid can be presented by a finite convergent string rewriting system, then it satisfies the homological finiteness condition left-FP3. Using this result, he constructed finitely presentable monoids with a decidable word problem, but that cannot be presented by finite convergent rewriting systems. Later, he introduced the condition of finite derivation type, which is a homotopical finiteness property on the presentation complex associated to a monoid presentation. He showed that this condition is an invariant of finite presentations and he gave a constructive way to prove this finiteness property based on the computation of the critical branchings: being of finite derivation type is a necessary condition for a finitely presented monoid to admit a finite convergent presentation. This survey presents Squiers results in the contemporary language of polygraphs and higher-dimensional categories, with new proofs and relations between them.
rate research
Read More
We study convergent (terminating and confluent) presentations of n-categories. Using the notion of polygraph (or computad), we introduce the homotopical property of finite derivation type for n-categories, generalizing the one introduced by Squier for word rewriting systems. We characterize this property by using the notion of critical branching. In particular, we define sufficient conditions for an n-category to have finite derivation type. Through examples, we present several techniques based on derivations of 2-categories to study convergent presentations by 3-polygraphs.
We present polygraphic programs, a subclass of Albert Burronis polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic interpretations, a termination proof method introduced by the second author, to characterize polygraphic programs that compute in polynomial time. We conclude with a characterization of polynomial time functions and non-deterministic polynomial time functions.
The notion of an internal preneighbourhood space on a finitely complete category with finite coproducts and a proper $(mathsf{E}, mathsf{M})$ system such that for each object $X$ the set of $mathsf{M}$-subobjects of $X$ is a complete lattice was initiated in cite{2020}. The notion of a closure operator, closed morphism and its near allies investigated in cite{2021-clos}. The present paper provides structural conditions on the triplet $(mathbb{A}, mathsf{E}, mathsf{M})$ (with $mathbb{A}$ lextensive) equivalent to the set of $mathsf{M}$-subobjects of an object closed under finite sums. Equivalent conditions for the set of closed embeddings (closed morphisms) closed under finite sums is also provided. In case when lattices of admissible subobjects (respectively, closed embeddings) are closed under finite sums, the join semilattice of admissible subobjects (respectively, closed embeddings) of a finite sum is shown to be a biproduct of the component join semilattices. Finally, it is shown whenever the set of closed morphisms is closed under finite sums, the set of proper (respectively, separated) morphisms are also closed under finite sums. This leads to equivalent conditions for the full subcategory of compact (respectively, Hausdorff) preneighbourhood spaces to be closed under finite sums.
This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a localization higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
