Finite algebras over a field with many characters are totally split

A finite-dimensional commutative algebra A over a field K has at most finrank K A characters A →ₐ[K] K (Mathlib's card_algHom_le_finrank). When it has that many, evaluation at the characters identifies A with the algebra of K-valued functions on them (TauCeti.AlgHom.pi_id_bijective_of_finrank_le_card), so A is totally split (Algebra.IsFiniteSplit), and in particular étale over K. Conversely, a totally split algebra has exactly finrank K A characters (Algebra.IsFiniteSplit.card_algHom_eq_finrank) and is the algebra of functions on them (Algebra.IsFiniteSplit.pi_id_bijective).

Geometrically: a finite scheme over a field with as many rational points as its degree is a disjoint union of copies of the base. This is the criterion used to show that the n-torsion of an elliptic curve over a separably closed field in which n is invertible is étale.

Main results

• Algebra.IsFiniteSplit.of_finrank_le_card_algHom: a finite-dimensional commutative algebra over a field with at least finrank K A characters is totally split.
• Algebra.IsFiniteSplit.card_algHom_eq_finrank: a totally split algebra has exactly finrank K A characters.
• Algebra.IsFiniteSplit.pi_id_bijective: evaluation at all characters identifies a totally split algebra over a field with the algebra of functions on its characters.

theorem Algebra.IsFiniteSplit.of_finrank_le_card_algHom {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] [Module.Finite K A] (h : Module.finrank K A ≤ Nat.card (A →ₐ[K] K)) : IsFiniteSplit K A

A finite algebra over a field with as many characters as its dimension is totally split. If a finite-dimensional commutative algebra A over a field K has at least finrank K A characters A →ₐ[K] K, then A is isomorphic to a finite product of copies of K; in particular it is étale over K.

theorem Algebra.IsFiniteSplit.card_algHom_eq_finrank {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] [IsFiniteSplit K A] : Nat.card (A →ₐ[K] K) = Module.finrank K A

A totally split algebra has as many characters as its dimension. If A is isomorphic to a finite product of copies of the field K, then it has exactly finrank K A characters A →ₐ[K] K.

theorem Algebra.IsFiniteSplit.pi_id_bijective {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] [IsFiniteSplit K A] : Function.Bijective ⇑(AlgHom.pi fun (χ : A →ₐ[K] K) => χ)

A totally split algebra is the algebra of functions on its characters. If A is isomorphic to a finite product of copies of the field K, then evaluation at all characters A →ₐ[K] K is an isomorphism from A onto the algebra of K-valued functions on them.