Skip to main content
added 108 characters in body
Source Link
varkor
  • 10.6k
  • 29
  • 71

Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a finitely complete category $\mathscr C[x \to y]$ together with a finitely continuous functor $I \colon \mathscr C \to \mathscr C[x \to y]$ and a distinguished morphism $I x \to I y$ such that, for every finitely continuous functor $F \colon \mathscr C \to \mathscr D$ where $\mathscr D$ is finitely complete and has a distinguished morphism $Fx \to Fy$, there is an essentially unique finitely continuous functor $\mathscr C[x \to y] \to \mathscr D$ making the evident triangle commute up to isomorphism and preserving the distinguished morphism.

Abstractly, $\mathscr C[x \to y]$ is the coinserter in $\mathbf{Lex}$, the 2-category of finitely complete categories, of the two functors $1 \to \mathscr C$ selecting $x$ and $y$ respectively.

When $x = 1$, there is an elegant construction of $\mathscr C[1 \to y]$: it is, up to equivalence, the slice category $\mathscr C/y$. (This can be found, for instance, as Proposition 1.10.15(ii) of Jacobs's Categorical Logic and Type Theory.)

Does a similar explicit categorical construction of $\mathscr C[x \to y]$ exist, for arbitrary $x$ and $y$?

The meaning of "explicit categorical construction" is left somewhat up to interpretation. In the case of $x = 1$By "explicit", we can give a construction in termsI want to avoid descriptions, for instance, that involve some tautological description of a 2-categorical limitcolimits; by "categorical", and which is certainly an explicit categorical construction. HoweverI want to avoid descriptions, for instance, I don't view a construction usingthat make use of the internal language of a finitely complete category to qualify as. In contrast, the slice category construction is both explicit (we have a direct description of its objects and morphisms) and categorical construction(it is a 2-limit).

Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a finitely complete category $\mathscr C[x \to y]$ together with a finitely continuous functor $I \colon \mathscr C \to \mathscr C[x \to y]$ and a distinguished morphism $I x \to I y$ such that, for every finitely continuous functor $F \colon \mathscr C \to \mathscr D$ where $\mathscr D$ is finitely complete and has a distinguished morphism $Fx \to Fy$, there is an essentially unique finitely continuous functor $\mathscr C[x \to y] \to \mathscr D$ making the evident triangle commute up to isomorphism and preserving the distinguished morphism.

Abstractly, $\mathscr C[x \to y]$ is the coinserter in $\mathbf{Lex}$, the 2-category of finitely complete categories, of the two functors $1 \to \mathscr C$ selecting $x$ and $y$ respectively.

When $x = 1$, there is an elegant construction of $\mathscr C[1 \to y]$: it is, up to equivalence, the slice category $\mathscr C/y$. (This can be found, for instance, as Proposition 1.10.15(ii) of Jacobs's Categorical Logic and Type Theory.)

Does a similar explicit categorical construction of $\mathscr C[x \to y]$ exist, for arbitrary $x$ and $y$?

The meaning of "explicit categorical construction" is left somewhat up to interpretation. In the case of $x = 1$, we can give a construction in terms of a 2-categorical limit, and which is certainly an explicit categorical construction. However, for instance, I don't view a construction using the internal language of a finitely complete category to qualify as a categorical construction.

Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a finitely complete category $\mathscr C[x \to y]$ together with a finitely continuous functor $I \colon \mathscr C \to \mathscr C[x \to y]$ and a distinguished morphism $I x \to I y$ such that, for every finitely continuous functor $F \colon \mathscr C \to \mathscr D$ where $\mathscr D$ is finitely complete and has a distinguished morphism $Fx \to Fy$, there is an essentially unique finitely continuous functor $\mathscr C[x \to y] \to \mathscr D$ making the evident triangle commute up to isomorphism and preserving the distinguished morphism.

Abstractly, $\mathscr C[x \to y]$ is the coinserter in $\mathbf{Lex}$, the 2-category of finitely complete categories, of the two functors $1 \to \mathscr C$ selecting $x$ and $y$ respectively.

When $x = 1$, there is an elegant construction of $\mathscr C[1 \to y]$: it is, up to equivalence, the slice category $\mathscr C/y$. (This can be found, for instance, as Proposition 1.10.15(ii) of Jacobs's Categorical Logic and Type Theory.)

Does a similar explicit categorical construction of $\mathscr C[x \to y]$ exist, for arbitrary $x$ and $y$?

The meaning of "explicit categorical construction" is left somewhat up to interpretation. By "explicit", I want to avoid descriptions, for instance, that involve some tautological description of 2-colimits; by "categorical", I want to avoid descriptions, for instance, that make use of the internal language of a finitely complete category. In contrast, the slice category construction is both explicit (we have a direct description of its objects and morphisms) and categorical (it is a 2-limit).

Source Link
varkor
  • 10.6k
  • 29
  • 71

Adjoining a morphism to a finitely complete category

Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a finitely complete category $\mathscr C[x \to y]$ together with a finitely continuous functor $I \colon \mathscr C \to \mathscr C[x \to y]$ and a distinguished morphism $I x \to I y$ such that, for every finitely continuous functor $F \colon \mathscr C \to \mathscr D$ where $\mathscr D$ is finitely complete and has a distinguished morphism $Fx \to Fy$, there is an essentially unique finitely continuous functor $\mathscr C[x \to y] \to \mathscr D$ making the evident triangle commute up to isomorphism and preserving the distinguished morphism.

Abstractly, $\mathscr C[x \to y]$ is the coinserter in $\mathbf{Lex}$, the 2-category of finitely complete categories, of the two functors $1 \to \mathscr C$ selecting $x$ and $y$ respectively.

When $x = 1$, there is an elegant construction of $\mathscr C[1 \to y]$: it is, up to equivalence, the slice category $\mathscr C/y$. (This can be found, for instance, as Proposition 1.10.15(ii) of Jacobs's Categorical Logic and Type Theory.)

Does a similar explicit categorical construction of $\mathscr C[x \to y]$ exist, for arbitrary $x$ and $y$?

The meaning of "explicit categorical construction" is left somewhat up to interpretation. In the case of $x = 1$, we can give a construction in terms of a 2-categorical limit, and which is certainly an explicit categorical construction. However, for instance, I don't view a construction using the internal language of a finitely complete category to qualify as a categorical construction.