Koszul coherence of derived sheaf tensor

For bounded-above complexes ${\mathcal{F}}^{\bullet },{\mathcal{G}}^{\bullet }$ the Koszul symmetry $S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})$ is an isomorphism of cochain complexes, natural in the two arguments, and on the summand ${\mathcal{P}}^i(\mathcal{F}){\otimes }_{\mathbb{Z}}{\mathcal{P}}^j(\mathcal{G})$ it is the Koszul map $x\otimes y\mapsto (-1{)}^{ij}y\otimes x$ [F5]. By the definition of the derived tensor product [F2] its source and target are ${\mathcal{F}}^{\bullet }{\otimes }_{\mathbb{Z}}^{\mathbf{L}}{\mathcal{G}}^{\bullet }$ and ${\mathcal{G}}^{\bullet }{\otimes }_{\mathbb{Z}}^{\mathbf{L}}{\mathcal{F}}^{\bullet }$, so $Q(S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G}))$ is a morphism between them in $D^{-}$ acting on each summand by the displayed rule, and it is an isomorphism with inverse $Q(S(\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{F}))$: $Q(S(\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{F}))\circ Q(S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G}))=Q(S(\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{F})\circ S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G}))=Q(\mathrm{id})=\mathrm{id}$ and symmetrically, because $S$ is involutive [F6] and $Q$ is a functor [F9].

For cochain maps $\phi :{\mathcal{F}}^{\bullet }\to {\mathcal{F}}^{\mathrm{\prime }\bullet }$ and $\psi :{\mathcal{G}}^{\bullet }\to {\mathcal{G}}^{\mathrm{\prime }\bullet }$ naturality of $S$ [F5] gives the cochain-map identity $S(\mathcal{P}{\mathcal{F}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{G}}^{\mathrm{\prime }})\circ \mathrm{Tot}(\mathcal{P}\phi {\otimes }_{\mathbb{Z}}\mathcal{P}\psi )=\mathrm{Tot}(\mathcal{P}\psi {\otimes }_{\mathbb{Z}}\mathcal{P}\phi )\circ S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})$. A cochain map is represented in the localization by the left roof with identity denominator [F13], so the bifunctor formula [F3] gives $\phi {\otimes }^{\mathbf{L}}\psi =Q(\mathrm{Tot}(\mathcal{P}\phi {\otimes }_{\mathbb{Z}}\mathcal{P}\psi ))$ and $\psi {\otimes }^{\mathbf{L}}\phi =Q(\mathrm{Tot}(\mathcal{P}\psi {\otimes }_{\mathbb{Z}}\mathcal{P}\phi ))$; applying the functor $Q$ to the displayed identity therefore yields ${\sigma }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }},{\mathcal{G}}^{\mathrm{\prime }})\circ (\phi {\otimes }^{\mathbf{L}}\psi )=(\psi {\otimes }^{\mathbf{L}}\phi )\circ {\sigma }^{\mathbf{L}}(\mathcal{F},\mathcal{G})$, so ${\sigma }^{\mathbf{L}}$ is natural with respect to cochain maps [F9].

The four factors of ${\lambda }^{\mathbf{L}}(\mathcal{F})$ and ${\rho }^{\mathbf{L}}(\mathcal{F})$ are invertible in $D^{-}$: $Q({\alpha }_{\mathcal{F}})$ because ${\alpha }_{\mathcal{F}}$ is a quasi-isomorphism [F1, F9]; $Q(\mathrm{\Lambda }(\mathcal{P}\mathcal{F}))$ and $Q(\mathrm{P}(\mathcal{P}\mathcal{F}))$ because $\mathrm{\Lambda },\mathrm{P}$ are isomorphisms of cochain complexes [F5]; and $Q(\mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\mathrm{id}}_{\mathcal{P}\mathcal{F}}))$, $Q(\mathrm{Tot}({\mathrm{id}}_{\mathcal{P}\mathcal{F}}\otimes {\alpha }_{\mathbb{Z}[0]}))$ because ${\alpha }_{\mathbb{Z}[0]}$ is a quasi-isomorphism, $\mathcal{P}(\mathcal{F})$ and $\mathcal{P}(\mathbb{Z}[0])$ are bounded-above complexes of flat sheaves [F1] hence K-flat [F12], so [F10] makes these maps quasi-isomorphisms. Hence ${\lambda }^{\mathbf{L}}(\mathcal{F})$ and ${\rho }^{\mathbf{L}}(\mathcal{F})$ are isomorphisms in $D^{-}$ from the derived tensor products to ${\mathcal{F}}^{\bullet }$ as displayed [F2, F9].

