Exact completion

Last updated

In category theory, a branch of mathematics, the exact completion constructs a Barr-exact category from any finitely complete category. It is used to form the effective topos and other realizability toposes.

Contents

Construction

Let C be a category with finite limits. Then the exact completion of C (denoted Cex) has for its objects pseudo-equivalence relations in C. [1] A pseudo-equivalence relation is like an equivalence relation except that it need not be jointly monic. An object in Cex thus consists of two objects X0 and X1 and two parallel morphisms x0 and x1 from X1 to X0 such that there exist a reflexivity morphism r from X0 to X1 such that x0r = x1r = 1X0; a symmetry morphism s from X1 to itself such that x0s = x1 and x1s = x0; and a transitivity morphism t from X1 × x1, X0, x0X1 to X1 such that x0t = x0p and x1t = x1q, where p and q are the two projections of the aforementioned pullback. A morphism from (X0, X1, x0, x1) to (Y0, Y1, y0, y1) in Cex is given by an equivalence class of morphisms f0 from X0 to Y0 such that there exists a morphism f1 from X1 to Y1 such that y0f1 = f0x0 and y1f1 = f0x1, with two such morphisms f0 and g0 being equivalent if there exists a morphism e from X0 to Y1 such that y0e = f0 and y1e = g0.

Examples

Properties

Related Research Articles

<span class="mw-page-title-main">Category theory</span> General theory of mathematical structures

Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, category theory is used in almost all areas of mathematics, and in some areas of computer science. In particular, many constructions of new mathematical objects from previous ones, that appear similarly in several contexts are conveniently expressed and unified in terms of categories. Examples include quotient spaces, direct products, completion, and duality.

In mathematics, especially in category theory and homotopy theory, a groupoid generalises the notion of group in several equivalent ways. A groupoid can be seen as a:

<span class="mw-page-title-main">Universal property</span> Central object of study in category theory

In mathematics, more specifically in category theory, a universal property is a property that characterizes up to an isomorphism the result of some constructions. Thus, universal properties can be used for defining some objects independently from the method chosen for constructing them. For example, the definitions of the integers from the natural numbers, of the rational numbers from the integers, of the real numbers from the rational numbers, and of polynomial rings from the field of their coefficients can all be done in terms of universal properties. In particular, the concept of universal property allows a simple proof that all constructions of real numbers are equivalent: it suffices to prove that they satisfy the same universal property.

<span class="mw-page-title-main">Category (mathematics)</span> Mathematical object that generalizes the standard notions of sets and functions

In mathematics, a category is a collection of "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose objects are sets and whose arrows are functions.

In category theory, an epimorphism is a morphism f : XY that is right-cancellative in the sense that, for all objects Z and all morphisms g1, g2: YZ,

In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.

In mathematics, a Heyting algebra is a bounded lattice equipped with a binary operation ab of implication such that ≤ b is equivalent to c ≤. From a logical standpoint, AB is by this definition the weakest proposition for which modus ponens, the inference rule AB, AB, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

In category theory, a branch of abstract mathematics, an equivalence of categories is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics. Establishing an equivalence involves demonstrating strong similarities between the mathematical structures concerned. In some cases, these structures may appear to be unrelated at a superficial or intuitive level, making the notion fairly powerful: it creates the opportunity to "translate" theorems between different kinds of mathematical structures, knowing that the essential meaning of those theorems is preserved under the translation.

In algebraic geometry, motives is a theory proposed by Alexander Grothendieck in the 1960s to unify the vast array of similarly behaved cohomology theories such as singular cohomology, de Rham cohomology, etale cohomology, and crystalline cohomology. Philosophically, a "motif" is the "cohomology essence" of a variety.

In category theory, a branch of mathematics, a pullback is the limit of a diagram consisting of two morphisms f : X → Z and g : Y → Z with a common codomain. The pullback is often written

Fibred categories are abstract entities in mathematics used to provide a general framework for descent theory. They formalise the various situations in geometry and algebra in which inverse images of objects such as vector bundles can be defined. As an example, for each topological space there is the category of vector bundles on the space, and for every continuous map from a topological space X to another topological space Y is associated the pullback functor taking bundles on Y to bundles on X. Fibred categories formalise the system consisting of these categories and inverse image functors. Similar setups appear in various guises in mathematics, in particular in algebraic geometry, which is the context in which fibred categories originally appeared. Fibered categories are used to define stacks, which are fibered categories with "descent". Fibrations also play an important role in categorical semantics of type theory, and in particular that of dependent type theories.

This is a glossary of properties and concepts in category theory in mathematics.

In mathematics, a category is distributive if it has finite products and finite coproducts and such that for every choice of objects , the canonical map

In category theory, a regular category is a category with finite limits and coequalizers of a pair of morphisms called kernel pairs, satisfying certain exactness conditions. In that way, regular categories recapture many properties of abelian categories, like the existence of images, without requiring additivity. At the same time, regular categories provide a foundation for the study of a fragment of first-order logic, known as regular logic.

In the mathematical field of category theory, an allegory is a category that has some of the structure of the category Rel of sets and binary relations between them. Allegories can be used as an abstraction of categories of relations, and in this sense the theory of allegories is a generalization of relation algebra to relations between different sorts. Allegories are also useful in defining and investigating certain constructions in category theory, such as exact completions.

In mathematics, a topos is a category that behaves like the category of sheaves of sets on a topological space. Topoi behave much like the category of sets and possess a notion of localization; they are a direct generalization of point-set topology. The Grothendieck topoi find applications in algebraic geometry; the more general elementary topoi are used in logic.

In mathematics, more specifically category theory, a quasi-category is a generalization of the notion of a category. The study of such generalizations is known as higher category theory.

In the mathematical discipline of category theory, a strict initial object is an initial object 0 of a category C with the property that every morphism in C with codomain 0 is an isomorphism. In a Cartesian closed category, every initial object is strict. Also, if C is a distributive or extensive category, then the initial object 0 of C is strict.

In mathematics, an extensive category is a category C with finite coproducts that are disjoint and well-behaved with respect to pullbacks. Equivalently, C is extensive if the coproduct functor from the product of the slice categories C/X × C/Y to the slice category C/(X + Y) is an equivalence of categories for all objects X and Y of C.

In mathematics, the ind-completion or ind-construction is the process of freely adding filtered colimits to a given category C. The objects in this ind-completed category, denoted Ind(C), are known as direct systems, they are functors from a small filtered category I to C.

References

  1. Menni, Matias (2000). "Exact completion and toposes" (PDF). Retrieved 18 September 2016.
  2. 1 2 Carboni, A. (15 September 1995). "Some free constructions in realizability and proof theory". Journal of Pure and Applied Algebra . 103 (2): 117–148. doi: 10.1016/0022-4049(94)00103-p .
  3. Carboni, A.; Magno, R. Celia (December 1982). "The free exact category on a left exact one". Journal of the Australian Mathematical Society . 33 (3): 295–301. doi: 10.1017/s1446788700018735 .
  4. Carboni, A.; Rosolini, G. (1 December 2000). "Locally cartesian closed exact completions". Journal of Pure and Applied Algebra . 154 (1–3): 103–116. doi: 10.1016/s0022-4049(99)00192-9 .