nLab enhanced 2-category

Redirected from "F-category".

Idea

An enhanced 2-category (or \mathcal{F}-category) is like a 2-category, but with two types of 1-morphisms, one of which we think of as “stricter” than the other. The stricter morphisms are called tight and the less strict ones are called loose.

Definition

Strict \mathcal{F}-categories

Let \mathcal{F} denote the category whose objects are functors that are fully faithful and injective on objects, and whose morphisms are commutative squares (a full subcategory of the arrow category of Cat). We call the objects of \mathcal{F}, for the nonce, full embeddings. Then \mathcal{F} is cartesian closed, complete and cocomplete, hence a Benabou cosmos.

A strict \mathcal{F}-category is a category enriched over \mathcal{F}. Therefore, between every two objects, an \mathcal{F}-category KK has an object K(x,y)K(x,y)\in \mathcal{F}, hence a full embedding K(x,y) τK(x,y) λK(x,y)_\tau \to K(x,y)_\lambda. The objects of K(x,y) τK(x,y)_\tau are called tight morphisms xyx\to y, and the objects of K(x,y) λK(x,y)_\lambda are called loose morphisms xyx\rightsquigarrow y.

Since full embeddings are injective on objects, “being tight” is a property of a loose morphism. (This would still be true in the “up to unique isomorphism” sense even if we did not ask for injectivity on objects, but when dealing with strict things, it is easier to keep them as strict as possible.) And since full embeddings are fully faithful, the 2-cells between two tight morphisms are the same whether we regard them as tight or as loose.

For any \mathcal{F}-category KK, the objects, tight morphisms, and 2-cells form a strict 2-category K τK_\tau, and the objects, loose morphisms, and 2-cells form a strict 2-category K λK_\lambda. There is an obvious strict 2-functor

K τK λK_\tau \to K_\lambda

which is the identity on objects, strictly faithful on 1-morphisms, and locally fully faithful. Since KK can be recovered from this 2-functor, an equivalent definition of a strict \mathcal{F}-category is as a strict 2-functor with these properties.

Strict \mathcal{F}-categories are equivalent to strict double categories with a functorial choice of companions, and for which the assignment of tight morphisms to loose morphisms is injective.

Weak \mathcal{F}-categories

Probably the best “fully weak” version of \mathcal{F}-categories is obtained by redefining \mathcal{F} to consist of fully faithful functors, with squares that commute up to specified isomorphism, and then by considering \mathcal{F}-enriched bicategories rather than enriched categories. Such a thing would be equivalent to an identity-on-objects and locally-fully-faithful pseudofunctor between bicategories.

One could consider semi-strict versions as well, in which (for example) the tight morphisms form a strict 2-category.

Examples

  • Any proarrow equipment is an \mathcal{F}-category (perhaps weak, perhaps semi-strict).

  • An example of a semi-strict \mathcal{F}-category is the localization 2-functor Cat(S)Cat(S)[W 1]Cat(S) \to Cat(S)[W^{-1}] for a class of weak equivalences WW.

  • For any (strict) 2-monad TT, there are strict \mathcal{F}-categories of TT-algebras whose tight and loose morphisms are, respectively:

    1. strict and pseudo TT-morphisms
    2. strict and lax TT-morphisms
    3. strict and colax TT-morphisms
    4. pseudo and lax TT-morphisms
    5. pseudo and colax TT-morphisms

    In fact, this can be generalized to any \mathcal{F}-monad on an \mathcal{F}-category.

  • Any 2-category gives rise to two \mathcal{F}-categories:

    • In a chordate \mathcal{F}-category, all morphisms are tight.
    • In an inchordate \mathcal{F}-category, only identities are tight.
  • The lax slice 2-category is an \mathcal{F}-category whose tight 2-category is the (pseudo) slice 2-category. This \mathcal{F}-category allows a definition of fibrations using lax F-adjunctions.

  • \mathcal{F} itself becomes an \mathcal{F}-category in the usual way. Its tight morphisms are just the morphisms in the underlying ordinary category \mathcal{F}, while its loose morphisms are simply functors between the loose parts (the codomains of the full embeddings).

\mathcal{F}-weighted limits

The general machinery of enriched category theory applied to \mathcal{F} gives us a notion of weighted limit. Note first that an \mathcal{F}-enriched diagram in an \mathcal{F}-category is a diagram of morphisms in which some are required to be tight, and others are not (but could “accidentally” be tight).

In general, a weighted limit of such a diagram in a (strict) \mathcal{F}-category is a weighted (strict) 2-limit in its 2-category of loose morphisms, with the property that certain specified projections from the limit object are tight and “jointly detect tightness”, in the sense that a morphism into the limit is tight if and only if its composites with all of the specified projections are tight. Details and examples can be found in (LS).

One of the most important things about \mathcal{F}-categories is that they allow us to define the classes of rigged limits, which are the \mathcal{F}-weighted limits that are created by the forgetful functors from the various \mathcal{F}-categories of algebras and strict/pseudo/lax/colax morphisms over a 2-monad (or an \mathcal{F}-monad).

Properties of \mathcal{F}

As mentioned above, the base of enrichment \mathcal{F} is well behaved. For instance, it is cartesian closed and locally finitely presentable (hence complete and cocomplete). Cartesian closure is proven in Lack and Shulman; we establish local finite presentability below.

Proposition

\mathcal{F} is locally finitely presentable.

Proof

Since ℂ𝔸𝕋 \mathbb{CAT}^\to is locally finitely presentable, to show that \mathcal{F} is locally finitely presentable, it suffices by Theorem 1.39 of Locally Presentable and Accessible Categories to show that \mathcal{F} is a finite orthogonality class in ℂ𝔸𝕋 \mathbb{CAT}^\to. First, note that, for any category \mathbb{C}, a morphism m:XYm \colon X \to Y is orthogonal in \mathbb{C} to a morphism e:ABe \colon A \to B if and only if mm is orthogonal, as an object in \mathbb{C}^\to, to the following square. It remains to observe that injectivity-on-objects and full faithfulness are both properties of functors captured by orthogonality in ℂ𝔸𝕋\mathbb{CAT}. - A functor is injective-on-objects if and only if it is orthogonal to the unique functor {**}{*}\{ * \quad *' \} \to \{ * \}. - A functor is fully faithful if and only if it is orthogonal to the unique identity-on-objects functor {**}{**}\{ * \quad *' \} \to \{ * \to *' \}.

The 1-category-theoretic version:

References

\mathcal{F}-categories were introduced in the following, where they were called enhanced 2-categories:

Last revised on November 16, 2024 at 10:53:18. See the history of this page for a list of all contributions to it.