Remark

Tag 044Y, permanent. Cite it as [Bourbaki, Tag 044Y].

Proposition 2 also follows from the existence of the exact sequence

E \otimes_S \operatorname{Tor}_1^R(\rho_*(S_d), F) \to \operatorname{Tor}_1^R(\rho_*(E), F) \to \operatorname{Tor}_1^S(E, S_d \otimes_R F) \to 0

arising from the spectral sequence of the "associativity" of the Tor functors.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by

Nothing.