Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Filtered colimit elimination from Birkhoff's variety theorem

Yuto Kawase

TL;DR

The paper addresses the need to relax the filtered colimit closure in Birkhoff-type theorems for relative algebraic theories. It introduces an ascending chain condition on locally finitely presentable categories as a sufficient criterion to achieve filtered colimit elimination, proving an equivalence between definability by $\rho$-relative judgments and closure under products, $\mathbb{T}$-closed subobjects, and $U^{\rho}$-local retracts (and, with retracts replaced by local retracts, closure under filtered colimits). This yields an HSP-type formalization for $ ext{A}$-relative theories and generalizes Birkhoff-type results to finite-sorted and ordered algebraic settings. The work further develops the theory by analyzing strongly connected components, showing how ACC on finitely presentable components is nearly necessary for elimination, and provides detailed computations in locally connected categories and categories of group actions. Collectively, these results broaden the applicability of Birkhoff-type theorems in categorical algebra and logic, offering structural criteria to verify elimination and practical insights for specific categories such as presheaf categories and $G$-sets.

Abstract

Birkhoff's variety theorem, a fundamental theorem of universal algebra, asserts that a subclass of a given algebra is definable by equations if and only if it satisfies specific closure properties. In a generalized version of this theorem, closure under filtered colimits is required. However, in some special cases, such as finite-sorted equational theories and ordered algebraic theories, the theorem holds without assuming closure under filtered colimits. We call this phenomenon "filtered colimit elimination," and study a sufficient condition for it. We show that if a locally finitely presentable category $\mathscr{A}$ satisfies a noetherian-like condition, then filtered colimit elimination holds in the generalized Birkhoff's theorem for algebras relative to $\mathscr{A}$.

Filtered colimit elimination from Birkhoff's variety theorem

TL;DR

The paper addresses the need to relax the filtered colimit closure in Birkhoff-type theorems for relative algebraic theories. It introduces an ascending chain condition on locally finitely presentable categories as a sufficient criterion to achieve filtered colimit elimination, proving an equivalence between definability by -relative judgments and closure under products, -closed subobjects, and -local retracts (and, with retracts replaced by local retracts, closure under filtered colimits). This yields an HSP-type formalization for -relative theories and generalizes Birkhoff-type results to finite-sorted and ordered algebraic settings. The work further develops the theory by analyzing strongly connected components, showing how ACC on finitely presentable components is nearly necessary for elimination, and provides detailed computations in locally connected categories and categories of group actions. Collectively, these results broaden the applicability of Birkhoff-type theorems in categorical algebra and logic, offering structural criteria to verify elimination and practical insights for specific categories such as presheaf categories and -sets.

Abstract

Birkhoff's variety theorem, a fundamental theorem of universal algebra, asserts that a subclass of a given algebra is definable by equations if and only if it satisfies specific closure properties. In a generalized version of this theorem, closure under filtered colimits is required. However, in some special cases, such as finite-sorted equational theories and ordered algebraic theories, the theorem holds without assuming closure under filtered colimits. We call this phenomenon "filtered colimit elimination," and study a sufficient condition for it. We show that if a locally finitely presentable category satisfies a noetherian-like condition, then filtered colimit elimination holds in the generalized Birkhoff's theorem for algebras relative to .
Paper Structure (10 sections, 23 theorems, 28 equations, 1 table)

This paper contains 10 sections, 23 theorems, 28 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Partial Horn theories
  4. Relative algebraic theories
  5. Local retracts in locally finitely presentable categories
  6. The ascending chain condition for categories
  7. Filtered colimit elimination
  8. Computation of strongly connected components
  9. Locally connected categories
  10. Categories of group actions

Key Result

Theorem 1.1

Let $\rho\colon\mathbb{S}\to\mathbb{T}$ be a theory morphism between partial Horn theories. Assume that $\mathbb{S}\mathchar'-\mathrm{PMod}$ satisfies the ascending chain condition. Then, for every replete full subcategory $\mathscr{E}\subseteq\mathbb{T}\mathchar'-\mathrm{PMod}$, the following are e

Theorems & Definitions (88)

  • Theorem 1.1: Filtered colimit elimination
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Theorem 2.7
  • proof
  • Example 2.8: posets
  • Definition 2.9: kawase2023birkhoffs
  • ...and 78 more