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
Main definitions #
IsHausdorff I M: this says that the intersection of
IsPrecomplete I M: this says that every Cauchy sequence converges.
IsAdicComplete I M: this says that
Mis Hausdorff and precomplete.
Hausdorffification I M: this is the universal Hausdorff module with a map from
adicCompletion 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 precomplete with respect to an ideal
I if every Cauchy sequence converges.
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.