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 (TODO, @chrisflav).

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 {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