Coherent derived tensor and pullback on perfect complexes

Locally represent $E$ and $F$ by bounded finite locally free complexes. Their derived tensor is computed by their ordinary total tensor there, because these bounded flat complexes are K-flat. It is again bounded finite locally free: each degree is a finite direct sum of tensor products of finite locally free sheaves. The unit ${\mathcal{O}}_X$ has this form. The full perfect subfamily in [F1] already retains these tensor coherences; the local computation identifies its fibers with precisely the perfect condition of [F2].

Tensoring K-flat representatives commutes with the signed mapping-cone matrices and takes zero to zero. Consequently its derived operation preserves cofiber sequences in each variable and is exact in the stable categories. The finite stable operations of $\mathrm{Perf}$ are ambient ones, so this exactness restricts to $\mathrm{Perf}$.

Given $E\in \mathrm{Perf}(Y)$, choose around $f(x)$ a bounded finite locally free presentation and restrict to its inverse-image neighbourhood of $x$. The derived pullback there is computed by ordinary pullback of that bounded flat presentation and is again bounded finite locally free, since pullback sends finite free local charts to finite free charts. Thus $L{f}^{\ast }$ preserves $\mathrm{Perf}$. Exactness and the strong monoidal and compositional coherences come from the single localized cocartesian family in [F1], not from transport between independently chosen pointwise functors.

For any ring map $A\to B$ and a bounded finite-projective $A$-complex $P$, $B{\otimes }_{A}P$ computes $B{\otimes }_A^{L}P$ because $P$ is bounded projective. Its terms are finite projective over $B$: a finite free-summand presentation remains a summand after tensor. Sheaf pullback of its associated sheaf is the associated sheaf of $B{\otimes }_{A}P$, naturally with the signed differentials. Under the actual affine fiber comparison [F3], this is the scalar-extension calculation: both operations on the bounded projective representative are literally sheaf pullback of that associated-sheaf complex. Both affine schemes are qcqs, so this verifies the affine specialization of the common-family functor for every such ring map, without asserting a natural equivalence of independently specified diagrams. Hence the enhanced pullback specializes to derived scalar extension and all assertions follow.