Galois stratification and ACFA

We prove a direct image theorem stating that the direct image of a Galois formula by a morphism of difference schemes is equivalent to a Galois formula modulo the theory ACFA of existentially closed difference fields. As a consequence, we obtain an effective quantifier elimination procedure and a precise algebraic-geometric description of definable sets over existentially closed difference fields in terms of twisted Galois formulae associated with finite Galois difference ring/scheme covers.