Totally split algebras

An R-algebra S is finite (totally) split if it is isomorphic to Fin n → R for some n. Geometrically, this corresponds to a trivial covering.

Every totally split algebra is finite étale and conversely, every finite étale covering is étale locally totally split.

Main results

• Algebra.IsFiniteSplit.exists_tensorProduct_of_etale: If S is finite étale over R of some constant rank, there exists a faithfully flat, finite étale R-algebra T such that T ⊗[R] S is finite split.

class Algebra.IsFiniteSplit (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Prop

S is a finite, totally split R-algebra if S is isomorphic to Fin n → R for some n. Geometrically, this is a trivial cover of degree n.

• nonempty_algEquiv_fun : ∃ (n : ℕ), Nonempty (S ≃ₐ[R] Fin n → R)

instance Algebra.IsFiniteSplit.instTensorProduct {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_3} [CommRing T] [Algebra R T] [IsFiniteSplit R S] : IsFiniteSplit T (TensorProduct R T S)

instance Algebra.IsFiniteSplit.instForallOfFinite {R : Type u_1} [CommRing R] {ι : Type u_3} [Finite ι] : IsFiniteSplit R (ι → R)

theorem Algebra.IsFiniteSplit.of_algEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {S' : Type u_3} [CommRing S'] [Algebra R S'] (e : S ≃ₐ[R] S') [IsFiniteSplit R S] : IsFiniteSplit R S'

instance Algebra.IsFiniteSplit.inst {R : Type u_1} [CommRing R] : IsFiniteSplit R R

theorem Algebra.IsFiniteSplit.of_subsingleton_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Subsingleton S] : IsFiniteSplit R S

theorem Algebra.IsFiniteSplit.of_subsingleton {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Subsingleton R] : IsFiniteSplit R S

instance Algebra.IsFiniteSplit.instFree {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFiniteSplit R S] : Module.Free R S

instance Algebra.IsFiniteSplit.instFinitePresentation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFiniteSplit R S] : Module.FinitePresentation R S

instance Algebra.IsFiniteSplit.instEtale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFiniteSplit R S] : Etale R S

theorem Algebra.IsFiniteSplit.exists_tensorProduct_of_etale {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Etale R S] [Module.Finite R S] {n : ℕ} (hn : Module.rankAtStalk S = ↑n) : ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (TensorProduct R T S)

If S is finite étale over R of (constant) rank n, there exists a finite faithfully flat, étale R-algebra T such that T ⊗[R] S is split of rank n over T. This is the commutative algebra version of Lenstra, Galois theory for schemes, 5.10.