An arithmetic étale-crystalline comparison with coefficients in crystalline local systems

We use the stacky approach to $p$-adic cohomology theories recently developed by Drinfeld and Bhatt–Lurie to generalise a comparison theorem between the rational crystalline cohomology of the special fibre and the rational $p$-adic étale cohomology of the arithmetic generic fibre of any proper $p$-adic formal scheme $X$ due to Colmez–Niziol to the case of coefficients in an arbitrary crystalline local system on the generic fibre of $X$. In the process, we establish a version of the Beilinson fibre square of Antieau–Mathew–Morrow–Nikolaus with coefficients in the proper case and prove a comparison between syntomic cohomology and $p$-adic étale cohomology with coefficients in an arbitrary $F$-gauge. Our methods also yield a description of the isogeny category of perfect $F$-gauges on ${\mathbb{Z}}_p$.