Étale algebras and idempotent decompositions

Idempotents split an algebra into a product of its clopen components. This file records that étaleness is compatible with both directions of such a splitting: a binary product of étale algebras is étale (TauCeti.Algebra.Etale.prod), and the quotient of an étale algebra by an idempotent, which is the complementary component, is étale (TauCeti.Algebra.Etale.quotient_span_singleton). Mathlib supplies the finite products Π i, A i indexed by a type; the binary product A × B is reduced to these.

Idempotents of the base split it in the same way, and étaleness is local for such a splitting: an algebra is étale if its base change to every component of a complete orthogonal family of idempotents of the base is (TauCeti.Algebra.Etale.of_completeOrthogonalIdempotents).

instance TauCeti.Algebra.Etale.prod {R : Type u} [CommRing R] {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra.Etale R A] [Algebra.Etale R B] : Algebra.Etale R (A × B)

A binary product of étale algebras is étale.

theorem TauCeti.Algebra.Etale.quotient_span_singleton {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] [Algebra.Etale R S] {e : S} (he : IsIdempotentElem e) : Algebra.Etale R (S ⧸ Ideal.span {e})

The quotient of an étale algebra by an idempotent is étale: it is the localization away from the complementary idempotent.

theorem TauCeti.Algebra.Etale.of_completeOrthogonalIdempotents {T : Type u_1} {X : Type u_2} [CommRing T] [CommRing X] [Algebra T X] {ι : Type u_3} [Fintype ι] {f : ι → T} (hf : CompleteOrthogonalIdempotents f) (h : ∀ (i : ι), Algebra.Etale (T ⧸ Ideal.span {1 - f i}) (TensorProduct T (T ⧸ Ideal.span {1 - f i}) X)) : Algebra.Etale T X

Étaleness is local for a decomposition of the base by complete orthogonal idempotents: if the base change of X to every component T ⧸ (1 - f i) is étale, then X is étale over T.