On log crystalline higher direct image

We define the big crystalline site for a log scheme and prove the basic properties. In particular, we show the boundedness, base change, and perfectness theorems for the crystalline higher direct image of quasi-coherent crystals between fine log schemes. We also introduce the big absolute crystalline sites and discuss the Frobenius isogeny property of the crystalline higher direct image of $F$-isocrystals.