Because $Q$ is a functor [F9], the defining composite is $Q({\alpha }_{\mathcal{F}}\circ \mathrm{\Lambda }(\mathcal{P}\mathcal{F})\circ \mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\mathrm{id}}_{\mathcal{P}\mathcal{F}}))$. Naturality of the sheaf-level unitor in each degree [F8] says ${\lambda }_{{\mathcal{F}}^n}\circ ({\mathrm{id}}_{{\mathbb{Z}}_X}\otimes {\alpha }_{\mathcal{F}}^n)={\alpha }_{\mathcal{F}}^n\circ {\lambda }_{(\mathcal{P}\mathcal{F}{)}^n}$ for every $n$, which by [F15] is the cochain-map identity $\mathrm{\Lambda }({\mathcal{F}}^{\bullet })\circ \mathrm{Tot}({\mathrm{id}}_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathcal{F}})={\alpha }_{\mathcal{F}}\circ \mathrm{\Lambda }(\mathcal{P}\mathcal{F})$; substituting it and using functoriality of $\mathrm{Tot}$ and the identity $({\mathrm{id}}_{{\mathbb{Z}}_X}\otimes {\alpha }_{\mathcal{F}})\circ ({\alpha }_{\mathbb{Z}[0]}\otimes {\mathrm{id}}_{\mathcal{P}\mathcal{F}})={\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathcal{F}}$ gives ${\lambda }^{\mathbf{L}}(\mathcal{F})=Q(\mathrm{\Lambda }({\mathcal{F}}^{\bullet })\circ \mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathcal{F}}))$, and the same computation with $\rho$ and $\mathrm{P}$ [F7] gives ${\rho }^{\mathbf{L}}(\mathcal{F})=Q(\mathrm{P}({\mathcal{F}}^{\bullet })\circ \mathrm{Tot}({\alpha }_{\mathcal{F}}\otimes {\alpha }_{\mathbb{Z}[0]}))$. For an abelian sheaf $\mathcal{F}$ read in degree zero the complex ${\mathcal{F}}_0$ is concentrated in degree zero, so $\mathrm{\Lambda }({\mathcal{F}}_0)$ and $\mathrm{P}({\mathcal{F}}_0)$ are the sheaf-level unitors ${\lambda }_{\mathcal{F}}$ and ${\rho }_{\mathcal{F}}$ in degree zero and zero in all other degrees [F8, F11], and $\mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{{\mathcal{F}}_0})$ is the comparison $c_{{\mathbb{Z}}_X,\mathcal{F}}$ [F4]; hence ${\lambda }^{\mathbf{L}}({\mathcal{F}}_0)=Q({\lambda }_{\mathcal{F}})\circ c_{{\mathbb{Z}}_X,\mathcal{F}}$ and ${\rho }^{\mathbf{L}}({\mathcal{F}}_0)=Q({\rho }_{\mathcal{F}})\circ c_{\mathcal{F},{\mathbb{Z}}_X}$.

