Completion of a topological ring

[kbuzzard]

We need completions to define the sections of the presheaf on Spa(A).

To define the presheaf on a rational open in Spa(A) via the formula in Wedhorn (8.2.1) (p75) we need to create the ring A<T/s>, which is a completion -- see p74, six lines down. To extend the presheaf to an arbitrary open we need that projective limits exist in the category of complete topological commutative rings, although Reid and possibly also Mario suggested that we might want to show that complete comm rings are a reflective category of all comm rings because this provides stronger results which we might well need. We need the universal property of completions stated at the beginning of section 8.1 (to define the restriction morphisms).

[PatrickMassot]

This is ridiculously close to being in mathlib. https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/completion.lean#L1168 assumes the ring is separated, but there is also https://github.com/leanprover/mathlib/blob/80d688e3ae2a721ab61f4cd000ea3e336158b04f/analysis/topology/quotient_topological_structures.lean#L204 saying that the separation quotient of a topological ring is a topological ring. So the maths 100% done, we only lack diamond-free transport of structure.

[PatrickMassot]

This is now done in my fork of mathlib, hopefully merged upstream soon