Rings without nonsplit finite étale covers

A finite étale R-algebra T is totally split (TauCeti.Algebra.IsTotallySplit) if T ≃ₐ[R] ∏_{j < m} R ⧸ (1 - e_j) for finitely many idempotents e_j of R. Geometrically, Spec T → Spec R is a disjoint union of finitely many clopen subsets of Spec R, so its rank may vary over the components of Spec R; Mathlib's Algebra.IsFiniteSplit is the constant-rank case T ≃ₐ[R] (Fin n → R) (TauCeti.Algebra.IsTotallySplit.of_isFiniteSplit). A ring R has no nonsplit finite étale covers (TauCeti.IsFiniteEtaleSplit) if every finite étale R-algebra is totally split. No topology is involved, and the zero ring is allowed.

This is the conclusion of Scholze's Lemma 15.3 for the perfectoid tower A_∞, and it is used there only through sections of faithfully flat covers and roots of separable polynomials.

Main results

• TauCeti.Algebra.IsTotallySplit.quotient_span_singleton: a quotient of a totally split algebra by an idempotent is totally split.
• TauCeti.Algebra.IsTotallySplit.nonempty_algHom_of_faithfulSMul: a totally split algebra with injective structure map, for example a faithfully flat one, has a section.
• TauCeti.isFiniteEtaleSplit_iff_exists_section: R has no nonsplit finite étale covers if and only if every faithfully flat finite étale R-algebra admits an R-algebra map to R.
• TauCeti.IsFiniteEtaleSplit.exists_root: over such a ring, every monic polynomial of positive degree whose derivative is a unit modulo it has a root.
• TauCeti.isFiniteEtaleSplit_iff_isSepClosed: a field has no nonsplit finite étale covers if and only if it is separably closed.
• TauCeti.IsFiniteEtaleSplit.of_isSepClosed: the instance for separably closed fields.
• TauCeti.Algebra.IsTotallySplit.isFiniteSplit, Algebra.IsFiniteSplit.of_isFiniteEtaleSplit: over a ring with preconnected spectrum, a totally split algebra, and so every finite étale algebra over a ring without nonsplit finite étale covers, is R-isomorphic to Fin n → R.
• TauCeti.Algebra.IsTotallySplit.baseChange: total splitting is stable under base change.
• Algebra.IsFiniteSplit.of_surjective: over a field, a quotient of a totally split algebra is totally split.
• TauCeti.IsFiniteEtaleSplit.nonempty_algHom: a faithfully flat finite étale R-algebra maps to every R-algebra without nonsplit finite étale covers.
• TauCeti.IsFiniteEtaleSplit.pi, TauCeti.IsFiniteEtaleSplit.prod: products of rings without nonsplit finite étale covers have none.
• TauCeti.isFiniteEtaleSplit_iff_of_full_of_essSurj: the condition is invariant under a ring map along which base change CommAlgCat.FiniteEtale.baseChange is full and essentially surjective (e.g. an equivalence of categories).
• RingEquiv.isFiniteEtaleSplit: the condition is invariant under ring isomorphisms.

Implementation notes

The section criterion is proved by induction on an upper bound of the rank of T, which is a locally constant function on Spec R. The support of T is cut out by an idempotent e₀, and T × R ⧸ (e₀) is faithfully flat. Its section splits off a copy of R, leaving a cover of smaller rank; T is recovered from the result as a quotient by an idempotent.

References

• P. Scholze, Étale cohomology of diamonds, Lemma 15.3.
• P. Scholze and J. Weinstein, Berkeley lectures on p-adic geometry, Lemma 10.1.6.

def TauCeti.Algebra.IsTotallySplit (R : Type u_1) (T : Type u_2) [CommRing R] [CommRing T] [Algebra R T] : Prop

An R-algebra T is totally split if T ≃ₐ[R] ∏_{j < m} R ⧸ (1 - e_j) for finitely many idempotents e_j of R (repetitions and zeros allowed). Mathlib's Algebra.IsFiniteSplit is the case where every e_j is 1; in general the number of sheets may vary over the clopen components of Spec R.

