Analytic rings in the light setting

In the original definition of analytic rings, this was defined in the “non-light” setting. In this case, there is an additional condition one needs to put: the Frobenius map \(A \to A/p\) is a map of analytic rings for every prime \(p\). In the light setting, this condition turns out to be automatic. (It is not known whether this condition is automatic in the “non-light” setting.)