For $p,q\ge 0$ the cochain map ${\kappa }_{p,q}$ is an isomorphism: by [F16] its source and target have ${\mathbb{Z}}_X{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X$ resp. ${\mathbb{Z}}_X$ as only nonzero term, in degree $p+q$, its only nonzero component is the unit identification ${\mathbb{Z}}_X{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X\to {\mathbb{Z}}_X$ [F8], which is an isomorphism, and all other components are zero maps between zero objects. Hence $Q({\kappa }_{p,q})$ is invertible in $D^{-}$ [F9]. The factor $Q(\mathrm{Tot}({\alpha }_{\mathbb{Z}[-p]}\otimes {\alpha }_{\mathbb{Z}[-q]}))$ is invertible as well: ${\alpha }_{\mathbb{Z}[-p]},{\alpha }_{\mathbb{Z}[-q]}$ are quasi-isomorphisms and $\mathcal{P}(\mathbb{Z}[-p]),\mathcal{P}(\mathbb{Z}[-q])$ are bounded-above complexes of flat sheaves [F1] hence K-flat [F12], and the target shifted units are K-flat by [F17]. Factoring the tensor of the two augmentations into two maps, each with a K-flat other factor, shows that $\mathrm{Tot}({\alpha }_{\mathbb{Z}[-p]}\otimes {\alpha }_{\mathbb{Z}[-q]})$ is a quasi-isomorphism [F10] and $Q$ carries it to an isomorphism [F9]. Therefore $\kappa (p,q)$ is a canonical isomorphism [F3].

$\mathrm{\Theta }$ and $\mathrm{\Xi }$ are invertible in $D^{-}$: the augmentations are quasi-isomorphisms [F1] and the other factors are bounded-above complexes of flat sheaves [F1] hence K-flat [F12], so [F10] makes the total tensor maps quasi-isomorphisms and [F9] makes their images under $Q$ invertible; $Q(A(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{H}))$ is invertible because $A$ is an isomorphism of cochain complexes [F5]. Hence ${\alpha }^{\mathbf{L}}(\mathcal{F},\mathcal{G},\mathcal{H})={\mathrm{\Xi }}^{-1}\circ Q(A)\circ \mathrm{\Theta }$ is a canonical isomorphism in $D^{-}$ [F3, F9], its source and target being the two parenthesizations $(\mathcal{F}{\otimes }^{\mathbf{L}}\mathcal{G}){\otimes }^{\mathbf{L}}\mathcal{H}$ and $\mathcal{F}{\otimes }^{\mathbf{L}}(\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H})$ of the triple derived tensor product [F2].

Let $\mathcal{F},\mathcal{G}$ be abelian sheaves read in degree zero and write $\mathcal{F}[0]$ for the complex concentrated in that degree [F16]. Naturality of $S$ [F5] applied to the cochain maps ${\alpha }_{\mathcal{F}[0]},{\alpha }_{\mathcal{G}[0]}$ gives $S(\mathcal{F}[0],\mathcal{G}[0])\circ \mathrm{Tot}({\alpha }_{\mathcal{F}[0]}{\otimes }_{\mathbb{Z}}{\alpha }_{\mathcal{G}[0]})=\mathrm{Tot}({\alpha }_{\mathcal{G}[0]}{\otimes }_{\mathbb{Z}}{\alpha }_{\mathcal{F}[0]})\circ S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})$. Both total complexes in the outer positions are concentrated in degree zero with single term $\mathcal{G}{\otimes }_{\mathbb{Z}}\mathcal{F}$ resp. $\mathcal{F}{\otimes }_{\mathbb{Z}}\mathcal{G}$ [F11], so their cochain maps are determined by their degree-zero components [F15]; in degree zero the Koszul sign is $(-1{)}^{0\cdot 0}=1$ [F5], so $S(\mathcal{F}[0],\mathcal{G}[0])={\sigma }_{\mathcal{F},\mathcal{G}}$ as cochain maps, comparing with the sheaf-level symmetry of [F7]. Applying $Q$, using that $c_{\mathcal{G},\mathcal{F}}=Q(\mathrm{Tot}({\alpha }_{\mathcal{G}[0]}\otimes {\alpha }_{\mathcal{F}[0]}))$ and $c_{\mathcal{F},\mathcal{G}}=Q(\mathrm{Tot}({\alpha }_{\mathcal{F}[0]}\otimes {\alpha }_{\mathcal{G}[0]}))$ [F4] and ${\sigma }^{\mathbf{L}}(\mathcal{F},\mathcal{G})=Q(S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G}))$, gives the first identity of clause 4(b).

