A result in positive characteristic is that if $R/\mathbb{F}_p$ is a smooth ring, then we have a Cartier isomorphism $$\Omega_{R}^\bullet\cong H^\bullet(\Omega_R^\bullet)$$ which is essentially extracted from the Frobenius. I'm curious what happens when we loosen the finiteness condition, and say consider formally smooth $\mathbb{F}_p$-algebras. The sort of base case for this would be the case of a polynomial algebra in say countably many variables $\mathbb{F}_p[x_1,\ldots]$. I think (unless I'm making an embarrasing mistake) that it is true there for two reasons: either an explicit computation or using the fact that $\mathbb{F}_p[x_1,\ldots]\cong \text{colim}_n \mathbb{F}_p[x_1,\ldots,x_n]$, and that both $\Omega_{(-)}$ and $H^\bullet(-)$ commute with filtered colimits to bootstrap the smooth case.
Does that argument hold up? (I'm concerned bc I haven't seen it mentioned, so presumably I'm missing something here). Is there a more general version of the Cariter isomorphism with weaker finiteness conditions?
