A crystalline incarnation of Berthelot's conjecture and Künneth formula for isocrystals
Berthelot's conjecture predicts that under a proper and smooth morphism of schemes in characteristic , the higher direct images of an overconvergent -isocrystal are overconvergent -isocrystals. In this paper we prove that this is true for crystals up to isogeny. As an application we prove a Künneth formula for the crystalline fundamental group.