For $p,q\ge 0$ put $m:=(-1{)}^{pq}{\mathrm{id}}_{{\mathbb{Z}}_X[-p-q]}$. The complexes $\mathrm{Tot}({\mathbb{Z}}_X[-p]{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X[-q])$ and $\mathrm{Tot}({\mathbb{Z}}_X[-q]{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X[-p])$ have a single nonzero term in degree $p+q$ [F16], so cochain maps between them are determined by their component in that degree [F15]. On that component the cochain map $S({\mathbb{Z}}_X[-p],{\mathbb{Z}}_X[-q])$ is $(-1{)}^{pq}$ times the exchange of the two factors [F6], the composite ${\kappa }_{q,p}^{-1}\circ m\circ {\kappa }_{p,q}$ is multiplication of the two generators followed by $(-1{)}^{pq}$ followed by the inverse of multiplication, and both are therefore the map ${\mathbb{Z}}_X{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X\to {\mathbb{Z}}_X{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X$ sending $1\otimes 1$ to $(-1{)}^{pq}(1\otimes 1)$; hence $S({\mathbb{Z}}_X[-p],{\mathbb{Z}}_X[-q])={\kappa }_{q,p}^{-1}\circ m\circ {\kappa }_{p,q}$ as cochain maps. Naturality of $S$ [F5] applied to the cochain maps ${\alpha }_{\mathbb{Z}[-p]},{\alpha }_{\mathbb{Z}[-q]}$ gives $S({\mathbb{Z}}_X[-p],{\mathbb{Z}}_X[-q])\circ \mathrm{Tot}({\alpha }_{\mathbb{Z}[-p]}\otimes {\alpha }_{\mathbb{Z}[-q]})=\mathrm{Tot}({\alpha }_{\mathbb{Z}[-q]}\otimes {\alpha }_{\mathbb{Z}[-p]})\circ S(\mathcal{P}\mathbb{Z}[-p],\mathcal{P}\mathbb{Z}[-q])$, that is $Q(c_{q,p})\circ {\sigma }^{\mathbf{L}}({\mathbb{Z}}_X[-p],{\mathbb{Z}}_X[-q])=Q({\kappa }_{q,p}^{-1}\circ m\circ {\kappa }_{p,q})\circ Q(c_{p,q})$ with $c_{p,q}=\mathrm{Tot}({\alpha }_{\mathbb{Z}[-p]}\otimes {\alpha }_{\mathbb{Z}[-q]})$. The comparison $c_{q,p}$ is a quasi-isomorphism [F1, F10, F12], so its image under $Q$ is invertible [F9], and multiplying the displayed identity by $Q(c_{q,p}{)}^{-1}$ on the left gives ${\sigma }^{\mathbf{L}}({\mathbb{Z}}_X[-p],{\mathbb{Z}}_X[-q])=Q(c_{q,p}{)}^{-1}\circ Q({\kappa }_{q,p}^{-1})\circ Q(m)\circ Q({\kappa }_{p,q})\circ Q(c_{p,q})=\kappa (q,p)\circ ((-1{)}^{pq}\mathrm{id})\circ \kappa (p,q{)}^{-1}$, which is clause 4(c).

For cochain maps $f:\mathcal{F}\to {\mathcal{F}}^{\mathrm{\prime }}$, $g:\mathcal{G}\to {\mathcal{G}}^{\mathrm{\prime }}$ and $h:\mathcal{H}\to {\mathcal{H}}^{\mathrm{\prime }}$, put $T(C,D)=\mathrm{Tot}(C{\otimes }_{\mathbb{Z}}D)$, $L=T(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})$, $L^{\mathrm{\prime }}=T(\mathcal{P}{\mathcal{F}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{G}}^{\mathrm{\prime }})$, $R=T(\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{H})$, $R^{\mathrm{\prime }}=T(\mathcal{P}{\mathcal{G}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{H}}^{\mathrm{\prime }})$, $u=T(\mathcal{P}f,\mathcal{P}g):L\to L^{\mathrm{\prime }}$ and $v=T(\mathcal{P}g,\mathcal{P}h):R\to R^{\mathrm{\prime }}$. Naturality of the augmentation [F1] yields the typed comparison squares ${\mathrm{\Theta }}^{\mathrm{\prime }}\circ QT(\mathcal{P}u,\mathcal{P}h)=QT(u,\mathcal{P}h)\circ \mathrm{\Theta }$ and ${\mathrm{\Xi }}^{\mathrm{\prime }}\circ QT(\mathcal{P}f,\mathcal{P}v)=QT(\mathcal{P}f,v)\circ \mathrm{\Xi }$. Naturality of the strict associator [F5] gives $QA(\mathcal{P}{\mathcal{F}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{G}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{H}}^{\mathrm{\prime }})\circ QT(u,\mathcal{P}h)=QT(\mathcal{P}f,v)\circ QA(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{H})$. Composing these three squares and inverting $\mathrm{\Xi },{\mathrm{\Xi }}^{\mathrm{\prime }}$ [step 1.6] proves ${\alpha }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }},{\mathcal{G}}^{\mathrm{\prime }},{\mathcal{H}}^{\mathrm{\prime }})\circ ((Qf{\otimes }^{\mathbf{L}}Qg){\otimes }^{\mathbf{L}}Qh)=(Qf{\otimes }^{\mathbf{L}}(Qg{\otimes }^{\mathbf{L}}Qh))\circ {\alpha }^{\mathbf{L}}(\mathcal{F},\mathcal{G},\mathcal{H})$. The intermediate objects are $T(\mathcal{P}L,\mathcal{P}\mathcal{H})$, $T(L,\mathcal{P}\mathcal{H})$, $T(\mathcal{P}\mathcal{F},\mathcal{P}R)$ and $T(\mathcal{P}\mathcal{F},R)$ and their primed counterparts, so every composite is typed.