theorem TauCeti.Algebra.isTotallySplit_iff {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] : IsTotallySplit R T ↔ ∃ (m : ℕ) (e : Fin m → R), (∀ (j : Fin m), IsIdempotentElem (e j)) ∧ Nonempty (T ≃ₐ[R] (j : Fin m) → R ⧸ Ideal.span {1 - e j})

Unfolding lemma for IsTotallySplit: it recovers the idempotents and the algebra isomorphism in modules where the body of the definition is not exposed.

theorem TauCeti.Algebra.IsTotallySplit.of_algEquiv_pi {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] {ι : Type u_3} [Finite ι] (e : ι → R) (he : ∀ (i : ι), IsIdempotentElem (e i)) (φ : T ≃ₐ[R] (i : ι) → R ⧸ Ideal.span {1 - e i}) : IsTotallySplit R T

A product of quotients by idempotents indexed by any finite type is totally split.

theorem TauCeti.Algebra.IsTotallySplit.of_algEquiv {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] {T' : Type u_3} [CommRing T'] [Algebra R T'] (h : IsTotallySplit R T) (φ : T ≃ₐ[R] T') : IsTotallySplit R T'

Total splitting is invariant under isomorphism of algebras.

theorem TauCeti.Algebra.IsTotallySplit.of_isFiniteSplit {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] [Algebra.IsFiniteSplit R T] : IsTotallySplit R T

An algebra of constant split rank is totally split, with every idempotent equal to 1.

theorem TauCeti.Algebra.IsTotallySplit.of_subsingleton (R : Type u_1) (T : Type u_2) [CommRing R] [CommRing T] [Algebra R T] [Subsingleton T] : IsTotallySplit R T

The zero algebra, and more generally any subsingleton algebra, is totally split: it is the empty product.

theorem TauCeti.Algebra.IsTotallySplit.self (R : Type u_1) [CommRing R] : IsTotallySplit R R

The base ring is totally split over itself, with one sheet.

