Ramification theory from homotopical point of view, I

We prove the compatibility of pushforward along a proper morphism of an '{e}tale constructible sheaf and the pushforward of its characteristic cycle up to $p$-torsion. This was conjectured by Takeshi Saito. For this, we revisit the construction of the characteristic cycle, due to Saito and Beilinson, from more homotopical point of view. In particular, the language of $\mathrm{\infty }$-categories is indispensable to carry this out.