2
$\begingroup$

Let $P: \mathcal{C}\to\mathcal{S}$ a fibration ($\mathcal{S}$ with finite limits).

In "Sketches of an Elephant I", pag. 272 P. Johnstone define $P$ a locally small if:

given any two objects $X, Y\in \mathcal{C}$ (let $A=P(X),\ B=P(Y)$) there exist a arrow $(a, b): I\to A\times B$ and a morphisms $f: a^\ast X\to b^\ast Y$ in the fibre $\mathcal{C}(I)$ such that given any $(c, d): J\to A\times B$ and any $g: c^\ast X\to d^\ast Y $ in $\mathcal{C}(J)$ there exists a unique $u: J\to I$ such that $a\circ u=c,\ b\circ u=d$ and $u^\ast(f)\ \dot{=}\ g$ (where " $\dot{=}$ " means up to canonical isomorphisms).

In LNM 661 "Indexed Categories and its Applications" p. 40, the authors post the J. Benabou definition: $P$ is a locally small if:

for any $I\in\mathcal{S}$ and every $X, Y\in \mathcal{C}(I)$ there exist a morfisms ${}^Ih_{A, B}: {}^IH_{A, B} \to I$ such that for any $\alpha: J\to I$ there is a bijection between the morphisms:

$\alpha \to {}^Ih_{A, B}$ in $\mathcal{S}\downarrow I$

and the morphisms $\alpha^\ast(X)\to \alpha^\ast(Y)$ in $\mathcal{C}(I)$

I ask: how are related (if they are) these two definitions?

Edit:

Johnston define "locally small" as the (what he define) comprehension scheme for the inclusion $2\to \underline{2}$

($2$ is the discrte category $\{0, 1}$ and $\underline{2}$ is $0\to 1$ plus identities).

THis means that the composition funtor $Rect(\underline{2},\ \mathcal{C} )\to Rect(2,\ \mathcal{C} )$ has a right adjoint, where $Rect(\mathcal{D},\ \mathcal{C} )$ is the category with objects the diagrams $d: \mathcal{D}\to \mathcal{C}$ with vertical edges (i.e. mapped to identities by $P$), and with morphisms the transformations with all components cartesians. (articulating this, get the definition given at the beginning).

THe BEnabou definition is equivalent to the more strict assert:

the composition funtor $Rect_P(\underline{2},\ \mathcal{C} )\to Rect_P(2,\ \mathcal{C} )$ has a right adjoint, where $Rect_P(\mathcal{D},\ \mathcal{C} )\subset Rect(\mathcal{D},\ \mathcal{C} )$ is given by diagram $d: \mathcal{D}\to \mathcal{C}$ with $P\circ d$ constant (i.e. maps all on some object $A$ and its identity $1_A$) and with morphisms the transformations with all components cartesians and mapped by $P$ on the same morphism.

THen the Johnstone definition imply the BEnabou one: by restriction of adjunction, observing that $2$ is just the objects of $\underline{2}$ then the condiction on transformations components is preserved.

From the CHuck answere, the reverse i true too:

LEt $X, Y\in \mathcal{C}$ and let $A=P(X),\ B=P(Y)$, considering $\pi_A: A\times B\to A,\ \pi_B : A\times B\to B$, put $I:=A\times B$ and considering $\pi_A^\ast(X),\ \pi_B^\ast(Y)$ on the $I$-fibre, appling the BEnabou condiction follow the Johnstone one.

Then the initial request has the follow generalization:

given a functor $F: \mathcal{D'}\to \mathcal{D} $

Is true that:

If the natural funtor

$Rect(\mathcal{D},\ \mathcal{C} )\to Rect(\mathcal{D'},\ \mathcal{C} )$ has a right adjoint

then

$Rect_P(\mathcal{D},\ \mathcal{C} )\to Rect_P(\mathcal{D'},\ \mathcal{C} )$ has a right adjoint ?

(from above, I seem the if $F$ is surjective on objets then the proposition is true)

Is true the reverse?, with such conditions on $F$ the reverse can be true?

$\endgroup$
4
  • $\begingroup$ I'm fairly sure they're equivalent. See Theorem 10.1 in Streicher's notes, or Theorem B2.2.2 in the Elephant. $\endgroup$
    – Zhen Lin
    Aug 19, 2012 at 13:19
  • $\begingroup$ THe definition in Streicher notes is equivalent to above BEanbou definition (see also "Categoriacal Logic and Type theory" B. JAcobs, Lemma 9.5.4, pag. 561) $\endgroup$ Aug 19, 2012 at 14:36
  • $\begingroup$ I may be misunderstanding your notation here, but your definition of $Rect_P$ seems to me to be the same as $Rect$ since all diagrams in $Rect$ already lie in only one fiber and have only vertical edges and hence applying $P$ to them will 'crush' them to the same object and its identity. $\endgroup$
    – Chuck
    Aug 19, 2012 at 19:18
  • $\begingroup$ on a non cennected cathegory as $2$, $Rect$ can send $0$ and $1$ on differents fibre, or also if send them on the some fibre, the 2 components of a transformations can have different priections on the base category. Anyway I seems that the above generalization is true if $\mathcal{D'}\subset \mathcal{D}$ and $\mathcal{D'}$ has finite connect components. $\endgroup$ Aug 19, 2012 at 22:04

1 Answer 1

6
$\begingroup$

The definitions are indeed equivalent. The idea of 'local smallness' is to get for any $X$,$Y$ in $\mathcal{C}^I$ an object of your indexing category to represent, as it were, all (vertical) morphisms between $X$ and $Y$. Both definitions describe this fact, although Johnstone's is, I guess, slightly more 'general' than it needs to be in that it applies the above property to any $X$ and $Y$ in $\mathcal{C}$ (and not to $X$, $Y$ in the same fibre), but that's OK by Theorem 10.1 in Streicher since $\mathcal{S}$ has finite limits. The equivalence of the definitions can also be proved as exercises 8.8.9 and 8.8.10 in Volume 2 of Borceaux.

To see that they are equivalent let for simplicity $X$ and $Y$ lie on the same fibre $I$ (WLOG bearing in mind what I said above.) Then Johnstone's definition says that there exists an arrow $\alpha \colon J \rightarrow I$ and a morphism $f \colon \alpha^*X \rightarrow \alpha^*Y$ such that for any $\beta \colon K \rightarrow I$ and any morphism $g \colon \beta^*X \rightarrow \beta^*Y$ there exists a unique $u: K \rightarrow J$ such that

$$u^{*}(f) = g$$

and $\alpha \circ u = \beta$. But now if you write $J$ as $H_{X,Y}$ and $\alpha$ as $h_{X,Y}$ you'll see that the last sentence says exactly that there is a bijection between morphisms $f \colon \beta^*X \rightarrow \beta^*Y$ and morphisms $u$ such that $h_{X,Y} \circ u = \beta$, i.e. between morphisms from $\beta$ to $h_{X,Y}$ in $\mathcal{S}/I$. And this is exactly the second definition.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.