Completion of a module with respect to an ideal.
In this file we define the notions of Hausdorff, precomplete, and complete for an R
-module M
with respect to an ideal I
:
Main definitions
is_Hausdorff I M
: this says that the intersection ofI^n M
is0
.is_precomplete I M
: this says that every Cauchy sequence converges.is_adic_complete I M
: this says thatM
is Hausdorff and precomplete.Hausdorffification I M
: this is the universal Hausdorff module with a map fromM
.completion I M
: ifI
is finitely generated, then this is the universal complete module (TODO) with a map fromM
. This map is injective iffM
is Hausdorff and surjective iffM
is precomplete.
A module M
is Hausdorff with respect to an ideal I
if ⋂ I^n M = 0
.
A module M
is precomplete with respect to an ideal I
if every Cauchy sequence converges.
Equations
A module M
is I
-adically complete if it is Hausdorff and precomplete.
Equations
- is_adic_complete I M = (is_Hausdorff I M ∧ is_precomplete I M)
The Hausdorffification of a module with respect to an ideal.
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.
Equations
- _ = _
Equations
- _ = _
The canonical linear map to the Hausdorffification.
Equations
- _ = _
universal property of Hausdorffification: any linear map to a Hausdorff module extends to a unique map from the Hausdorffification.
Uniqueness of lift.
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
The canonical linear map to the completion.
Linearly evaluating a sequence in the completion at a given input.
Equations
- adic_completion.eval I M n = {to_fun := λ (f : ↥(adic_completion I M)), f.val n, map_add' := _, map_smul' := _}
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _