Descent of finiteness conditions under faithfully flat maps #
In this file we show that
descend along faithfully flat base change.
theorem Module.Finite.of_finite_tensorProduct_of_faithfullyFlat {R : Type u_1} [CommRing R] (T : Type u_3) [CommRing T] [Algebra R T] {M : Type u_4} [AddCommGroup M] [Module R M] [FaithfullyFlat R T] [Module.Finite T (TensorProduct R T M)] :
Module.Finite R M
theorem Ideal.FG.of_FG_map_of_faithfullyFlat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] {I : Ideal R} (hI : (Ideal.map (algebraMap R S) I).FG) :
I.FG
theorem Algebra.FiniteType.of_finiteType_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] [FiniteType T (TensorProduct R T S)] :
FiniteType R S
If T ⊗[R] S is of finite type over T and T is R-faithfully flat,
then S is of finite type over R
theorem Algebra.FinitePresentation.of_finitePresentation_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] [FinitePresentation T (TensorProduct R T S)] :
If T ⊗[R] S is of finite presentation over T and T is R-faithfully flat,
then S is of finite presentation over R
theorem RingHom.FiniteType.codescendsAlong_faithfullyFlat :
CodescendsAlong (fun {R S : Type u_4} [CommRing R] [CommRing S] => FiniteType)
fun {R S : Type u_4} [CommRing R] [CommRing S] => FaithfullyFlat
theorem RingHom.FinitePresentation.codescendsAlong_faithfullyFlat :
CodescendsAlong (fun {R S : Type u_4} [CommRing R] [CommRing S] => FinitePresentation)
fun {R S : Type u_4} [CommRing R] [CommRing S] => FaithfullyFlat
theorem RingHom.Finite.codescendsAlong_faithfullyFlat :
CodescendsAlong (fun {R S : Type u_4} [CommRing R] [CommRing S] => Finite)
fun {R S : Type u_4} [CommRing R] [CommRing S] => FaithfullyFlat