Exact completion
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.
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, x0 X1 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
- If the axiom of choice holds, then Setex is equivalent to Set.
- More generally, let C be a small category with finite limits. Then the category of presheaves SetCop is equivalent to the exact completion of the coproduct completion of C.[2]
- The effective topos is the exact completion of the category of assemblies.[2]
Properties
- If C is an additive category, then Cex is an abelian category.[3]
- If C is cartesian closed or locally cartesian closed, then so is Cex.[4]
References
- ↑ Menni, Matias (2000). "Exact completion and toposes". http://www.lfcs.inf.ed.ac.uk/reports/00/ECS-LFCS-00-424/ECS-LFCS-00-424.pdf.
- ↑ 2.0 2.1 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.
- ↑ 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.
- ↑ 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.
External links
 |  |
