Equalizers of finite étale algebras

The equalizer of two algebra maps f g : A →ₐ[R] B between finite étale R-algebras is a finite étale R-algebra (AlgHom.etale_equalizer, AlgHom.finite_equalizer). In particular, the invariants of a finite étale algebra under a finite monoid acting by algebra endomorphisms form a finite étale algebra (TauCeti.FixedPoints.etale_subalgebra, TauCeti.FixedPoints.finite_subalgebra). Geometrically, the affine coequalizer of two morphisms of finite étale Spec R-schemes, and the invariant quotient of a finite étale Spec R-scheme by a finite group, are again finite étale. The invariant quotients supply the quotients by finite groups that the axioms of a Galois category require of finite étale covers.

Main results

• AlgHom.etale_equalizer, AlgHom.finite_equalizer: equalizers of finite étale algebras are finite étale.
• TauCeti.FixedPoints.etale_subalgebra, TauCeti.FixedPoints.finite_subalgebra: invariants of a finite étale algebra under a finite monoid are finite étale.

Implementation notes

The proof reduces to split algebras in three steps.

• Over a split base, an algebra map φ : (ι → T) →ₐ[T] (κ → T) has idempotent matrix entries φ (Pi.single i 1) j. Over the component of each atom of the Boolean algebra they generate (TauCeti.completeOrthogonalIdempotents_prod_ite), every entry is 0 or 1, so φ is induced by a map κ → ι, and the equalizer of two such maps is the algebra of functions on a quotient of ι.
• If A and B have constant ranks, they both split after a faithfully flat finite étale base change (Algebra.IsFiniteSplit.exists_tensorProduct_of_etale). Flat base change commutes with equalizers (AlgHom.tensorEqualizerEquiv), and finite étaleness descends along faithfully flat maps.
• In general the ranks are locally constant, and the atoms of the idempotents cutting out their fibres decompose the base into components where both ranks are constant. Finite étaleness is local for such a decomposition (TauCeti.Algebra.Etale.of_completeOrthogonalIdempotents, TauCeti.Module.Finite.of_completeOrthogonalIdempotents).

The main results take R, A and B in one universe, as Algebra.IsFiniteSplit.exists_tensorProduct_of_etale does.

References

• H. W. Lenstra, Galois theory for schemes, Section 5.
• The Stacks Project, Section 58.5 (tag 0BL8), Finite étale covers of schemes.

instance AlgHom.etale_equalizer {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra.Etale R A] [Module.Finite R A] [Algebra.Etale R B] [Module.Finite R B] (f g : A →ₐ[R] B) : Algebra.Etale R ↥(f.equalizer g)

The equalizer of two algebra maps between finite étale algebras is étale.

instance AlgHom.finite_equalizer {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra.Etale R A] [Module.Finite R A] [Algebra.Etale R B] [Module.Finite R B] (f g : A →ₐ[R] B) : Module.Finite R ↥(f.equalizer g)

The equalizer of two algebra maps between finite étale algebras is a finite module.

instance TauCeti.FixedPoints.etale_subalgebra {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_1) [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] [Algebra.Etale R S] [Module.Finite R S] [Finite G] : Algebra.Etale R ↥(FixedPoints.subalgebra R S G)

The invariants of a finite étale algebra under a finite monoid of algebra endomorphisms form an étale algebra.

instance TauCeti.FixedPoints.finite_subalgebra {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_1) [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] [Algebra.Etale R S] [Module.Finite R S] [Finite G] : Module.Finite R ↥(FixedPoints.subalgebra R S G)

The invariants of a finite étale algebra under a finite monoid of algebra endomorphisms form a finite module.