Frobenius line invariance of algebraic 𝐾-theory

The K K -theory of smooth schemes is A 1 \mathbf {A}^{1} -invariant. We show that this remains true over finite fields if one replaces the affine line by the Frobenius line, i.e., the non-commutative algebra where multiplication with the variable behaves like the Frobenius. Emerton had shown that over regular rings the Frobenius line is left coherent. As a technical ingredient for our theorem, but also of independent interest, we extend this and show that merely assuming finite type (or just F F -finite), the Frobenius line is right coherent.