Completion of a module with respect to an ideal.
In this file we define the notions of Hausdorff, precomplete, and complete for an
with respect to an ideal
is_Hausdorff I M: this says that the intersection of
is_precomplete I M: this says that every Cauchy sequence converges.
is_adic_complete I M: this says that
Mis Hausdorff and precomplete.
Hausdorffification I M: this is the universal Hausdorff module with a map from
completion I M: if
Iis finitely generated, then this is the universal complete module (TODO) with a map from
M. This map is injective iff
Mis Hausdorff and surjective iff
M is Hausdorff with respect to an ideal
⋂ I^n M = 0.
M is precomplete with respect to an ideal
I if every Cauchy sequence converges.
I-adically complete if it is Hausdorff and precomplete.
The completion of a module with respect to an ideal. This is not necessarily Hausdorff. In fact, this is only complete if the ideal is finitely generated.
universal property of Hausdorffification: any linear map to a Hausdorff module extends to a unique map from the Hausdorffification.
Uniqueness of lift.
The canonical linear map to the completion.
Linearly evaluating a sequence in the completion at a given input.