Remark 52.7.4. Here are some references to discussions of related material the literature. It seems that a “derived formal functions theorem” for proper maps goes back to [Theorem 6.3.1, lurie-thesis]. There is the discussion in [dag12], especially Chapter 4 which discusses the affine story, see More on Algebra, Section 15.90. In [Section 2.9, G-R] one finds a discussion of proper base change and derived completion using (ind) coherent modules. An analogue of (52.7.0.1) for complexes of quasi-coherent modules can be found as [Theorem 6.5, HL-P]

There are also:

• 2 comment(s) on Section 52.7: The theorem on formal functions

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).