Let $\mathcal{F},\mathcal{G},\mathcal{H}$ be abelian sheaves in degree zero, put $T(C,D)=\mathrm{Tot}(C{\otimes }_{\mathbb{Z}}D)$, $L=T(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})$, $R=T(\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{H})$, $W=(\mathcal{F}\otimes \mathcal{G})[0]$ and $V=(\mathcal{G}\otimes \mathcal{H})[0]$. Write $m_{FG}=T({\alpha }_{\mathcal{F}},{\alpha }_{\mathcal{G}}):L\to W$ and $m_{GH}=T({\alpha }_{\mathcal{G}},{\alpha }_{\mathcal{H}}):R\to V$ for the cochain representatives of $c_{\mathcal{F},\mathcal{G}}$ and $c_{\mathcal{G},\mathcal{H}}$ [F4]. The left side of the associator-comparison identity of clause 4(b) uses $\mathcal{P}(m_{GH})$ and the right side uses $\mathcal{P}(m_{FG})$ [F3]. Naturality of the augmentation [F1] gives the typed identities ${\alpha }_V\circ \mathcal{P}(m_{GH})=m_{GH}\circ {\alpha }_R$ and ${\alpha }_W\circ \mathcal{P}(m_{FG})=m_{FG}\circ {\alpha }_L$. Tensor the first with ${\mathrm{id}}_{\mathcal{P}\mathcal{F}}$ and the second with ${\mathrm{id}}_{\mathcal{P}\mathcal{H}}$, then use the definitions of $\mathrm{\Xi },\mathrm{\Theta }$ [step 1.6]. The two composites in clause 4(b) reduce to the routes of the strict naturality square $A(\mathcal{F}[0],\mathcal{G}[0],\mathcal{H}[0])\circ T(T({\alpha }_{\mathcal{F}},{\alpha }_{\mathcal{G}}),{\alpha }_{\mathcal{H}})=T({\alpha }_{\mathcal{F}},T({\alpha }_{\mathcal{G}},{\alpha }_{\mathcal{H}}))\circ A(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G},\mathcal{P}\mathcal{H})$. This is an equality of cochain maps by strict associator naturality [F5]. Its degree-zero target map is the sheaf-level associator ${\alpha }_{\mathcal{F},\mathcal{G},\mathcal{H}}$ [F7, F11]. Applying $Q$ proves clause 4(b), without inverting any comparison $c$.

