The Stacks project

I apologise if this is my misunderstanding, but this seems to be a useful technical lemma. Maybe one can add a slogan 'Perfect complexes lift along nilpotent immersions with same tor-amplitude'

I guess that the slogan I suggested seems to be a bit stronger than what the lemma is doing (eg. as a $k[x]/x^e$-module $k$ has unbounded tor-dimension). Maybe a better slogan is that 'perfectness and tor-amplitude can be checked after base change along a nilpotent surjection'

One final comment (which I learnt from Yuchen Wu, all mistakes are solely mine).

It seems that at least in the absolute case i.e. when $A'=R'$ and therefore $A=R$ then one can show that tor-dimension can be checked after base change to $R$ without the seemingly implicit pseudocoherence assumption (apologies if this is already obvious in the proof above).

The reason is that if $M'$ is an $R'$-module so that $IM'=0$ then $M'$ is already an $R$ module. Therefore $M'=R\otimes^L_R M'$.

Now the equation $K'\otimes^L_{R'}M'=K\otimes^L_{R}M'$ seems to hold without passing through the explicit resolutions $P$ and $E$ because $$K'\otimes^L_{R'}M'=K'\otimes^L_{R'}(R\otimes^L_R M')=(K'\otimes^L_{R'}R)\otimes^L_RM'=K\otimes_R^L M'.$$

Then one reasons as you do.

If this is fine, I would suggest adding this in tag 0651.

OK, this is such a technical lemma that a slogan does not work well, I think.

I like your and Yuchen Wu's suggestion of the additional lemma. I have added it here.