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