Let $u:{\mathcal{F}}^{\bullet }\to {\mathcal{F}}^{\mathrm{\prime }\bullet }$ and $v:{\mathcal{G}}^{\bullet }\to {\mathcal{G}}^{\mathrm{\prime }\bullet }$ be arbitrary morphisms of $D^{-}$; by the roof calculus [F13, F14] they are represented by left roofs $u=Q(h)Q(s{)}^{-1}$ and $v=Q(k)Q(t{)}^{-1}$ with quasi-isomorphism denominators $s:\mathcal{V}\to \mathcal{F}$, $t:\mathcal{W}\to \mathcal{G}$. The formula of [F3] gives $(u{\otimes }^{\mathbf{L}}v)=Q(\mathrm{Tot}(\mathcal{P}h{\otimes }_{\mathbb{Z}}\mathcal{P}k))\circ Q(\mathrm{Tot}(\mathcal{P}s{\otimes }_{\mathbb{Z}}\mathcal{P}t){)}^{-1},(v{\otimes }^{\mathbf{L}}u)=Q(\mathrm{Tot}(\mathcal{P}k{\otimes }_{\mathbb{Z}}\mathcal{P}h))\circ Q(\mathrm{Tot}(\mathcal{P}t{\otimes }_{\mathbb{Z}}\mathcal{P}s){)}^{-1},$ and the two denominator factors are invertible in $D^{-}$, since $\mathcal{P}s,\mathcal{P}t$ are quasi-isomorphisms and a quasi-isomorphism in either variable induces an isomorphism of derived tensor products [F1, F3, F9]. Naturality of $S$ [F5] applied to the cochain maps $\mathcal{P}s,\mathcal{P}t,\mathcal{P}h,\mathcal{P}k$ gives $S(\mathcal{P}{\mathcal{F}}^{\mathrm{\prime }},\mathcal{P}{\mathcal{G}}^{\mathrm{\prime }})\circ \mathrm{Tot}(\mathcal{P}h\otimes \mathcal{P}k)=\mathrm{Tot}(\mathcal{P}k\otimes \mathcal{P}h)\circ S(\mathcal{P}\mathcal{V},\mathcal{P}\mathcal{W})$ and $S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G})\circ \mathrm{Tot}(\mathcal{P}s\otimes \mathcal{P}t)=\mathrm{Tot}(\mathcal{P}t\otimes \mathcal{P}s)\circ S(\mathcal{P}\mathcal{V},\mathcal{P}\mathcal{W})$; the second rearranges, by invertibility of the two outer factors [F9], to $Q(\mathrm{Tot}(\mathcal{P}t\otimes \mathcal{P}s){)}^{-1}\circ Q(S(\mathcal{P}\mathcal{F},\mathcal{P}\mathcal{G}))=Q(S(\mathcal{P}\mathcal{V},\mathcal{P}\mathcal{W}))\circ Q(\mathrm{Tot}(\mathcal{P}s\otimes \mathcal{P}t){)}^{-1}$. Substituting this and the first identity into the two displayed composites shows ${\sigma }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }},{\mathcal{G}}^{\mathrm{\prime }})\circ (u{\otimes }^{\mathbf{L}}v)=(v{\otimes }^{\mathbf{L}}u)\circ {\sigma }^{\mathbf{L}}(\mathcal{F},\mathcal{G})$, so ${\sigma }^{\mathbf{L}}$ is natural in both variables; with [step 1.1] this proves clause 1.

For a cochain map $f:\mathcal{F}\to {\mathcal{F}}^{\mathrm{\prime }}$, write $Z={\mathbb{Z}}_X[0]$ and $T(C,D)=\mathrm{Tot}(C{\otimes }_{\mathbb{Z}}D)$. The defining left unitor is ${\lambda }^{\mathbf{L}}(\mathcal{F})=Q({\alpha }_{\mathcal{F}})\circ Q(\mathrm{\Lambda }(\mathcal{P}\mathcal{F}))\circ Q(T({\alpha }_Z,{\mathrm{id}}_{\mathcal{P}\mathcal{F}}))$ [step 1.3]. Naturality ${\alpha }_{{\mathcal{F}}^{\mathrm{\prime }}}\circ \mathcal{P}f=f\circ {\alpha }_{\mathcal{F}}$ [F1] and $\mathrm{\Lambda }(\mathcal{P}{\mathcal{F}}^{\mathrm{\prime }})\circ T({\mathrm{id}}_Z,\mathcal{P}f)=\mathcal{P}f\circ \mathrm{\Lambda }(\mathcal{P}\mathcal{F})$ [F5] give the typed equality ${\lambda }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }})\circ ({\mathrm{id}}_Z{\otimes }^{\mathbf{L}}Qf)=Qf\circ {\lambda }^{\mathbf{L}}(\mathcal{F})$: the two middle squares are the naturality of $T({\alpha }_Z,-)$ and of $\mathrm{\Lambda }$. The analogous argument for the right unitor $\mathrm{P}$ gives ${\rho }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }})\circ (Qf{\otimes }^{\mathbf{L}}{\mathrm{id}}_Z)=Qf\circ {\rho }^{\mathbf{L}}(\mathcal{F})$. If a derived morphism is represented by a left roof $Qh\circ Q{s}^{-1}$, apply each equality to $h$ and its quasi-isomorphism denominator $s$, then invert only the equality for $s$; the bifunctor [F3] sends $Qs$ to an isomorphism. This proves naturality of both unitors for arbitrary derived morphisms.

