Etale descends along faithfully flat ring maps

In this file we show that smooth, unramified and étale algebras descend along faithfully flat base change.

Main results

• Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat: Smooth descends.
• Algebra.Unramified.of_smooth_tensorProduct_of_faithfullyFlat: Unramified descends.
• Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat: Etale descends.

We also provide the corresponding RingHom.CodescendsAlong lemmas.

TODOs

• The lemma Algebra.FormallySmooth.of_formallySmooth_tensorProduct_of_faithfullyFlat has an additional Algebra.FinitePresentation assumption, because the proof uses that a flat module of finite presentation is projective and the former descends. This also holds without the finite presentation assumption, but requires showing that projectivity descends along faithfully flat base change, which is due to Raynaud and Gruson (see https://stacks.math.columbia.edu/tag/058B).

theorem Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.FaithfullyFlat R T] [FormallyUnramified T (TensorProduct R T S)] : FormallyUnramified R S

theorem Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.FaithfullyFlat R T] [Smooth T (TensorProduct R T S)] : Smooth R S

theorem Algebra.Unramified.of_unramified_tensorProduct_of_faithfullyFlat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.FaithfullyFlat R T] [Unramified T (TensorProduct R T S)] : Unramified R S

theorem Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] [Module.FaithfullyFlat R T] [Etale T (TensorProduct R T S)] : Etale R S

theorem RingHom.Smooth.codescendsAlong_faithfullyFlat : CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] => Smooth) fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat

theorem RingHom.FormallyUnramified.codescendsAlong_faithfullyFlat : CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] => FormallyUnramified) fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat

theorem RingHom.Etale.codescendsAlong_faithfullyFlat : CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] => Etale) fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat