Redirected from "external tensor products".
Contents
coContext
Monoidal categories
monoidal categories
With braiding
With duals for objects
With duals for morphisms
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
Contents
Idea
The concept of external tensor product is a variant of that of tensor product in a monoidal category when the latter is generalized to indexed monoidal categories (dependent linear type theory ).
Definition
Consider an indexed monoidal category given by a Cartesian fibration
Mod ( − ) ↓ H
\array{
Mod(-)
\\
\downarrow
\\
\mathbf{H}
}
over a cartesian monoidal category H \mathbf{H} .
Definition
(external tensor product) Given X 1 , X 2 ∈ H X_1, X_2 \in \mathbf{H} the external tensor product over these is the functor
⊠ : Mod ( X 1 ) × Mod ( X 2 ) ⟶ Mod ( X 1 × X 2 )
\boxtimes \;\colon\;
Mod(X_1)\times Mod(X_2)
\longrightarrow
Mod(X_1 \times X_2)
given on A 1 ∈ Mod ( X 1 ) A_1 \in Mod(X_1) with A 2 ∈ Mod ( X 2 ) A_2 \in Mod(X_2) by
A 1 ⊠ A 2 ≔ ( p 1 * A 1 ) ⊗ X 1 × X 2 ( p 2 * A 2 ) ∈ Mod ( X 1 × X 2 ) ,
A_1 \boxtimes A_2 \coloneqq (p_1^\ast A_1) \otimes_{X_1 \times X_2} (p_2^\ast A_2)
\in Mod(X_1 \times X_2)
\,,
where p 1 , p 2 p_1, p_2 denote the projection maps out of the Cartesian product X 1 × X 2 ∈ H X_1 \times X_2 \in \mathbf{H} .
Properties
Relation to fiberwise tensor product
Proposition
The fiberwise (“internal”) tensor product over X ∈ H X\in \mathbf{H} is recovered form the external one via a natural equivalence
A 1 ⊗ X A 2 ≃ Δ X * ( A 1 ⊠ A 2 )
A_1 \otimes_X A_2 \simeq \Delta_X^\ast (A_1 \boxtimes A_2)
for A 1 , A 2 ∈ Mod ( X ) A_1, A_2 \in Mod(X) , where Δ : X ⟶ X × X \Delta \colon X \longrightarrow X \times X is the diagonal in H \mathbf{H} on X X .
Generation of Mod ( X 1 × X 2 ) Mod(X_1 \times X_2) from external tensor products
Under suitable conditions on compact generation of Mod ( − ) Mod(-) then one may deduce that Mod ( X 1 × X 2 ) Mod(X_1 \times X_2) is generated under external product from Mod ( X 1 ) Mod(X_1) and Mod ( X 2 ) Mod(X_2) .
(Bondal-vdBerg 03 , BFN 08, proof of prop. 3.24 )
In indexed monoidal categories
Suppose an indexed monoidal category which satisfies the motivic yoga (Wirthmüller context -form) in that:
the corresponding pseudofunctor takes values in adjoint functors
C : Base ⟶ Cat 𝒳 ↦ C 𝒳 ↓ f f ! ↓ ⊣ ↑ f * 𝒴 ↦ C 𝒴
\array{
\mathllap{
\mathbf{C} \,\colon\,
\;
}
Base &\longrightarrow& Cat
\\
\mathcal{X} &\mapsto& \mathbf{C}_{\mathcal{X}}
\\
\Big\downarrow\mathrlap{{}^{f}}
&&
\mathllap{^{f_!}}\Big\downarrow
\dashv
\Big\uparrow\mathrlap{{}^{f^\ast}}
\\
\mathcal{Y}
&\mapsto&
\mathbf{C}_{\mathcal{Y}}
}
between closed monoidal categories
the base change functors f * f^\ast are
besides being strong monoidal functors
also strong closed functors ,
hence the pushforward functors f ! f_! satisfy the projection formula (“Frobenius reciprocity ”)
preserving colimits
pull-push through cartesian squares in Base Base satisfies the Beck-Chevalley condition .
Also assume that
Then:
Proof
Consider any object
𝒲 𝒴 ∈ ∫ C
\mathcal{W}_{\mathcal{Y}}
\,\in\,
\textstyle{\int} \mathbf{C}
and any diagram
𝒱 𝒳 : I ⟶ ∫ C i ↦ 𝒱 ( i ) 𝒳 i
\begin{array}{ccc}
\mathcal{V}_{\mathcal{X}}
\,\colon\,
I &\longrightarrow& \int \mathbf{C}
\\
i &\mapsto& \mathcal{V}(i)_{\mathcal{X}_i}
\end{array}
in the Grothendieck construction category ∫ C \int \mathbf{C} .
Then with
the description of colimits in Grothendieck constructions as (see there )
lim ⟶ i ∈ I ( 𝒱 ( i ) 𝒳 i ) ≃ ( lim ⟶ i ∈ I q ! 𝒳 i 𝒱 ( i ) ) lim ⟶ i ∈ I 𝒳 i
\underset{\underset{i \in I}{\longrightarrow}}{lim}
\big(
\mathcal{V}(i)_{\mathcal{X}_i}
\big)
\;\simeq\;
\left(
\underset{\underset{i \in I}{\longrightarrow}}{lim}
q^{\mathcal{X}_i}_!
\mathcal{V}(i)
\right)_{
\underset{\underset{i \in I}{\longrightarrow}}{lim}
\mathcal{X}_i
}
where
q 𝒳 i : 𝒳 i ⟶ lim ⟶ 𝒳
q^{\mathcal{X}_i}
\;\colon\;
\mathcal{X}_i
\longrightarrow
\underset{\longrightarrow}{lim} \mathcal{X}
denote the coprojections of the colimit of the underlying diagram in Base Base ,
the Beck-Chevalley condition for the following cartesian squares in Base Base
𝒳 i × 𝒴 ⟶ pr 𝒳 i 𝒳 i q 𝒳 i × id 𝒴 ↓ ↓ q 𝒳 i lim ⟶ j ∈ I 𝒳 j × 𝒴 ⟶ pr lim ⟶ 𝒳 lim ⟶ j ∈ I 𝒳 j ,
\array{
\mathcal{X}_i
\times
\mathcal{Y}
&
\overset{\; pr_{\mathcal{X}_i} \;}{\longrightarrow}
&
\mathcal{X}_i
\\
\mathllap{{q}^{\mathcal{X}_i} \times id_{\mathcal{Y}}}
\Big\downarrow
&&
\Big\downarrow
\mathrlap{{}^{ q^{\mathcal{X}_i} }}
\\
\underset{\underset{j \in I}{\longrightarrow}}{lim}
\mathcal{X}_j
\times
\mathcal{Y}
&
\underset
{pr_{\underset{\longrightarrow}{lim}\mathcal{X}}}
{\longrightarrow}
&
\underset{\underset{j \in I}{\longrightarrow}}{lim}
\mathcal{X}_j
\mathrlap{\,,}
}
the fact that both ( − ) × 𝒴 (-) \times \mathcal{Y} and ( − ) ⊗ ( pr 𝒴 ) * 𝒲 (-)\otimes (pr_{\mathcal{Y}})^\ast\mathscr{W} preserve colimits (being left adjoints )
we obtain the following sequence of natural isomorphisms :
( lim ⟶ i ∈ I 𝒱 ( i ) 𝒳 i ) ⊠ 𝒲 𝒴 ≃ ( ( lim ⟶ q ! 𝒳 𝒱 ) lim ⟶ 𝒳 ) ⊠ 𝒲 𝒴 colimit in Groth. constr. ≃ ( ( ( pr lim ⟶ 𝒳 ) * ( lim ⟶ q ! 𝒳 𝒱 ) ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) ( lim ⟶ 𝒳 ) × 𝒴 def. of external tensor ≃ ( ( lim ⟶ ( pr lim ⟶ 𝒳 ) * q ! 𝒳 𝒱 ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) ( lim ⟶ 𝒳 ) × 𝒴 pullback preserves colimits ≃ ( ( lim ⟶ ( q 𝒳 × id 𝒴 ) ! ( pr 𝒳 ) * 𝒱 ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) ( lim ⟶ 𝒳 ) × 𝒴 Beck-Chevalley ≃ ( lim ⟶ ( ( ( q 𝒳 × id 𝒴 ) ! ( pr 𝒳 ) * 𝒱 ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) ) lim ⟶ ( 𝒳 × 𝒴 ) tensoring preserves colimits ≃ ( lim ⟶ ( q 𝒳 × id 𝒴 ) ! ( ( ( pr 𝒳 ) * 𝒱 ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) ) lim ⟶ ( 𝒳 × 𝒴 ) projection formula ≃ lim ⟶ i ∈ I ( ( ( ( pr 𝒳 i ) * 𝒱 ( i ) ) ⊗ ( ( pr 𝒴 ) * 𝒲 ) ) 𝒳 i × 𝒴 ) colimit in Groth. constr. ≃ lim ⟶ i ∈ I ( 𝒱 ( i ) 𝒳 i ⊠ 𝒲 𝒴 ) def of external tensor.
\begin{array}{ll}
\Big(
\underset{\underset{i \in I}{\longrightarrow}}{lim}
\mathscr{V}(i)_{\mathcal{X}_i}
\Big)
\boxtimes
\mathscr{W}_{\mathcal{Y}}
\\
\;\simeq\;
\left(
\big(
\underset{\longrightarrow}{\lim}
q^{\mathcal{X}}_!\mathscr{V}
\big)_{\underset{\longrightarrow}{\lim}\mathcal{X}}
\right)
\boxtimes
\mathscr{W}_{\mathcal{Y}}
&
\text{colimit in Groth. constr.}
\\
\;\simeq\;
\Big(
\big(
(pr_{\underset{\longrightarrow}{lim}\mathcal{X}})^\ast
(
\underset{\longrightarrow}{\lim}
q^{\mathcal{X}}_!\mathscr{V}
)
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast
\mathscr{W}
\big)
\Big)_{
\big(\underset{\longrightarrow}{\lim}\mathcal{X}\big)
\times
\mathcal{Y}
}
&
\text{def. of external tensor}
\\
\;\simeq\;
\Big(
\big(
\underset{\longrightarrow}{\lim}
(pr_{\underset{\longrightarrow}{lim}\mathcal{X}})^\ast
q^{\mathcal{X}}_!
\mathscr{V}
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast
\mathscr{W}
\big)
\Big)_{
\big(\underset{\longrightarrow}{\lim}\mathcal{X}\big)
\times
\mathcal{Y}
}
&
\text{pullback preserves colimits}
\\
\;\simeq\;
\Big(
\big(
\underset{\longrightarrow}{\lim}
(q^{\mathcal{X}} \times id_{\mathcal{Y}} )_!
(pr_{\mathcal{X}})^\ast
\mathscr{V}
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast
\mathscr{W}
\big)
\Big)_{
\big(\underset{\longrightarrow}{\lim}\mathcal{X}\big)
\times
\mathcal{Y}
}
&
\text{Beck-Chevalley}
\\
\;\simeq\;
\bigg(
\underset{\longrightarrow}{\lim}
\Big(
\big(
(q^{\mathcal{X}} \times id_{\mathcal{Y}} )_!
(pr_{\mathcal{X}})^\ast
\mathscr{V}
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast
\mathscr{W}
\big)
\Big)
\bigg)_{
\underset{\longrightarrow}{\lim}
\big(
\mathcal{X}
\times
\mathcal{Y}
\big)
}
&
\text{tensoring preserves colimits}
\\
\;\simeq\;
\bigg(
\underset{\longrightarrow}{\lim}
(q^{\mathcal{X}} \times id_{\mathcal{Y}} )_!
\Big(
\big(
(pr_{\mathcal{X}})^\ast
\mathscr{V}
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast
\mathscr{W}
\big)
\Big)
\bigg)_{
\underset{\longrightarrow}{\lim}
\big(
\mathcal{X}
\times
\mathcal{Y}
\big)
}
&
\text{projection formula}
\\
\;\simeq\;
\underset{\underset{i \in I}{\longrightarrow}}{lim}
\bigg(
\Big(
\big(
(pr_{\mathcal{X}_i})^\ast \mathscr{V}(i)
\big)
\,\otimes\,
\big(
(pr_{\mathcal{Y}})^\ast \mathscr{W}
\big)
\Big)_{
\mathcal{X}_i
\times
\mathcal{Y}
}
\bigg)
&
\text{colimit in Groth. constr.}
\\
\;\simeq\;
\underset{\underset{i \in I}{\longrightarrow}}{lim}
\Big(
\mathscr{V}(i)_{\mathcal{X}_i}
\,\boxtimes\,
\mathscr{W}_{\mathcal{Y}}
\Big)
&
\text{def of external tensor.}
\end{array}
The following proposition still assumes the “motivic yoga” above , but in fact we need to assume the Beck-Chevalley condition only for the very special squares of this form:
𝒳 × 𝒴 ⟶ f × id 𝒳 ′ × 𝒴 pr 𝒳 ↓ ↓ 𝒳 ⟶ f 𝒳 ′
\array{
\mathcal{X} \times \mathcal{Y}
&\overset{ f \times id }{\longrightarrow}&
\mathcal{X}' \times \mathcal{Y}
\\
\mathllap{{}^{ pr_{\mathcal{X}} }}
\Big\downarrow
&&
\Big\downarrow
\\
\mathcal{X}
&\underset{\;\;\; f \;\;\;}{\longrightarrow}&
\mathcal{X}'
}
Proposition
Given
f : 𝒳 ⟶ 𝒳 ′ g : 𝒴 ⟶ 𝒴 ′
\array{
f \,\colon\, \mathcal{X} &\longrightarrow& \mathcal{X}'
\\
g \,\colon\, \mathcal{Y} &\longrightarrow& \mathcal{Y}'
}
we have
for 𝒱 ∈ C 𝒳 ′ \mathscr{V} \,\in\, \mathbf{C}_{\mathcal{X}'} and 𝒲 ∈ C 𝒴 ′ \mathscr{W} \,\in\, \mathbf{C}_{\mathcal{Y}'} natural isomorphism of this form:
(1) ( f × g ) * ( 𝒱 ⊠ 𝒲 ) ≃ ( f * 𝒱 ) ⊠ ( g * 𝒲 )
(f \times g)^\ast (\mathscr{V} \boxtimes \mathscr{W})
\;\simeq\;
\big(f^\ast \mathscr{V}\big)
\boxtimes
\big(g^\ast \mathscr{W}\big)
for 𝒱 ∈ C 𝒳 \mathscr{V} \,\in\, \mathbf{C}_{\mathcal{X}} and 𝒲 ∈ C 𝒴 \mathscr{W} \,\in\, \mathbf{C}_{\mathcal{Y}} natural isomorphism of this form:
(2) ( f × g ) ! ( 𝒱 ⊠ 𝒲 ) ≃ ( f ! 𝒱 ) ⊠ ( g ! 𝒲 ) .
(f \times g)_! (\mathscr{V} \boxtimes \mathscr{W})
\;\simeq\;
\big(f_! \mathscr{V}\big)
\boxtimes
\big(g_! \mathscr{W}\big)
\mathrlap{\,.}
(The first statement is essentially immediate from the fact that pullback
( − ) * (-)^* is assumed to be strong closed, but the second statement is not quite so immediate; it is discussed for the case of
smash product of
retractive spaces and
parameterized spectra in
May & Sigurdsson (2006), Rem. 2.5.8, Prop. 13.7.2 , see also
Malkiewich (2019), Lem. 3.4.1 ,
Malkiewich (2023), Lem. 2.5.1 , and is mentioned in generality but without proof in
Shulman (2012), p. 624 .)
Proof
For the first statement (1) we have the following sequence of natural isomorphisms :
( f × g ) * ( 𝒱 ⊠ 𝒲 ) ≃ ( f × g ) * ( ( pr Y * 𝒱 ) ⊗ Y × Y ′ ( pr Y ′ * 𝒲 ) ) by definition ≃ ( ( f × g ) * pr Y * 𝒱 ) ⊗ X × X ′ ( ( f × g ) * pr Y ′ * 𝒲 ) since pullback is strong closed ≃ ( pr X * f * 𝒱 ) ⊗ X × X ′ ( pr X ′ * g * 𝒲 ) by pseudo-functoriality ≃ ( f * 𝒱 ) ⊠ ( g * 𝒲 ) by definition.
\begin{array}{ll}
(f \times g)^\ast
\big(
\mathscr{V}
\,\boxtimes\,
\mathscr{W}
\big)
\\
\;\simeq\;
(f \times g)^\ast
\Big(
\big(
\mathrm{pr}_{\mathbf{Y}}^\ast
\mathscr{V}
\big)
\,\otimes_{\mathbf{Y} \times \mathbf{Y}'}\,
\big(
\mathrm{pr}_{\mathbf{Y}'}^\ast
\mathscr{W}
\big)
\Big)
&
\text{by definition}
\\
\;\simeq\;
\big(
(f \times g)^\ast
\mathrm{pr}_{\mathbf{Y}}^\ast
\mathscr{V}
\big)
\otimes_{\mathbf{X} \times \mathbf{X}'}
\big(
(f \times g)^\ast
\mathrm{pr}_{\mathbf{Y}'}^\ast
\mathscr{W}
\big)
&
\text{since pullback is strong closed}
\\
\;\simeq\;
\big(
\mathrm{pr}_{\mathbf{X}}^\ast
f^\ast
\mathscr{V}
\big)
\otimes_{\mathbf{X} \times \mathbf{X}'}
\big(
\mathrm{pr}_{\mathbf{X}'}^\ast
g^\ast
\mathscr{W}
\big)
&
\text{by pseudo-functoriality}
\\
\;\simeq\;
\big(f^\ast \mathscr{V}\big)
\boxtimes
\big(g^\ast \mathscr{W}\big)
&
\text{by definition.}
\end{array}
For the second statement (2) , first notice the special case where one of the maps is an identity morphism and the corresponding external tensor factor is the tensor unit ; and notice here that external tensoring with the tensor unit is just pullback to a product (since pullback along the other leg preserves tensor units, being strong monoidal):
𝒱 ⊠ 𝟙 ≃ ( pr 𝒳 ) * 𝒱 .
\mathscr{V} \boxtimes \mathbb{1}
\;\simeq\;
(pr_{\mathcal{X}})^\ast \mathscr{V}
\,.
This way we first find
( f × id ) ! ( 𝒱 ⊠ 𝟙 ) ≃ ( f × id ) ! ( pr 𝒳 * 𝒱 ) by the above comment ≃ pr 𝒳 ′ * ( f ! 𝒱 ) using the BC-condition ≃ ( f ! 𝒱 ) ⊠ 𝟙 by the above comment ,
\begin{array}{ll}
(f \times id)_!
\big(
\mathscr{V} \boxtimes \mathbb{1}
\big)
\\
\;\simeq\;
(f \times id)_!
\big(
pr_{\mathcal{X}}^\ast \mathscr{V}
\big)
&
\text{ by the above comment }
\\
\;\simeq\;
pr_{\mathcal{X}'}^\ast\big(f_! \mathscr{V}\big)
&
\text{ using the BC-condition }
\\
\;\simeq\;
(f_! \mathscr{V}) \boxtimes \mathbb{1}
&
\text{ by the above comment }
\,,
\end{array}
from which the general case is obtained as follows:
( f × g ) ! ( 𝒱 ⊠ 𝒲 ) ≃ ( f × g ) ! ( ( 𝒱 ⊠ 𝟙 ) ⊗ ( 𝟙 ⊠ 𝒲 ) ) by the above comment ≃ ( f × g ) ! ( ( ( id × g ) * ( 𝒱 ⊠ 𝟙 ) ) ⊗ ( 𝟙 ⊠ 𝒲 ) ) by first claim and strong monoidalness ≃ ( f × id ) ! ( id × g ) ! ( ( ( id × g ) * ( 𝒱 ⊠ 𝟙 ) ) ⊗ ( 𝟙 ⊠ 𝒲 ) ) by pseudo-functoriality ≃ ( f × id ) ! ( ( 𝒱 ⊠ 𝟙 ) ⊗ ( ( id × g ) ! ( 𝟙 ⊠ 𝒲 ) ) ) by the projection formula ≃ ( f × id ) ! ( ( 𝒱 ⊠ 𝟙 ) ⊗ ( 𝟙 ⊠ ( g ! 𝒲 ) ) ) by the special case above ≃ ( f × id ) ! ( ( 𝒱 ⊠ 𝟙 ) ⊗ ( f × id ) * ( 𝟙 ⊠ ( g ! 𝒲 ) ) ) by first claim and strong monoidalness ≃ ( ( f × id ) ! ( 𝒱 ⊠ 𝟙 ) ) ⊗ ( 𝟙 ⊠ ( g ! 𝒲 ) ) by the projection formula ≃ ( ( f ! 𝒱 ) ⊠ 𝟙 ) ⊗ ( 𝟙 ⊠ ( g ! 𝒲 ) ) by the special case above ≃ ( f ! 𝒱 ) ⊠ ( g ! 𝒲 ) by the above comment .
\begin{array}{ll}
(f \times g)_!
\big(
\mathscr{V}
\boxtimes
\mathscr{W}
\big)
\\
\;\simeq\;
(f \times g)_!
\big(
(\mathscr{V} \boxtimes \mathbb{1})
\otimes
(\mathbb{1} \boxtimes \mathscr{W})
\big)
&
\text{by the above comment}
\\
\;\simeq\;
(f \times g)_!
\Big(
\big(
(id \times g)^\ast
(\mathscr{V} \boxtimes \mathbb{1})
\big)
\otimes
(\mathbb{1} \boxtimes \mathscr{W})
\Big)
&
\text{by first claim and strong monoidalness}
\\
\;\simeq\;
(f \times id)_!
(id \times g)_!
\Big(
\big(
(id \times g)^\ast
(\mathscr{V} \boxtimes \mathbb{1})
\big)
\otimes
\big(\mathbb{1} \boxtimes \mathscr{W}\big)
\Big)
&
\text{by pseudo-functoriality}
\\
\;\simeq\;
(f \times id)_!
\Big(
\big(\mathscr{V} \boxtimes \mathbb{1}\big)
\otimes
\big(
(id \times g)_!
\big(\mathbb{1} \boxtimes \mathscr{W}\big)
\big)
\Big)
&
\text{by the projection formula}
\\
\;\simeq\;
(f \times id)_!
\Big(
\big(\mathscr{V} \boxtimes \mathbb{1}\big)
\otimes
\big(
\mathbb{1} \boxtimes (g_!\mathscr{W})
\big)
\Big)
&
\text{by the special case above}
\\
\;\simeq\;
(f \times id)_!
\Big(
\big(\mathscr{V} \boxtimes \mathbb{1}\big)
\otimes
(f \times id)^\ast
\big(
\mathbb{1} \boxtimes (g_!\mathscr{W})
\big)
\Big)
&
\text{by first claim and strong monoidalness}
\\
\;\simeq\;
\Big(
(f \times id)_!
\big(\mathscr{V} \boxtimes \mathbb{1}\big)
\Big)
\otimes
\big(
\mathbb{1} \boxtimes (g_!\mathscr{W})
\big)
&
\text{by the projection formula}
\\
\;\simeq\;
\big(
(f_!\mathscr{V}) \boxtimes \mathbb{1}
\big)
\otimes
\big(
\mathbb{1} \boxtimes (g_!\mathscr{W})
\big)
&
\text{by the special case above}
\\
\;\simeq\;
(f_! \mathscr{V})
\boxtimes
(g_! \mathscr{W})
&
\text{by the above comment}.
\end{array}
Corollary
The ( ( f × g ) ! ⊣ ( f × g ) * ) \big((f \times g)_! \dashv (f \times g)^\ast\big) -adjunct f ⊠ g ˜ \widetilde{f \boxtimes g} of an external tensor product of morphisms into the separate pullbacks
𝒱 ⊠ 𝒲 ⟶ ϕ ⊠ γ ( f * 𝒱 ′ ) ⊠ ( g * 𝒲 ′ ) ≃ ( f × g ) * ( 𝒱 ′ ⊠ 𝒲 ′ )
\mathscr{V}
\boxtimes
\mathscr{W}
\overset{ \phi \boxtimes \gamma }{\longrightarrow}
(f^\ast \mathscr{V}') \boxtimes (g^\ast \mathscr{W}')
\;\simeq\;
(f \times g)^\ast
(\mathscr{V}' \boxtimes \mathscr{W}')
is the external tensor product of the separate adjuncts
f ⊠ g ˜ : ( f × g ) ! ( 𝒱 ⊠ 𝒲 ) ≃ ( f ! 𝒱 ) ⊠ ( g ! 𝒲 ) ⟶ ϕ ˜ ⊠ γ ˜ 𝒱 ′ ⊠ 𝒲 ′ ,
\widetilde{ f \boxtimes g }
\,\colon\,
(f \times g)_!( \mathscr{V} \boxtimes \mathscr{W} )
\,\simeq\,
(f_! \mathscr{V}) \boxtimes (g_! \mathscr{W})
\overset{
\widetilde \phi \,\boxtimes\, \widetilde \gamma
}{\longrightarrow}
\mathscr{V}' \boxtimes \mathscr{W}'
\,,
where the natural isomorphisms shown are those form Prop. .
Proof
After restriction along the (non-full) subcategory -inclusion
C 𝒳 × C 𝒴 ⟶ C 𝒳 × 𝒴 ( 𝒱 , 𝒲 ) ↦ 𝒱 ⊠ 𝒲 ( ϕ , γ ) ↓ ↓ ϕ ⊠ γ ( 𝒱 ′ , 𝒲 ′ ) ↦ 𝒱 ′ ⊠ 𝒲 ′
\array{
\mathbf{C}_{\mathcal{X}}
\times
\mathbf{C}_{\mathcal{Y}}
&\longrightarrow&
\mathbf{C}_{\mathcal{X} \times \mathcal{Y}}
\\
\big(\mathscr{V},\, \mathscr{W}\big)
&\mapsto&
\mathscr{V} \boxtimes \mathscr{W}
\\
\mathllap{{}^{ (\phi, \gamma) }}
\Big\downarrow
&&
\Big\downarrow
\mathrlap{{}^{ \phi \boxtimes \gamma }}
\\
\big(\mathscr{V}',\, \mathscr{W}'\big)
&\mapsto&
\mathscr{V}' \boxtimes \mathscr{W}'
}
we can clearly make the restriction of the functors ( f × g ) ! (f \times g)_! and ( f × g ) * (f \times g)^\ast into adjoints by declaring the adjunction counit ϵ \epsilon to be the external tensor product of the ( f ! ⊣ f * ) (f_! \dashv f^\ast) - with the ( f ! ⊣ g * ) (f_! \dashv g^\ast) -adjunction counits . But by uniqueness of adjoints (here ) this must be isomorphic to the actual adjunction counit restricted to external tensor products:
ϵ 𝒳 ⊠ 𝒴 ( ( f × g ) ! ⊣ ( f × g ) * ) ≃ ϵ 𝒳 ( f ! ⊣ f * ) ⊠ ϵ 𝒴 ( g ! ⊣ g * ) .
\epsilon^{
\big((f \times g)_! \dashv (f \times g)^\ast\big)
}_{\mathcal{X} \boxtimes \mathcal{Y}}
\;\;
\simeq
\;\;
\epsilon^{ (f_! \dashv f^\ast) }_{\mathcal{X}}
\,\boxtimes\,
\epsilon^{ (g_! \dashv g^\ast) }_{\mathcal{Y}}
\,.
Now using the expression on the right together with Prop. in the formula (here ) that expresses adjuncts as functor-images composed with the (co)unit gives that the adjunct is formed external tensor-factor wise, as claimed:
ϕ ⊠ γ ˜ ≃ ϵ 𝒱 ′ ⊠ 𝒲 ′ ( f × g ) ! ⊣ ( f × g ) * ∘ ( f × g ) ! ( ϕ ⊠ γ ) by the formula for adjuncts ≃ ( ϵ 𝒱 ′ f ! ⊣ f * ∘ ( f ! ϕ ) ) ⊠ ( ϵ 𝒲 ′ g ! ⊣ g * ∘ ( g ! γ ) ) by the previous discussion ≃ ϕ ˜ ⊠ γ ˜ by the formula for adjuncts.
\begin{array}{ll}
\widetilde{ \phi \boxtimes \gamma }
\\
\;\simeq\;
\epsilon^{
(f \times g)_! \dashv (f \times g)^\ast
}_{ \mathscr{V}' \boxtimes \mathscr{W}' }
\circ
(f \times g)_!\big(\phi \boxtimes \gamma\big)
&
\text{ by the formula for adjuncts }
\\
\;\simeq\;
\big(
\epsilon^{ f_! \dashv f^\ast }_{\mathscr{V}'}
\circ
(f_! \phi)
\big)
\,\boxtimes\,
\big(
\epsilon^{ g_! \dashv g^\ast }_{\mathscr{W}'}
\circ
(g_! \gamma)
\big)
&
\text{ by the previous discussion }
\\
\;\simeq\;
\widetilde \phi
\,\boxtimes\,
\widetilde \gamma
&
\text{ by the formula for adjuncts. }
\end{array}
Proposition
(external pushout-product ) In the situation above, the ⊠ \boxtimes -pushout-product (with respect to the external tensor product) is given by
( ϕ f ) ⊠ ^ ( γ g ) ≃ ( ( ( pr X ′ ) * ϕ ) ⊗ ^ ( ( pr Y ′ ) * γ ) ) f × ^ g
\big(
\phi_f
\big)
\,\widehat{\boxtimes}\,
\big(
\gamma_g
\big)
\;\;\;
\simeq
\;\;\;
\Big(
\big(
(pr_{X'})^\ast \phi
\big)
\,\widehat{\otimes}\,
\big(
(pr_{Y'})^\ast \gamma
\big)
\Big)_{ f \,\widehat{\times}\, g }
where here we use the left-handed convention for component maps in morphisms in the Grothendieck construction:
ϕ f : 𝒱 X → 𝒱 ′ X ′ stands for X → f X ′ f ! 𝒱 → ϕ 𝒱 ′
\phi_f \,\colon\, \mathscr{V}_X \to \mathscr{V}'_{X'}
\;\;\;\;\;\;
\text{stands for}
\;\;\;\;\;\;
\begin{array}{rcl}
X &\xrightarrow{f}& X'
\\
f_!\mathscr{V} &\xrightarrow{\phi}& \mathscr{V}'
\end{array}
Proof
By the general formula for colimits in Grothendieck constructions (here ) the underlying colimit in the base category is the evident one
and the component map over the dashed morphism is the colimiting cocone of the diagram obtained from pushing the separate component maps along the coprojections q ⋅ q_\cdot to form a span in C f × ^ g \mathbf{C}_{f \widehat{\times} g} . This yields:
( f × ^ g ) ! ( ( ( q l ) ! ( ( ( pr X ′ ) * ϕ ) ⊗ ( ( pr Y ) * id 𝒲 ) ) ) ∧ ( ( q r ) ! ( ( ( pr X ) * id 𝒱 ) ⊗ ( ( pr Y ′ ) * γ ) ) ) ) ≃ ( ( ( f × ^ g ) ! ( q l ) ! ( ( ( pr X ′ ) * ϕ ) ⊗ ( ( pr Y ) * id 𝒲 ) ) ) ∧ ( ( f × ^ g ) ! ( q r ) ! ( ( ( pr X ) * id 𝒱 ) ⊗ ( ( pr Y ′ ) * γ ) ) ) ) since the left adjoint ( − ) ! preserves pushouts ≃ ( ( ( id ⊗ g ) ! ( ( ( pr X ′ ) * ϕ ) ⊗ ( ( pr Y ) * id 𝒲 ) ) ) ∧ ( ( f ⊗ id ) ! ( ( ( pr X ) * id 𝒱 ) ⊗ ( ( pr Y ′ ) * γ ) ) ) ) by commutativity of the above diagram ≃ ( ( ( ( ( pr X ′ ) * ϕ ) ⊗ ( ( pr Y ) * id f ! 𝒲 ) ) ) ∧ ( ( ( ( pr X ) * id f ! 𝒱 ) ⊗ ( ( pr Y ′ ) * γ ) ) ) ) by the above result ≃ ( ( pr X ′ ) * ϕ ) ⊗ ^ ( ( pr Y ′ ) * γ ) by definition
\begin{array}{ll}
(f \widehat{\times} g)_!
\Bigg(
\bigg(
(q_l)_!
\Big(
\big(
(pr_{X'})^\ast \phi
\big)
\otimes
\big(
(pr_{Y})^\ast
\mathrm{id}_{\mathscr{W}}
\big)
\Big)
\bigg)
\wedge
\bigg(
(q_r)_!
\Big(
\big(
(pr_X)^\ast
\mathrm{id}_{\mathscr{V}}
\big)
\otimes
\big(
(pr_{Y'})^\ast \gamma
\big)
\Big)
\bigg)
\Bigg)
\\
\;\simeq\;
\Bigg(
\bigg(
(f \widehat{\times} g)_!
(q_l)_!
\Big(
\big(
(pr_{X'})^\ast \phi
\big)
\otimes
\big(
(pr_{Y})^\ast
\mathrm{id}_{\mathscr{W}}
\big)
\Big)
\bigg)
\wedge
\bigg(
(f \widehat{\times} g)_!
(q_r)_!
\Big(
\big(
(pr_X)^\ast
\mathrm{id}_{\mathscr{V}}
\big)
\otimes
\big(
(pr_{Y'})^\ast \gamma
\big)
\Big)
\bigg)
\Bigg)
&
\begin{array}{l}
\text{since the left adjoint}\; (-)_!
\\
\text{preserves pushouts}
\end{array}
\\
\;\simeq\;
\Bigg(
\bigg(
(id \otimes g)_!
\Big(
\big(
(pr_{X'})^\ast \phi
\big)
\otimes
\big(
(pr_{Y})^\ast
\mathrm{id}_{\mathscr{W}}
\big)
\Big)
\bigg)
\wedge
\bigg(
(f \otimes id)_!
\Big(
\big(
(pr_X)^\ast
\mathrm{id}_{\mathscr{V}}
\big)
\otimes
\big(
(pr_{Y'})^\ast \gamma
\big)
\Big)
\bigg)
\Bigg)
&
\begin{array}{l}
\text{by commutativity of}
\\
\text{the above diagram}
\end{array}
\\
\;\simeq\;
\Bigg(
\bigg(
\Big(
\big(
(pr_{X'})^\ast \phi
\big)
\otimes
\big(
(pr_{Y})^\ast
\mathrm{id}_{f_!\mathscr{W}}
\big)
\Big)
\bigg)
\wedge
\bigg(
\Big(
\big(
(pr_X)^\ast
\mathrm{id}_{f_!\mathscr{V}}
\big)
\otimes
\big(
(pr_{Y'})^\ast \gamma
\big)
\Big)
\bigg)
\Bigg)
&
\text{by the above result}
\\
\;\simeq\;
\big(
(pr_{X'})^\ast \phi
\big)
\,\displaystyle{\widehat{\otimes}}\,
\big(
(pr_{Y'})^\ast \gamma
\big)
&
\text{by definition}
\end{array}
Here in the second-but-last step we used (2) .
Examples
References
The notion of the external tensor product of vector bundles originates in discussion of topological K-theory :
Michael Atiyah , §2.6 in: K-theory , Harvard Lecture 1964 (notes by D. W. Anderson), Benjamin (1967) [pdf , pdf ]
Raoul Bott , p. 19 of: Lectures on K ( X ) K(X) , Benjamin (1969) [pdf , pdf ]
Max Karoubi , §4.9 in: K-Theory – An introduction , Grundlehren der mathematischen Wissenschaften 226 , Springer (1978) [pdf , doi:10.1007/978-3-540-79890-3 ]
The notion of external tensor product of representations seems to be folklore , it is mentioned in most textbooks but without any attribution:
The external tensor product of perverse sheaves :
The external tensor product of of quasicoherent sheaves in (derived ) algebraic geometry :
The external product on cobordism rings :
and on differential cobordism rings :
and in the Hodge-filtered version :
The external smash product of retractive spaces and of parameterized spectra :
For general abstract literature dealing with the external tensor products see the references at indexed monoidal category and at dependent linear type theory , such as