By the form of [step 1.4] the unitor is ${\lambda }^{\mathbf{L}}({\mathbb{Z}}_X[-q])=Q(\mathrm{\Lambda }({\mathbb{Z}}_X[-q])\circ \mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathbb{Z}[-q]}))$. The cochain maps $\mathrm{\Lambda }({\mathbb{Z}}_X[-q])$ and ${\kappa }_{0,q}$ have the same source $\mathrm{Tot}({\mathbb{Z}}_X[0]{\otimes }_{\mathbb{Z}}{\mathbb{Z}}_X[-q])$, the same target ${\mathbb{Z}}_X[-q]$, and the same only nonzero component, namely the unit identification in degree $q$: for ${\kappa }_{0,q}$ this is its definition, and for $\mathrm{\Lambda }$ it holds because $\mathrm{\Lambda }$ is the degreewise unitor [F5, F8] and ${\mathbb{Z}}_X[-q]$ has its only nonzero term in degree $q$ [F16]. Hence $\mathrm{\Lambda }({\mathbb{Z}}_X[-q])={\kappa }_{0,q}$ and ${\lambda }^{\mathbf{L}}({\mathbb{Z}}_X[-q])=Q({\kappa }_{0,q}\circ \mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathbb{Z}[-q]}))$. Composing with $\kappa (0,q)=Q(\mathrm{Tot}({\alpha }_{\mathbb{Z}[0]}\otimes {\alpha }_{\mathbb{Z}[-q]}){)}^{-1}\circ Q({\kappa }_{0,q}^{-1})$ and using functoriality of $Q$ [F9] gives ${\lambda }^{\mathbf{L}}({\mathbb{Z}}_X[-q])\circ \kappa (0,q)=Q({\kappa }_{0,q})\circ Q({\kappa }_{0,q}^{-1})=Q(\mathrm{id})=\mathrm{id}$. The same argument with $\mathrm{P}({\mathbb{Z}}_X[-q])={\kappa }_{q,0}$ in place of $\mathrm{\Lambda }$ gives ${\rho }^{\mathbf{L}}({\mathbb{Z}}_X[-q])\circ \kappa (q,0)=\mathrm{id}$ [F5, F8, F16].

Write $T(B,C)=\mathrm{Tot}(B\otimes C)$ and $Z={\mathbb{Z}}_X[0]$. The ordinary identities in clause 4(a) follow by applying $Q$ to [F6], with $Z$ as the actual unit. In particular no identification of $\mathcal{P}Z$ with $Z$ as complexes is used. A total tensor of bounded-above K-flat complexes $B,C$ is K-flat: for acyclic bounded-above $E$, the associator identifies $T(E,T(B,C))$ with $T(T(E,B),C)$, which is acyclic by K-flatness twice. This proves the closure needed below directly from [F5] and the definition of K-flatness; $Z$ is K-flat by [F17]. For a parenthesized derived tensor tree let $M_t$ be its chosen complex model and $B_t$ the corresponding ordinary tensor tree with nonunit leaves $\mathcal{P}{\mathcal{F}}_i$ and unit leaves $Z$. Construct cochain quasi-isomorphisms $b_t:\mathcal{P}{M}_t\to B_t$ recursively. At a nonunit leaf use the identity, and at a unit leaf use ${\alpha }_Z$. At an internal node with children $l,r$, set $M_t=T(\mathcal{P}{M}_l,\mathcal{P}{M}_r)$, $e_t=T(b_l,b_r):M_t\to B_t$ and $b_t=e_t{\alpha }_{M_t}$. Both tensor factors of the source and target are K-flat, so [F10] makes $e_t$ a quasi-isomorphism; then $b_t$ is one too. Naturality of $\alpha$ and of the ordinary structure maps makes the comparisons $Q(e_t)$ intertwine each derived associator or symmetry with the corresponding ordinary one: at a binary reassociation these are precisely the $\mathrm{\Theta },\mathrm{\Xi }$ squares of step 2.1, and the same squares at an internal node extend the equality recursively. For the unit triangle, insert ${\alpha }_Z$ in the middle factor. Naturality of $A$ then reduces the two routes to the ordinary identity $T(\mathrm{id},\mathrm{\Lambda }(\mathcal{P}\mathcal{G}))A(\mathcal{P}\mathcal{F},Z,\mathcal{P}\mathcal{G})=T(\mathrm{P}(\mathcal{P}\mathcal{F}),\mathrm{id}),$ precomposed with $T(T(\mathrm{id},{\alpha }_Z),\mathrm{id})$; the remaining augmentations are exactly those in the definitions of ${\lambda }^{\mathbf{L}},{\rho }^{\mathbf{L}}$, and commute by their naturality. Consequently each derived pentagon, triangle and hexagon is conjugate by the invertible comparisons to an ordinary coherence diagram of [F6], so both routes agree. Involutivity likewise reduces to $S^2=1$.

