Overholonomicity of overconvergent \(F\)-isocrystals over smooth varieties (Q456663)

From the introduction: ``Let [...] \(k\) be a perfect residue field of characteristic \(p>0\) [...] In order to define a good category of \(p\)-adic coefficients over \(k\)-varieties stable under cohomological operations, Berthelot introduced the notion of arithmetic \({\mathcal D}\)-modules and their cohomological operations. [...] Also, he defined holonomic \(F\)-complexes of arithmetic \({\mathcal D}\)-modules. Virrion checked the stability of holonomicity under the dual functor. Berthelot conjectured its stability under the other Grothendieck operations. [...] In order to avoid these conjectures and to get a category of \(F\)-complexes of arithmetic \({\mathcal D}\)-modules that satisfies these stability conditions, the first step was to introduce the notion of overcoherence [...] To improve the stability properties, we defined the category of overholonomic \(F\)-complexes over \(k\)-varieties [...] We got the stability of overholonomicity by direct images, extraordinary direct images, extraordinary inverse images, and inverse images. Moreover, it is already known that this category of \(p\)-adic coefficients is not zero since it contains unit-root overconvergent \(F\)-isocrystals [...] Now it remains to check the stability of overholonomicity by (internal and external) tensor products. The second step [...] established that \(F\)-complexes dévissable in overconvergent \(F\)-isocrystals are stable under tensor products. The third step is to prove that the notions (still with Frobenius structure) of overcoherence, overholonomicity and d{e}vissability in overconvergent \(F\)-isocrystals are identical. With what we have proved in the first and second steps, the equality between the overholonomicity and d{e}vissability in overconvergent \(F\)-isocrystals implies that the overholonomicity is stable under Grothendieck's aforesaid six cohomological operations.'' The purpose of the present paper is to perform this indicated third step. For this, the decisive geometric input needed is Kedlaya's semistable reduction theorem [K. Kedlaya, Semistable reduction for overconvergent \(F\)-isocrystals, I, II, III, IV]. From the introduction: ''The technical key point is a comparison theorem between the relative logarithmic rigid cohomology and rigid cohomology [...] This fundamental key point was checked by the second author, and the fact that this implies the overholonomicity of log-extendable overconvergent \(F\)-isocrystals was checked by the first one.'' It should be mentioned that, besides arithmetic \({\mathcal D}\)-modules themselves, also various other basic constructions originally introduced by Berthelot (e.g. quasi coherence on formal schemes, modified here as quasi coherence on formal log-schemes) play an important role here.