We may check this locally on
so by
Lemma 5.2.5 we may assume that
is principal generated by a distinguished element
Let
be a morphism of
-pairs. Let
be the free
-ring over
in the generators
for
Let
be the derived
-completion of
(viewed as a
-ring using
Exercise 6.7.12). If
is
-torsion-free, then
has the desired universal property. Otherwise, we transfinitely iterate the operations of taking the maximal
-torsion-free quotient and taking the derived
-completion; this terminates because a countably filtered colimit of derived
-complete rings is again derived
-complete (
Remark 6.3.4), so we can stop taking the completions once we get to an uncountable ordinal.