nLab coherent 2-category

Redirected from "higher foundations".
Contents

Contents

Idea

The generalization of the notion of coherent category from category theory to 2-category theory.

Definition

Definition

A 2-category is called coherent if 1. it has finite 2-limits, 1. finite jointly-eso? families are stable under 2-pullback, and 1. every finitary 2-polycongruence? which is a kernel can be completed to an exact 2-polyfork?.

Here a family {f i:A iB}\{f_i:A_i \to B\} is said to be jointly-eso if whenever m:CBm:C\to B is ff and every f if_i factors through mm (up to isomorphism), then mm is an equivalence.

Likewise, we have infinitary coherent 2-categories in which “finite” in the second two conditions is replaced by “small.”

Examples

Properties

Factorizations

The following are proven just like their unary analogues in a regular 2-category.

Lemma

(Street’s Lemma) In a finitely complete 2-category where finite jointly-eso families are stable under pullback, if {e i:A iB}\{e_i:A_i \to B\} is finite and jointly-eso and n:BCn:B\to C is such that the induced functor ker(e i)ker(ne i)\ker(e_i) \to ker(n e_i) is an equivalence, then nn is ff.

Theorem

A 2-category is coherent if and only if 1. it has finite limits, 1. finite jointly-eso families are stable under pullback, 1. every finite family {f i}\{f_i\} factors as f i=me if_i = m e_i where mm is ff and {e i}\{e_i\} is jointly-eso, and 1. every jointly-eso family is the quotient of its kernel.

Of course, there are infinitary versions. In particular, we conclude that in a coherent (resp. infinitary-coherent) 2-category, the posets Sub(X)Sub(X) have finite (resp. small) unions that are preserved by pullback.

Colimits

Lemma

A coherent 2-category has a strict initial object; that is an initial object 00 such that any morphism X0X\to 0 is an equivalence.

Proof

The empty 2-congruence is the kernel of the empty family (over any object), so it must have a quotient 00, which is clearly an initial object. The empty family over 00 is jointly-eso, so for any X0X\to 0 the empty family over XX is also jointly-eso; but this clearly makes XX initial as well.

Two ffs m:AXm:A\to X and n:BXn:B\to X are said to be disjoint if the comma objects (m/n)(m/n) and (n/m)(n/m) are initial objects. If initial objects are strict, then this implies that the pullback A× XBA\times_X B is also initial, but it is strictly stronger already in PosPos.

Lemma

In a coherent 2-category, if AXA\to X and BXB\to X are disjoint subobjects, then their union ABA\cup B in Sub(X)Sub(X) is also their coproduct A+BA+B.

Proof

If AA and BB are disjoint subobjects of XX, then the kernel of {AX,BX}\{A\to X, B\to X\} is the disjoint union of ker(A)ker(A) and ker(B)ker(B). Therefore, a quotient of it (which is a union of AA and BB in Sub(X)Sub(X)) will be a coproduct of AA and BB.

A coproduct A+BA+B in a 2-category is disjoint if AA and BB are disjoint subobjects of A+BA+B. We say a coherent 2-category is positive if any two objects have a disjoint coproduct. By Lemma , this is equivalent to saying that any two objects can be embedded as disjoint subobjects of some other object. Disjoint coproducts in a coherent 2-category are automatically stable under pullback, so a positive coherent 2-category is necessarily extensive. Conversely, we have:

Lemma

A regular and extensive 2-category is coherent (and positive).

In the presence of finite coproducts, a family {e i:A iB}\{e_i:A_i\to B\} is jointly-eso iff iA iB\coprod_i A_i \to B is eso; thus regularity and universal coproducts imply that finite jointly-eso families are stable under pullback. And assuming extensivity, any 2-polycongruence {C ij}{C i}\{C_{i j}\} \rightrightarrows \{C_i\} gives rise to an ordinary 2-congruence ijC ij iC i\coprod_{i j} C_{i j} \rightrightarrows \coprod_i C_i. Likewise, 2-polyforks {C ij}{C i}X\{C_{i j}\} \rightrightarrows \{C_i\} \to X correspond to 2-forks ijC ij iC iX\coprod_{i j} C_{i j} \rightrightarrows \coprod_i C_i \to X, and the property of being a kernel or a quotient is preserved; thus regularity implies coherency.

Preservation

If KK is coherent, then easily so are K coK^{co}, disc(K)disc(K), gpd(K)gpd(K), pos(K)pos(K), and Sub(1)Sub(1). Moreover, we have:

Theorem

If KK is a coherent 2-category, so are the fibrational slices Opf(X)Opf(X) and Fib(X)Fib(X) for any XKX\in K.

References

This is due to

based on

Created on March 9, 2012 at 19:02:48. See the history of this page for a list of all contributions to it.