Redirected from "adjoint quadruples".
Contents
Contents
Definition
An adjoint quadruple is a sequence of three adjunctions
f ! ⊣ f * ⊣ f * ⊣ f !
f_! \dashv f^* \dashv f_* \dashv f^!
between a quadruple of morphisms . That is, it is an adjoint string of length 4.
Properties
General
Every adjoint quadruple
( f ! ⊣ f * ⊣ f * ⊣ f ! ) : C ← f ! → f * ← f * → f ! D
(f_! \dashv f^* \dashv f_* \dashv f^!)
:
C
\stackrel{\overset{f_!}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\stackrel{\overset{f_*}{\to}}{\underset{f^!}{\leftarrow}}}}
D
induces an adjoint triple on C C
( f * f ! ⊣ f * f * ⊣ f ! f * ) : C → C ,
(f^* f_! \dashv f^* f_* \dashv f^! f_*)
:
C \to C
\,,
(hence a monad left adjoint to a comonad left adjoint to a monad) and an adjoint triple
( f ! f * ⊣ f * f * ⊣ f * f ! ) : D → D
(f_! f^* \dashv f_* f^* \dashv f_* f^!) : D \to D
on D D .
Since moreover every adjoint triple ( F ⊣ G ⊣ H ) (F \dashv G \dashv H) induces an adjoint pair ( G F ⊣ G H ) (G F \dashv G H) and an adjoint pair ( F G ⊣ H G ) (F G \dashv H G) , the adjoint quadruple above induces four adjoint pairs, such as
( f * f * f * f ! ⊣ f * f * f ! f * ) : C → C .
(f^* f_* f^* f_! \dashv f^* f_* f^! f_*) : C \to C
\,.
\,
Let
( p ! ⊣ p * ⊣ p * ⊣ p ! ) : ℰ ⟶ 𝒮
(p_! \dashv p^* \dashv p_*\dashv p^!)
\;\colon\;
\mathcal{E}
\longrightarrow
\mathcal{S}
be an adjoint quadruple of adjoint functors such that p * p^* and p ! p^! are full and faithful functors . We record some general properties of such a setup.
We write
η : id → p * p !
\eta \;\colon\; id \to p^* p_!
etc. for units and
ϵ : p ! p * → id
\epsilon \;\colon\; p_! p^* \to id
etc. for counits.
Proposition/Definition
We have commuting diagrams , natural in X ∈ ℰ X \in \mathcal{E} , S ∈ 𝒮 S \in \mathcal{S}
p * X ⟶ ≃ ϵ p * X − 1 p ! p * p * X p * ( η X ) ↓ ↘ θ X ↓ p ! ( ϵ X ) p * p * p ! X ⟶ η p ! X − 1 p ! X
\array{
p_*X &\underoverset{\simeq}{\epsilon_{p^* X}^{-1}}{\longrightarrow}& p_! p^* p_*X
\\
{}^{\mathllap{p_*(\eta_X)}}\downarrow
&\searrow^{\mathrlap{\theta_X}}&
\downarrow^{\mathrlap{p_!(\epsilon_X)}}
\\
p_* p^* p_! X &\stackrel{\eta_{p_!X}^{-1}}{\longrightarrow}& p_! X
}
and
p * S ⟶ η p * S p ! p * p * S p * ϵ S − 1 ↓ ↘ ϕ X ↓ p ! ( η S − 1 ) p * p * p ! S ⟶ ϵ p ! S p ! S .
\array{
p^* S &\stackrel{\eta_{p^* S}}{\longrightarrow}& p^! p_* p^* S
\\
{}^{\mathllap{p^* \epsilon_S^{-1}}}\downarrow
&\searrow^{\mathrlap{\phi_X}}& \downarrow^{\mathrlap{p^!(\eta_S^{-1})}}
\\
p^* p_* p^!S &\stackrel{{\epsilon}_{p_!S }}{\longrightarrow}& p^!S
}
\,.
where the diagonal morphisms
θ X : p * X → p ! X
\theta_X : p_* X \to p_! X
and
ϕ S : p * S → p ! S
\phi_S : p^* S \to p^! S
are defined to be the equal composites of the sides of these diagrams.
This appears as (Johnstone 11, lemma 2.1, corollary 2.2 ).
Proposition
The following conditions are equivalent:
for all X ∈ ℰ X \in \mathcal{E} the morphism θ X : p * X → p ! X \theta_X : p_*X \to p_! X is an epimorphism ;
for all S ∈ 𝒮 S \in \mathcal{S} ,, the morphism ϕ S : p * S → p ! S \phi_S : p^*S \to p^! S is a monomorphism ;
p * p_* is faithful on morphisms of the form A → p * S A \to p^* S .
This appears as (Johnstone 11, lemma 2.3 ).
Proof
By the above definition, ϕ S \phi_S is a monomorphism precisely if η p * S : p * S → p ! p * p * S \eta_{p^* S} : p^* S \to p^! p_* p^* S is. This in turn is so (see monomorphism ) precisely if the first function in
ℰ ( A , p * X ) ⟶ ( η p * X ) ∘ ( − ) ℰ ( A , p ! p * p * S ) ⟶ ≃ 𝒮 ( p * A , p * p * S )
\mathcal{E}(A,p^* X)
\stackrel{(\eta_{p^* X}) \circ (-)}{\longrightarrow}
\mathcal{E}(A, p^! p_* p^* S)
\stackrel{\simeq}{\longrightarrow}
\mathcal{S}(p_* A, p_* p^* S)
and hence the composite is a monomorphism in Set .
By definition of adjunct and using the ( p * ⊣ p ! ) (p_* \dashv p^!) -zig-zag identity , this is equal to the action of p * p_* on morphisms
( η p * X ) ∘ ( − ) : ( A → p * S ) ↦ p * ( A → p * S ) .
(\eta_{p^* X}) \circ (-) :
(A \to p^* S) \mapsto p_*(A \to p^* S)
\,.
Similarly, by the above definition the morphism θ X \theta_X is an epimorphism precisely if p ! ( ϵ X ) : p ! p * p * X → p ! X p_!(\epsilon_X) : p_! p^* p_* X \to p_! X is so, which is the case precisely if the top morphism in
𝒮 ( p ! X , S ) ⟶ ( − ) ∘ p ! ( ϵ X ) 𝒮 ( p ! p * p * X , S ) ≃ ↓ ↓ ≃ ℰ ( p * p * X , p * S ) ≃ ↓ ↓ ≃ ℰ ( X , p * S ) ⟶ p * 𝒮 ( p * X , p * p * S )
\array{
\mathcal{S}(p_! X, S)
&\stackrel{(-) \circ p_!(\epsilon_X)}{\longrightarrow} &
\mathcal{S}(p_! p^* p_* X, S)
\\
{}^{\mathllap{\simeq}}\downarrow && \downarrow^{\mathrlap{\simeq}}
\\
&& \mathcal{E}(p^* p_* X, p^* S)
\\
{}^{\mathllap{\simeq}}\downarrow && \downarrow^{\mathrlap{\simeq}}
\\
\mathcal{E}(X, p^* S) &\stackrel{p_*}{\longrightarrow}& \mathcal{S}(p_* X, p_* p^* S)
}
and hence the bottom morphism is a monomorphism in Set , where again the commutativity of this diagram follows from the definition of adjunct and the ( p ! ⊣ p * ) (p_! \dashv p^*) -zig-zag identity .
\,
Examples
Via Kan extension of adjoint pairs
A rich source of adjoint quadruples arises form adjoint pairs between small categories by left/right Kan extension to their categories of presheaves .
More interesting examples of adjoint quadruples tend to arise from these presheaf constructions when the quadruple (co )restricts to sub-categories of sheaves .
We spell out two proofs of this fact, the first using coend -calculus in the generality of enriched category theory , the second using more elementary colimit -notation.
Proposition
(Kan extension of adjoint pair is adjoint quadruple ) For 𝒱 \mathcal{V} a symmetric closed monoidal category with all limits and colimits , let 𝒞 \mathcal{C} , 𝒟 \mathcal{D} be two small 𝒱 \mathcal{V} -enriched categories and let
𝒞 ⊥ ⟶ p ⟵ q 𝒟
\mathcal{C}
\underoverset
{\underset{p}{\longrightarrow}}
{\overset{q}{\longleftarrow}}
{\bot}
\mathcal{D}
be a 𝒱 \mathcal{V} -enriched adjunction . Then there are 𝒱 \mathcal{V} -enriched natural isomorphisms
( q op ) * ≃ Lan p op : [ 𝒞 op , 𝒱 ] ⟶ [ 𝒟 op , 𝒱 ]
(q^{op})^\ast \;\simeq\; Lan_{p^{op}}
\;\colon\;
[\mathcal{C}^{op},\mathcal{V}]
\longrightarrow
[\mathcal{D}^{op},\mathcal{V}]
( p op ) * ≃ Ran q op : [ 𝒟 op , 𝒱 ] ⟶ [ 𝒞 op , 𝒱 ]
(p^{op})^\ast \;\simeq\; Ran_{q^{op}}
\;\colon\;
[\mathcal{D}^{op},\mathcal{V}]
\longrightarrow
[\mathcal{C}^{op},\mathcal{V}]
between the precomposition on enriched presheaves with one functor and the left/right Kan extension of the other.
By essential uniqueness of adjoint functors (this Prop. ), this means that the two Kan extension adjoint triples of q q and p p
Lan q op ⊣ ( q op ) * ⊣ Ran q op Lan p op ⊣ ( p op ) * ⊣ Ran p op
\array{
Lan_{q^{op}} &\dashv& (q^{op})^\ast &\dashv& Ran_{q^{op}}
\\
&& Lan_{p^{op}} &\dashv& (p^{op})^\ast &\dashv& Ran_{p^{op}}
}
merge into an adjoint quadruple
Lan q op ⊣ ( q op ) * ⊣ ( p op ) * ⊣ Ran p op : [ 𝒞 op , 𝒱 ] ↔ [ 𝒟 op , 𝒱 ]
\array{
Lan_{q^{op}} &\dashv& (q^{op})^\ast &\dashv& (p^{op})^\ast &\dashv& Ran_{p^{op}}
}
\;\colon\;
[\mathcal{C}^{op},\mathcal{V}]
\leftrightarrow
[\mathcal{D}^{op}, \mathcal{V}]
Proof
For every enriched presheaf F : 𝒞 op → 𝒱 F \;\colon\; \mathcal{C}^{op} \to \mathcal{V} we have a sequence of 𝒱 \mathcal{V} -enriched natural isomorphism as follows
( Lan p op F ) ( d ) ≃ ∫ c ∈ 𝒞 𝒟 ( d , p ( c ) ) ⊗ F ( c ) ≃ ∫ c ∈ 𝒞 𝒞 ( q ( d ) , c ) ⊗ F ( c ) ≃ F ( q ( d ) ) = ( ( q op ) * F ) ( d ) .
\begin{aligned}
(Lan_{p^{op}} F)(d)
& \simeq
\int^{ c \in \mathcal{C} } \mathcal{D}(d,p(c)) \otimes F(c)
\\
& \simeq
\int^{ c \in \mathcal{C} } \mathcal{C}(q(d),c) \otimes F(c)
\\
& \simeq
F(q(d))
\\
& = \left( (q^{op})^\ast F\right) (d)
\,.
\end{aligned}
Here the first step is the coend -formula for left Kan extension (here ), the second step is the enriched adjunction -isomorphism for q ⊣ p q \dashv p and the third step is the co-Yoneda lemma .
This shows the first statement. By essential uniqueness of adjoints (this Prop. ), the other statements follow.
The following is the same argument without using coend-calculus. This argument applies verbatim also, for instance, in
∞
\infty
-category theory using results from standard sources:
Proof
We already know that each functor f f by itself induces an adjoint triple f ! ⊣ f * ⊣ f * f_! \dashv f^\ast \dashv f_\ast , by Kan extension . Due to essential uniqueness of adjoints (this Prop. ) it is hence sufficient to show that these two adjoint triples “overlap”, in that (ℓ * ≃ r ! \ell^\ast \simeq r_! and equivalently) ℓ * ≃ r * \ell_\ast \simeq r^\ast , hence equivalently that ℓ * ⊣ r * \ell^\ast \dashv r^\ast .
Now the hom-isomorphism which is characteristic of the latter adjunction ℓ * ⊣ r * \ell^\ast \dashv r^\ast may be obtained as the following sequence of natural bijections :
PSh ( 𝒮 1 ) ( X 1 , r * ( X 2 ) ) ≃ PSh ( 𝒮 1 ) ( lim ⟶ s 1 → X 1 y ( s 1 ) , r * ( lim ⟶ s 2 → X 2 y ( s 2 ) ) ) ≃ lim ⟵ s 1 → X 1 PSh ( 𝒮 1 ) ( y ( s 1 ) , lim ⟶ s 2 → X 2 r * ( y ( s 2 ) ) ) ≃ lim ⟵ s 1 → X 1 lim ⟶ s 2 → X 2 PSh ( 𝒮 1 ) ( y ( s 1 ) , r * ( y ( s 2 ) ) ) ≃ lim ⟵ s 1 → X 1 lim ⟶ s 2 → X 2 𝒮 2 ( r ( s 1 ) , s 2 ) ≃ lim ⟵ s 1 → X 1 lim ⟶ s 2 → X 2 PSh ( 𝒮 2 ) ( y ( r ( s 1 ) ) , y ( s 2 ) ) ≃ lim ⟵ s 1 → X 1 PSh ( 𝒮 2 ) ( y ( r ( s 1 ) ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( lim ⟶ s 1 → X 1 y ( r ( s 1 ) ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( lim ⟶ s 1 → X 1 𝒮 2 ( ( − ) , r ( s 1 ) ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( lim ⟶ s 1 → X 1 𝒮 2 ( ℓ ( − ) , s 1 ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( lim ⟶ s 1 → X 1 ℓ * ( y ( s 1 ) ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( ℓ * ( lim ⟶ s 1 → X 1 y ( s 1 ) ) , lim ⟶ s 2 → X 2 y ( s 2 ) ) ≃ PSh ( 𝒮 2 ) ( ℓ * ( X 1 ) , X 2 )
\begin{aligned}
&
\mathrm{PSh}(\mathcal{S}_1)
\big(
X_1
,\,
r^\ast(X_2)
\big)
\\
&
\;\simeq\;
\mathrm{PSh}(\mathcal{S}_1)
\Big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
\,
y(s_1)
\,
,\,
r^\ast
\big(
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
\,
y(s_2)
\big)
\Big)
\\
&
\;\simeq\;
\underset{
\underset{
s_1 \to X_1
}{\longleftarrow}
}{\lim}
\mathrm{PSh}(\mathcal{S}_1)
\Big(
y(s_1)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
\,
r^\ast
\big(
y(s_2)
\big)
\Big)
\\
&
\;\simeq\;
\underset{
\underset{
s_1 \to X_1
}{\longleftarrow}
}{\lim}
\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
\mathrm{PSh}(\mathcal{S}_1)
\Big(
y(s_1)
,\,
r^\ast
\big(
y(s_2)
\big)
\Big)
\\
& \;\simeq\;
\underset{
\underset{
s_1 \to X_1
}{\longleftarrow}
}{\lim}
\;
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
\mathcal{S}_2
\big(
r(s_1)
,\,
s_2
\big)
\\
& \;\simeq\;
\underset{
\underset{
s_1 \to X_1
}{\longleftarrow}
}{\lim}
\;
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
\mathrm{PSh}(\mathcal{S}_2)
\Big(
y\big(r(s_1)\big)
,\,
y(s_2)
\Big)
\\
& \;\simeq\;
\underset{
\underset{
s_1 \to X_1
}{\longleftarrow}
}{\lim}
\mathrm{PSh}(\mathcal{S}_2)
\Big(
y\big(r(s_1)\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
\mathrm{PSh}(\mathcal{S}_2)
\Big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
y\big(r(s_1)\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
\mathrm{PSh}(\mathcal{S}_2)
\Big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
\mathcal{S}_2
\big(
(-)
,\,
r(s_1)
\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
\mathrm{PSh}(\mathcal{S}_2)
\Big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
\mathcal{S}_2
\big(
\ell(-)
,\,
s_1
\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
PSh(\mathcal{S}_2)
\Big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
\ell^\ast
\big(
y(s_1)
\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
PSh(\mathcal{S}_2)
\Big(
\ell^\ast
\big(
\underset{
\underset{
s_1 \to X_1
}{\longrightarrow}
}{\lim}
y(s_1)
\big)
,\,
\underset{
\underset{
s_2 \to X_2
}{\longrightarrow}
}{\lim}
y(s_2)
\Big)
\\
& \;\simeq\;
PSh(\mathcal{S}_2)
\Big(
\ell^\ast
(
X_1
)
,\,
X_2
\Big)
\end{aligned}
Here we used repeatedly
the co-Yoneda lemma in the form
X ≃ lim ⟶ y ( s ) → X y ( s ) ,
X
\;\simeq\;
\underset{
\underset{y(s) \to X}{\longrightarrow}
}{\lim}
\,y(s)
\,,
expressing a presheaf X ∈ PSh ( S ) X \,\in\, PSh(S) as a colimit of representable functors y ( s ) y(s) (the colimit is over the comma category y ↓ X y \downarrow X , but that does not even matter in the proof above),
the fact that any hom-functor sends colimits in its first argument to limits ,
the strong Yoneda lemma which says that PSh ( 𝒮 ) ( y ( s ) , X ) ≃ X ( s ) PSh(\mathcal{S})\big(y(s), X\big) \,\simeq\, X(s) ,
the fact that colimits of presheaves are computed objectwise .
As before, the adjunction ℓ * ⊣ r ! \ell^\ast \dashv r_! implies the overlapping adjoint triples by essential uniqueness of adjoint functors (this Prop. ).
Cohesion
Proof
The preservation of finite products by the leftmost adjoint follows by Prop. below.
The fully faithfulness of i ! i_! follows by Prop. below. This implies that also i * i_\ast is fully faithful, by this Prop. .
The proof of Prop. as spelled out below applies verbatim also in
∞
\infty
-category theory . Here, it has interesting examples even without passage to
∞
\infty
-sheaves , when the
∞
\infty
-sites are higher than 1-sites :
This example is a special case of the following general class:
We now spell out the proof of the lemmas used in the proof of Prop. .
Lemma
Given a functor 𝒮 1 → f 𝒮 2 \mathcal{S}_1 \xrightarrow{\;f\;} \mathcal{S}_2 between small categories , its left Kan extension f ! : PSh ( 𝒮 1 ) → PSh ( 𝒮 1 ) f_! \;\colon\; PSh(\mathcal{S}_1) \xrightarrow{\;\;} PSh(\mathcal{S}_1) restricts to f f on representables , in that for s 1 ∈ 𝒮 1 s_1 \,\in\, \mathcal{S}_1 we have a natural isomorphism
f ! ( y ( s 1 ) ) ≃ y ( f ( s 1 ) ) .
f_!\big( y(s_1) \big)
\;\simeq\;
y\big(
f(s_1)
\big)
\,.
Proof
For X ∈ PSh ( 𝒮 2 ) X \,\in\, PSh(\mathcal{S}_2) we have the following sequence of natural isomorphism :
PSh ( 𝒮 2 ) ( f ! ( y ( s 1 ) ) , X ) ≃ PSh ( 𝒮 1 ) ( y ( s 1 ) , f * ( X ) ) ≃ X ( f ( s 1 ) ) ≃ PSh ( 𝒮 2 ) ( y ( f ( s 1 ) ) , X ) .
\begin{aligned}
PSh(\mathcal{S}_2)
\left(
f_!
\left(
y(s_1)
\right)
,\,
X
\right)
& \;\simeq\;
PSh(\mathcal{S}_1)
\left(
y(s_1)
,\,
f^\ast(X)
\right)
\\
&
\;\simeq\;
X\left( f(s_1) \right)
\\
&
\;\simeq\;
PSh(\mathcal{S}_2)
\left(
y\left(f(s_1)\right)
,\,
X
\right)
\,.
\end{aligned}
The first line is the defining adjointness of f ! f_! , the second line the Yoneda lemma over 𝒮 1 \mathcal{S}_1 and the definition of f * f^\ast , while the last line is the Yoneda lemma over 𝒮 2 \mathcal{S}_2 .
Since the composite of these isomorphisms is natural, the Yoneda lemma over PSh ( 𝒮 2 ) op PSh(\mathcal{S}_2)^{op} (which is large but locally small , so that the lemma does apply) implies the claim.
Lemma
Let 𝒮 1 \mathcal{S}_1 and 𝒮 2 \mathcal{S}_2 be small categories with binary products and 𝒮 1 → f 𝒮 2 \mathcal{S}_1 \xrightarrow{\;f\;} \mathcal{S}_2 a functor which preserves these, in that for s , s ′ ∈ 𝒮 1 s, s' \,\in\, \mathcal{S}_1 there is a natural isomorphism f ( s × s ′ ) ≃ f ( X 1 ) × f ( X 2 ) f(s \times s') \,\simeq\, f(X_1) \times f(X_2) . Then also the left Kan extension f ! f_! preserves binary products , in that for X , X ′ ∈ PSh ( 𝒮 1 ) X, X' \,\in\, PSh(\mathcal{S}_1) there is a natural isomorphism
f ! ( X × X ′ ) ≃ f ! ( X ) × f ! ( X ′ ) .
f_!(X \times X')
\;\simeq\;
f_!(X) \times f_!(X')
\,.
Proof
This is the composite of the following sequence of natural isomorphisms :
f ! ( X × X ′ ) ≃ f ! ( ( lim ⟶ s → X y ( s ) ) × ( lim ⟶ s ′ → X y ( s ′ ) ) ) ≃ f ! ( lim ⟶ s → X lim ⟶ s ′ → X ( y ( s ) × y ( s ′ ) ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X f ! ( y ( s ) × y ( s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X f ! ( y ( s × s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X y ( f ( s × s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X y ( f ( s ) × f ( s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X y ( f ( s ) ) × y ( f ( s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X f ! ( y ( s ) ) × f ! ( y ( s ′ ) ) ≃ ( lim ⟶ s → X f ! ( y ( s ) ) ) × ( lim ⟶ s ′ → X f ! ( y ( s ′ ) ) ) .
\begin{aligned}
f_!(X \times X')
& \;\simeq\;
f_!
\Big(\!
\big(
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\,
y(s)
\big)
\times
\big(
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
y(s')
\big)
\!\Big)
\\
& \;\simeq\;
f_!
\Big(
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
\left(
y(s)
\times
y(s')
\right)
\!\!\Big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\big(
y(s)
\times
y(s')
\big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\big(
y(s \times s')
\big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
y\big( f(s \times s') \big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
y\big( f(s) \times f(s') \big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
y\big( f(s) \big)
\times
y\big(f(s') \big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s)
\right)
\times
f_!
\left(
y(s')
\right)
\\
& \;\simeq\;
\Big(\,
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s)
\right)
\!\!\Big)
\times
\Big(\,
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s')
\right)
\!\!\Big).
\end{aligned}
Here
The following Lem. is an immediate variant of Lem. obtained by relaxing the assumptions slightly to a form that is often still readily checked:
Lemma
Let
be a functor between small categories such that
their free coproduct completions PSh ⊔ ( − ) PSh_{\sqcup}(-) have binary products ,
the unique coproduct-preserving extension f ! f_! of f f to these completions preserves binary products , in that for s , s ′ ∈ , 𝒮 1 s, s' \,\in, \mathcal{S}_1 there is a natural isomorphism :
f ! ( y ( s ) × y ( s ′ ) ) ≃ f ! ( y ( s ) ) × f ! ( y ( s ′ ) )
f_!\big( y(s) \times y(s') \big)
\,\simeq\,
f_!\big(y(s)\big) \times f_!\big( y(s') \big)
Then also the left Kan extension f ! : PSh ( 𝒮 1 ) → PSh ( 𝒮 2 ) f_! \,\colon\, PSh(\mathcal{S}_1) \xrightarrow{\;} PSh(\mathcal{S}_2) to the full categories of presheaves preserves products.
Proof
The proof starts and ends as the proof of Prop. , but the main step in between is now more immediate, as it just needs to invoke the assumption:
f ! ( X × X ′ ) ≃ f ! ( ( lim ⟶ s → X y ( s ) ) × ( lim ⟶ s ′ → X y ( s ′ ) ) ) ≃ f ! ( lim ⟶ s → X lim ⟶ s ′ → X ( y ( s ) × y ( s ′ ) ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X f ! ( y ( s ) × y ( s ′ ) ) ≃ lim ⟶ s → X lim ⟶ s ′ → X f ! ( y ( s ) ) × f ! ( y ( s ′ ) ) ≃ ( lim ⟶ s → X f ! ( y ( s ) ) ) × ( lim ⟶ s ′ → X f ! ( y ( s ′ ) ) ) .
\begin{aligned}
f_!(X \times X')
& \;\simeq\;
f_!
\Big(\!
\big(
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\,
y(s)
\big)
\times
\big(
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
y(s')
\big)
\!\Big)
\\
& \;\simeq\;
f_!
\Big(
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
\left(
y(s)
\times
y(s')
\right)
\!\!\Big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\big(
y(s)
\times
y(s')
\big)
\\
& \;\simeq\;
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\;
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s)
\right)
\times
f_!
\left(
y(s')
\right)
\\
& \;\simeq\;
\Big(\,
\underset{
\underset{ s \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s)
\right)
\!\!\Big)
\times
\Big(\,
\underset{
\underset{ s' \to X}{\longrightarrow}
}{\lim}
\,
f_!
\left(
y(s')
\right)
\!\!\Big).
\end{aligned}
In conclusion so far:
Proof
We need to show that f ! f_! preserves (1) the terminal object and (2) binary products . With the given assumption on f f , the first follows with Lem. while the second follows with Lem. or Lem. , respectively.
Proof
We need to show for X , X ′ ∈ PSh ( 𝒮 2 ) X, X' \,\in\, PSh(\mathcal{S}_2) the morphism
PSh ( 𝒮 2 ) ( X , X ′ ) → ( i ! ) X , X ′ PSh ( 𝒮 ` ) ( i ! ( X ) , i ! ( X ′ ) )
PSh(\mathcal{S}_2)
(X,\, X')
\xrightarrow{ \; (i_!)_{X, X'} \; }
PSh(\mathcal{S}_`)
\big(
i_!(X)
,\,
i_!( X')
\big)
is an equivalence. But since i ! i_! is a left adjoint and since X X and X ′ X' are colimits of representables, this morphism is the unique one which reduces to
(1) 𝒮 2 ( s , s ′ ) → i s , s ′ 𝒮 1 ( i ( s ) , i ( s ′ ) )
\mathcal{S}_2
(s,\, s')
\xrightarrow{ \; i_{s, s'} \; }
\mathcal{S}_1
\big(
i(s)
,\,
i( s')
\big)
on representables, where this is an isomorphism by the assumption that i i is fully faithful. If follows that ( i ! ) X , X ′ (i_!)_{X, X'} , is the compostite of the following isomorphisms, and hence an isomorphism:
PSh ( 𝒮 1 ) ( i ! ( X 1 ) , i ! ( X 2 ) ) ≃ PSh ( 𝒮 1 ) ( i ! ( lim ⟶ s → X y ( s ) ) , i ! ( lim ⟶ s ′ → X ′ y ( s ′ ) ) ) ≃ PSh ( 𝒮 1 ) ( lim ⟶ s → X i ! ( y ( s ) ) , lim ⟶ s ′ → X ′ i ! ( y ( s ′ ) ) ) ≃ PSh ( 𝒮 1 ) ( lim ⟶ s → X y ( i ( s ) ) , lim ⟶ s ′ → X ′ y ( i ( s ′ ) ) ) ≃ lim lim ⟶ s ′ → X ′ PSh ( 𝒮 1 ) ( y ( i ( s ) ) , y ( i ( s ′ ) ) ) ≃ lim ⟵ s → X lim ⟶ s ′ → X ′ 𝒮 1 ( i ( s ) , i ( s ′ ) ) ≃ lim ⟵ s → X lim ⟶ s ′ → X ′ 𝒮 2 ( s , s ′ ) ≃ lim ⟵ s → X lim ⟶ s ′ → X ′ PSh ( 𝒮 2 ) ( y ( s ) , y ( s ′ ) ) ≃ PSh ( 𝒮 2 ) ( lim ⟶ s → X y ( s ) , lim ⟶ s ′ → X ′ y ( s ′ ) ) ≃ PSh ( 𝒮 2 ) ( X , X ′ )
\begin{aligned}
&
PSh(\mathcal{S}_1)
\big(
i_!(X_1)
,\,
i_!(X_2)
\big)
\\
&
\;\simeq\;
PSh(\mathcal{S}_1)
\Big(
i_!
\big(
\underset{
\underset{s \to X}{\longrightarrow}
}{\lim}
y(s)
\big)
,\,
i_!
\big(
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
y(s')
\big)
\Big)
\\
&
\;\simeq\;
PSh(\mathcal{S}_1)
\Big(
\underset{
\underset{s \to X}{\longrightarrow}
}{\lim}
i_!
\big(
y(s)
\big)
,\,
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
i_!
\big(
y(s')
\big)
\Big)
\\
&
\;\simeq\;
PSh(\mathcal{S}_1)
\Big(
\underset{
\underset{s \to X}{\longrightarrow}
}{\lim}
y
\big(
i
(s)
\big)
,\,
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
y
\big(
i(s')
\big)
\Big)
\\
&
\;\simeq\;
\underset{
}{\lim}
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
PSh(\mathcal{S}_1)
\Big(
y
\big(
i
(s)
\big)
,\,
y
\big(
i(s')
\big)
\Big)
\\
&
\;\simeq\;
\underset{
\underset{s \to X}{\longleftarrow}
}{\lim}
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
\mathcal{S}_1
\big(
i(s)
,\,
i(s')
\big)
\\
&
\;\simeq\;
\underset{
\underset{s \to X}{\longleftarrow}
}{\lim}
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
\mathcal{S}_2
\big(
s
,\,
s'
\big)
\\
&
\;\simeq\;
\underset{
\underset{s \to X}{\longleftarrow}
}{\lim}
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
PSh(\mathcal{S}_2)
\big(
y(s)
,\,
y(s')
\big)
\\
&
\;\simeq\;
PSh(\mathcal{S}_2)
\Big(
\underset{
\underset{s \to X}{\longrightarrow}
}{\lim}
y(s)
,\,
\underset{
\underset{s' \to X'}{\longrightarrow}
}{\lim}
y(s')
\Big)
\\
&
\;\simeq\;
PSh(\mathcal{S}_2)
\big(
X
,\,
X'
\big)
\end{aligned}
Here the first and last steps are the co-Yoneda lemma and the preservation of its colimits as in the proofs before. In the middle steps we are using Lem. to evaluate i ! i_! on representables and then (1) inside the (co)limits.
References
The above prop. is from:
Peter Johnstone , Remarks on punctual local connectedness , Theory and Applications of Categories, Vol. 25, 2011, No. 3, pp 51-63. (tac )