Theorems · Theorem · commutative algebra

Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T]
  [Algebra.FinitePresentation T (TensorProduct R T S)], Algebra.FinitePresentation R 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

Defined in

Mathlib.RingTheory.Finiteness.Descent

Cited by

2 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraModule.FaithfullyFlatAlgebra.FinitePresentation