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_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_4} [CommRing T] [Algebra R T] [IsFiniteSplit R S] : IsFiniteSplit T (TensorProduct R T S)

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

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

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

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

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

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

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

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

theorem Algebra.IsFiniteSplit.bijective_algebraMap_quotient (k : Type u_1) {R : Type u_2} [Field k] [CommRing R] [Algebra k R] [IsFiniteSplit k R] (p : Ideal R) [p.IsPrime] : Function.Bijective ⇑(algebraMap k (R ⧸ p))

noncomputable def Algebra.IsFiniteSplit.algHomEquivPrimeSpectrum (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [Algebra k R] [IsFiniteSplit k R] : (R →ₐ[k] k) ≃ PrimeSpectrum R

If R is finite split over a field k, the k-rational points of R are in one-to-one correspondence with its prime spectrum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.IsFiniteSplit.coe_algHomEquivPrimeSpectrum {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] [IsFiniteSplit k R] (f : R →ₐ[k] k) : ((algHomEquivPrimeSpectrum k R) f).asIdeal = RingHom.ker f

instance Algebra.IsFiniteSplit.instOfIsSepClosedOfEssFiniteTypeOfFormallyEtale {k : Type u_1} {R : Type u_2} [Field k] [CommRing R] [Algebra k R] [IsSepClosed k] [EssFiniteType k R] [FormallyEtale k R] : IsFiniteSplit k R

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.