Totally split algebras over a totally split algebra

Let K be a field and A → B a map of totally split K-algebras (Algebra.IsFiniteSplit), with B flat over A. Geometrically, Spec B → Spec A is a finite flat morphism between finite disjoint unions of copies of Spec K. Above every K-point χ of A there are exactly as many K-points of B as the rank of B at the prime ker χ: the fibre K ⊗[A] B is a quotient of B, hence totally split, so its points are counted by its dimension.

When this rank is a constant d, the points of B are labelled by pairs of a point of A and an index in Fin d, compatibly with the projection to the points of A, and B is the trivial cover Fin d → A of A. Here flatness is automatic, since A is a semisimple ring. This splits a finite flat cover of constant rank of a finite étale scheme over a field once both schemes are split over the base field, for instance the branches of a nodal curve over its nodes.

Main results

• Algebra.IsFiniteSplit.card_algHom_comp_eq_rankAtStalk: the number of points of B above a point χ of A is the rank of B at ker χ.
• Algebra.IsFiniteSplit.nonempty_algEquiv_fun_of_rankAtStalk_eq: if B has constant rank d over A, then B ≃ₐ[A] (Fin d → A).

theorem Algebra.IsFiniteSplit.card_algHom_comp_eq_rankAtStalk {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] [Algebra A B] [IsScalarTower K A B] [IsFiniteSplit K B] [Module.Flat A B] (χ : A →ₐ[K] K) : Nat.card { ψ : B →ₐ[K] K // ψ.comp (IsScalarTower.toAlgHom K A B) = χ } = Module.rankAtStalk B { asIdeal := RingHom.ker χ, isPrime := ⋯ }

The points of a totally split algebra above a point of its base number its rank there. If B is a totally split K-algebra, flat over the K-algebra A, then the K-points of B restricting to a K-point χ of A are as many as the rank of B at the prime ker χ of A.

theorem Algebra.IsFiniteSplit.nonempty_algEquiv_fun_of_rankAtStalk_eq {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] [Algebra A B] [IsScalarTower K A B] [IsFiniteSplit K A] [IsFiniteSplit K B] {d : ℕ} (hd : ∀ (p : PrimeSpectrum A), Module.rankAtStalk B p = d) : Nonempty (B ≃ₐ[A] Fin d → A)

A totally split algebra of constant rank over a totally split algebra is a trivial cover. Let A and B be totally split algebras over a field K, with B an A-algebra of constant rank d. Then B is A-isomorphic to Fin d → A: the K-points of B are labelled by pairs of a K-point of A below them and an index in Fin d. No flatness hypothesis is needed: A is a finite product of copies of K, a semisimple ring, over which every module is flat.