This question is a follow up to my previous [question](https://mathoverflow.net/questions/444168/reference-request-on-rings-of-crystalline-differential-operators) on rings of crystaline differential operators, to which I refer for the adequate definitions.

First, let's consider the case of an algebraically closed field of zero characteristic $\mathsf{k}$ and usual rings of differential operators (denoted here by $\mathcal{D}(\cdot)$) All varieties are irreducible.

Let $X$ be an affine smooth variety and $A=\mathcal{O}(X)$ its ring of regular functions. $\mathcal{D}(X)$ and $\mathcal{D}(A)$ mean the samething.

One of the most useful basic facts about rings of differential operators, and which allows us to sheafify, is following:

Proposition 1: Let $S$ be a multiplicatively closed subset of $A$. Then left and right localization of $\mathcal{D}(A)$ by $S$ exists and $\mathcal{D}(A)S^{-1}=S^{-1}\mathcal{D}(A)=\mathcal{D}(AS^{-1})$.

The next result I am going to recall is much more deep. It usually is treated as a folklore, and hence I am not sure about who was the first one to prove it, but its proof appears in print only in a paper of Cannings and Holland.

Theorem 1: Let $G$ be a finite group acting freely on a smooth affine variety $X$. Then $\mathcal{D}(X)^G \simeq \mathcal{D}(X/G)$.

Now we move to crystaline rings of differential operators. Now $\mathsf{k}$ has prime characteristic, and I denote the ring of crystalline differential operators by $\mathcal{D}_c(\cdot)$.

I was reading the following [paper](https://www.sciencedirect.com/science/article/pii/S0001870821006009) by Tikaradze, and in the proof of Lemma 0.2 it seems to me that he uses implictly the following 'crystalline' analogues of the above proposition and theorem:

Proposition 1*: Let $X$ and $Y$ be two smooth affine varieties such that the function fields $\mathsf{k}(X)$ and $\mathcal{k}(Y)$ are isomorphic. Then $\operatorname{Frac}(\mathcal{D}_c(X)) \simeq \operatorname{Frac}(\mathcal{D}_c(Y))$, where $\operatorname{Frac}$ denotes the skew field of fractions an Ore domain.

Theorem 1*: Let $X$ be an smooth affine variety and $G$ a finite group acting freely on it. Then $\mathcal{D}_c(X)^G \simeq \mathcal{D}_c(X/G)$.

The main reference I know of about rings of crystalline differential operators is Roman Bezrukavnikov, Ivan Mirković, Dmitriy Rumynin: "*Localization of modules for a semisimple Lie algebra in prime characteristic*". In this paper the authors shows that $\mathcal{D}_c(\cdot)$ sheafifies, and hence I think that the above Proposition 1* is more or less a direct consequence of this. I am correct, or should I look for a proof for Proposition 1*?

Things are different in regarding Theorem 1*. It definitely does not follow form what is done in the paper by Bezrukavnikov, Mirković and Rumynin. Hence I am looking for a proof of this fact - I couldn't find any.

Justification for this question: I am writing a short paper where I pretend to use Proposition 1* and Theorem 1*, and I would like to include adequate proofs/references for these statements.