Finitely many homomorphisms out of a finite-type algebra into a finite algebra

An algebra homomorphism out of a finitely generated R-algebra A is determined by its values on a finite generating set. So when the target B is finite there are only finitely many of them. Applied to the coordinate algebra of an affine scheme of finite type over a finite field 𝔽_q, this says that the scheme has finitely many 𝔽_q-points, and more generally finitely many points over any finite 𝔽_q-algebra.

Main declarations

• Algebra.FiniteType.finite_algHom: A →ₐ[R] B is finite when A is of finite type over R and B is finite.

instance Algebra.FiniteType.finite_algHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [FiniteType R A] [Finite B] : Finite (A →ₐ[R] B)

A finite-type algebra has finitely many homomorphisms into a finite algebra: such a homomorphism is determined by its values on a finite generating set.