Let $u:{\mathcal{F}}^{\bullet }\to {\mathcal{F}}^{\mathrm{\prime }\bullet }$ be a morphism of $D^{-}$ represented by a left roof $(s:\mathcal{V}\to \mathcal{F},h:\mathcal{V}\to {\mathcal{F}}^{\mathrm{\prime }})$ with $s$ a quasi-isomorphism [F13, F14]. Bifunctoriality [F3] gives $((u{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}})=((h{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}})\circ ((s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}}{)}^{-1}$ and $u{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}}=(h{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}})\circ (s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}}{)}^{-1}$, the inverse factors being invertible because $s$ is a quasi-isomorphism [F3, F9]. Applying [step 2.1] to the cochain maps $h$ and $s$ gives ${\alpha }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }},\mathcal{G},\mathcal{H})\circ ((h{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}})=(h{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}})\circ {\alpha }^{\mathbf{L}}(\mathcal{V},\mathcal{G},\mathcal{H})$ and ${\alpha }^{\mathbf{L}}(\mathcal{F},\mathcal{G},\mathcal{H})\circ ((s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}})=(s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}})\circ {\alpha }^{\mathbf{L}}(\mathcal{V},\mathcal{G},\mathcal{H})$, and the second inverts to ${\alpha }^{\mathbf{L}}(\mathcal{V},\mathcal{G},\mathcal{H})\circ ((s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}}{)}^{-1}=(s{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}}{)}^{-1}\circ {\alpha }^{\mathbf{L}}(\mathcal{F},\mathcal{G},\mathcal{H})$. Substituting these into the composite proves ${\alpha }^{\mathbf{L}}({\mathcal{F}}^{\mathrm{\prime }},\mathcal{G},\mathcal{H})\circ ((u{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}}){\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{H}})=(u{\otimes }^{\mathbf{L}}{\mathrm{id}}_{\mathcal{G}{\otimes }^{\mathbf{L}}\mathcal{H}})\circ {\alpha }^{\mathbf{L}}(\mathcal{F},\mathcal{G},\mathcal{H})$, so ${\alpha }^{\mathbf{L}}$ is natural in the first variable; the other two variables are identical computations, and clause 3 follows with [step 1.6].

Clause 1 is [step 1.1] with [step 1.2] and [step 2.3]; clause 2 is [step 1.3], [step 1.4], [step 2.4], [step 1.5] and [step 2.5]; clause 3 is [step 1.6] with [step 2.1] and [step 3.2]; clause 4(a) is [step 3.1], clause 4(b) is [step 1.7] and [step 2.2], and clause 4(c) is [step 1.8]. No choice principle is used: the canonical replacement and its augmentation are choice-free [F1, F12], the structure maps $A,S,\mathrm{\Lambda },\mathrm{P}$ and $\alpha ,\sigma ,\lambda ,\rho$ are the published canonical maps [F5, F6, F7, F8], and every morphism above is a composite of these with the localization functor [F9]. ∎