theorem TauCeti.Algebra.IsTotallySplit.prod {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (hA : IsTotallySplit R A) (hB : IsTotallySplit R B) : IsTotallySplit R (A × B)

A product of two totally split algebras is totally split.

theorem TauCeti.Algebra.IsTotallySplit.quotient_span_singleton {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] (h : IsTotallySplit R T) {ε : T} (hε : IsIdempotentElem ε) : IsTotallySplit R (T ⧸ Ideal.span {ε})

A quotient of a totally split algebra by an idempotent, that is, a direct factor of it, is totally split.

theorem TauCeti.Algebra.IsTotallySplit.of_prod_fst {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (h : IsTotallySplit R (A × B)) : IsTotallySplit R A

A factor of a totally split product is totally split: A is the quotient of A × B by the idempotent (0, 1).

theorem TauCeti.Algebra.IsTotallySplit.of_prod_snd {R : Type u_1} [CommRing R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (h : IsTotallySplit R (A × B)) : IsTotallySplit R B

The second factor of a totally split product is totally split: swap the factors and apply of_prod_fst.

theorem TauCeti.Algebra.IsTotallySplit.nonempty_algHom_of_faithfulSMul {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] (h : IsTotallySplit R T) [FaithfulSMul R T] : Nonempty (T →ₐ[R] R)

A totally split algebra with injective structure map, for example a faithfully flat one, has a section: injectivity says that the components D(e j) cover Spec R, and a section is assembled from an orthogonal refinement of this cover.

theorem TauCeti.Algebra.IsTotallySplit.etale {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] (h : IsTotallySplit R T) : Algebra.Etale R T

A totally split algebra is étale.

theorem TauCeti.Algebra.IsTotallySplit.finite {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] (h : IsTotallySplit R T) : Module.Finite R T

A totally split algebra is finite.

theorem TauCeti.Algebra.IsTotallySplit.isFiniteSplit {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] [PreconnectedSpace (PrimeSpectrum R)] (h : IsTotallySplit R T) : Algebra.IsFiniteSplit R T

Over a ring with preconnected prime spectrum, for example a local ring, a totally split algebra has constant split rank: every idempotent e_j is 0 or 1, so each factor R ⧸ (1 - e_j) is a copy of R or the zero ring.

theorem TauCeti.Algebra.IsTotallySplit.baseChange {R : Type u_1} {T : Type u_2} [CommRing R] [CommRing T] [Algebra R T] (S : Type u_3) [CommRing S] [Algebra R S] (h : IsTotallySplit R T) : IsTotallySplit S (TensorProduct R S T)

Total splitting is stable under base change: if T ≃ₐ[R] ∏ R ⧸ (1 - e_j), then S ⊗[R] T ≃ₐ[S] ∏ S ⧸ (1 - e_j), with the images of the same idempotents.

theorem Algebra.IsFiniteSplit.of_surjective {K : Type u_1} {B : Type u_2} {C : Type u_3} [Field K] [CommRing B] [CommRing C] [Algebra K B] [Algebra K C] [IsFiniteSplit K B] (g : B →ₐ[K] C) (hg : Function.Surjective ⇑g) : IsFiniteSplit K C

A quotient of a totally split algebra over a field is totally split. If B is K-isomorphic to Fin m → K and g : B →ₐ[K] C is surjective, then C is K-isomorphic to Fin n → K for some n: every ideal of Fin m → K is generated by an idempotent, so C is a direct factor of B. Geometrically, a closed subscheme of a finite disjoint union of copies of Spec K is again one.

class TauCeti.IsFiniteEtaleSplit (R : Type u) [CommRing R] : Prop

A ring R has no nonsplit finite étale covers if every finite étale R-algebra is totally split. This is the conclusion of Scholze's Lemma 15.3 for the perfectoid tower A_∞.

• isTotallySplit (T : Type u) [CommRing T] [Algebra R T] [Algebra.Etale R T] [Module.Finite R T] : Algebra.IsTotallySplit R T

  Every finite étale R-algebra is totally split.

@[instance 100]

instance TauCeti.IsFiniteEtaleSplit.of_subsingleton {R : Type u} [CommRing R] [Subsingleton R] : IsFiniteEtaleSplit R

The zero ring has no nonsplit finite étale covers: every algebra over it is the empty product.

theorem TauCeti.isFiniteEtaleSplit_iff_exists_section {R : Type u} [CommRing R] : IsFiniteEtaleSplit R ↔ ∀ (T : Type u) [inst : CommRing T] [inst_1 : Algebra R T] [Algebra.Etale R T] [Module.Finite R T] [Module.FaithfullyFlat R T], Nonempty (T →ₐ[R] R)

A ring has no nonsplit finite étale covers if and only if every faithfully flat finite étale algebra over it admits a section. Faithful flatness is needed: over a nonzero ring the zero algebra is finite étale and totally split, but has no section.

theorem TauCeti.IsFiniteEtaleSplit.exists_root {R : Type u} [CommRing R] [IsFiniteEtaleSplit R] {P : Polynomial R} (hP : P.Monic) (hd : 0 < P.natDegree) (hu : IsUnit ((AdjoinRoot.mk P) (Polynomial.derivative P))) : ∃ (r : R), P.IsRoot r

Over a ring without nonsplit finite étale covers, every monic polynomial of positive degree whose derivative is a unit modulo it, that is, every separable one (Polynomial.separable_iff_isUnit_mk_derivative), has a root: R[X] ⧸ (P) is finite étale and free of positive rank, so it has a section.

instance TauCeti.IsFiniteEtaleSplit.of_isSepClosed (K : Type u) [Field K] [IsSepClosed K] : IsFiniteEtaleSplit K

A separably closed field has no nonsplit finite étale covers: every finite étale algebra over it has constant split rank.

theorem TauCeti.isFiniteEtaleSplit_iff_isSepClosed (K : Type u) [Field K] : IsFiniteEtaleSplit K ↔ IsSepClosed K

A field has no nonsplit finite étale covers if and only if it is separably closed.

theorem TauCeti.Algebra.IsTotallySplit.of_isFiniteEtaleSplit {R : Type u} [CommRing R] [IsFiniteEtaleSplit R] (T : Type u_1) [CommRing T] [Algebra R T] [Algebra.Etale R T] [Module.Finite R T] : IsTotallySplit R T

Over a ring without nonsplit finite étale covers, a finite étale algebra in any universe is totally split. The defining property of IsFiniteEtaleSplit R only quantifies over algebras in the universe of R; a finite algebra is small over R, so it applies to an isomorphic copy.

theorem Algebra.IsFiniteSplit.of_isFiniteEtaleSplit {R : Type u} [CommRing R] [TauCeti.IsFiniteEtaleSplit R] [PreconnectedSpace (PrimeSpectrum R)] (T : Type u_1) [CommRing T] [Algebra R T] [Etale R T] [Module.Finite R T] : IsFiniteSplit R T

Over a ring with preconnected prime spectrum and without nonsplit finite étale covers, every finite étale algebra has constant split rank: it is R-isomorphic to Fin n → R for some n.

theorem TauCeti.IsFiniteEtaleSplit.nonempty_algHom {R : Type u} [CommRing R] (S : Type u_1) [CommRing S] [Algebra R S] [IsFiniteEtaleSplit S] (T : Type u_2) [CommRing T] [Algebra R T] [Algebra.Etale R T] [Module.Finite R T] [Module.FaithfullyFlat R T] : Nonempty (T →ₐ[R] S)

A faithfully flat finite étale R-algebra T admits an R-algebra map to every R-algebra S without nonsplit finite étale covers: the base change S ⊗[R] T is faithfully flat and finite étale over S, hence has a section.

instance TauCeti.IsFiniteEtaleSplit.pi {ι : Type u_1} (A : ι → Type u_2) [(i : ι) → CommRing (A i)] [∀ (i : ι), IsFiniteEtaleSplit (A i)] : IsFiniteEtaleSplit ((i : ι) → A i)

A product of rings without nonsplit finite étale covers, over any index type, has none: a faithfully flat finite étale algebra over the product maps to every factor, and these maps assemble to a section.

instance TauCeti.IsFiniteEtaleSplit.prod (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [IsFiniteEtaleSplit A] [IsFiniteEtaleSplit B] : IsFiniteEtaleSplit (A × B)

A product of two rings without nonsplit finite étale covers has none: a faithfully flat finite étale algebra over the product maps to both factors, and these maps assemble to a section.

theorem TauCeti.IsFiniteEtaleSplit.of_essSurj_baseChange {R : Type u} [CommRing R] (R' : Type u_1) [CommRing R'] [Algebra R R'] [IsFiniteEtaleSplit R] [(CommAlgCat.FiniteEtale.baseChange R R').EssSurj] : IsFiniteEtaleSplit R'

If every finite étale R'-algebra is a base change of a finite étale R-algebra, and R has no nonsplit finite étale covers, then neither does R'.

theorem TauCeti.IsFiniteEtaleSplit.of_full_baseChange {R : Type u} [CommRing R] (R' : Type u_1) [CommRing R'] [Algebra R R'] [IsFiniteEtaleSplit R'] [(CommAlgCat.FiniteEtale.baseChange R R').Full] : IsFiniteEtaleSplit R

If base change along R → R' is full on finite étale algebras and R' has no nonsplit finite étale covers, then neither does R: the section of R' ⊗[R] T over R' descends to a section of T over R.

theorem TauCeti.isFiniteEtaleSplit_iff_of_full_of_essSurj {R : Type u} [CommRing R] (R' : Type u_1) [CommRing R'] [Algebra R R'] [(CommAlgCat.FiniteEtale.baseChange R R').Full] [(CommAlgCat.FiniteEtale.baseChange R R').EssSurj] : IsFiniteEtaleSplit R ↔ IsFiniteEtaleSplit R'

Having no nonsplit finite étale covers is invariant under a ring map along which base change of finite étale algebras is full and essentially surjective, e.g. an equivalence of categories.

theorem RingEquiv.isFiniteEtaleSplit {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] [TauCeti.IsFiniteEtaleSplit A] (e : A ≃+* R) : TauCeti.IsFiniteEtaleSplit R

Having no nonsplit finite étale covers is invariant under ring isomorphisms: a faithfully flat finite étale R-algebra is faithfully flat and finite étale over A through e, and its section over A composed with e is a section over R.