Endomorphisms whose square is a power map

If a ring endomorphism squares to a positive power map, it is integral and induces an involution on the prime spectrum. For an endomorphism of a finitely generated algebra, integrality implies finiteness. These criteria apply in particular to square roots of Frobenius, without requiring the ring to be reduced.

theorem RingHom.isIntegral_of_comp_self_eq_pow {A : Type u_1} [CommRing A] (f : A →+* A) {n : ℕ} (hn : 0 < n) (hf : ∀ (x : A), f (f x) = x ^ n) : f.IsIntegral

An endomorphism whose square is a positive power map is integral.

theorem RingHom.comap_involutive_of_comp_self_eq_pow {A : Type u_1} [CommSemiring A] (f : A →+* A) {n : ℕ} (hn : 0 < n) (hf : ∀ (x : A), f (f x) = x ^ n) : Function.Involutive (PrimeSpectrum.comap f)

An endomorphism whose square is a positive power map induces an involution on prime ideals. This includes nonreduced rings: prime ideals detect membership of positive powers.

theorem AlgHom.finite_of_comp_self_eq_pow {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Algebra.FiniteType R A] (f : A →ₐ[R] A) {n : ℕ} (hn : 0 < n) (hf : ∀ (x : A), f (f x) = x ^ n) : f.Finite

A square root of a positive power map on a finite-type algebra is a finite morphism. No field or characteristic hypothesis is needed.