# 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 of I^n M is 0.
• is_precomplete I M: this says that every Cauchy sequence converges.
• is_adic_complete I M: this says that M is Hausdorff and precomplete.
• Hausdorffification I M: this is the universal Hausdorff module with a map from M.
• completion I M: if I is finitely generated, then this is the universal complete module (TODO) with a map from M. This map is injective iff M is Hausdorff and surjective iff M is precomplete.
@[class]
structure is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Prop

A module M is Hausdorff with respect to an ideal I if ⋂ I^n M = 0.

Instances
@[class]
structure is_precomplete {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Prop

A module M is precomplete with respect to an ideal I if every Cauchy sequence converges.

Instances
@[class]
structure is_adic_complete {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Prop
• to_is_Hausdorff : M
• to_is_precomplete :

A module M is I-adically complete if it is Hausdorff and precomplete.

Instances
theorem is_Hausdorff.haus {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] (h : M) (x : M) :
(∀ (n : ), x 0 [SMOD I ^ n ])x = 0
theorem is_Hausdorff_iff {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] :
M ∀ (x : M), (∀ (n : ), x 0 [SMOD I ^ n ])x = 0
theorem is_precomplete.prec {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] (h : M) {f : → M} :
(∀ {m n : }, m nf m f n [SMOD I ^ m ])(∃ (L : M), ∀ (n : ), f n L [SMOD I ^ n ])
theorem is_precomplete_iff {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] :
∀ (f : → M), (∀ {m n : }, m nf m f n [SMOD I ^ m ])(∃ (L : M), ∀ (n : ), f n L [SMOD I ^ n ])
def Hausdorffification {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Type u_2

The Hausdorffification of a module with respect to an ideal.

Equations
def adic_completion {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
(Π (n : ), (I ^ n ).quotient)

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
@[instance]
def is_Hausdorff.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [ M] :
theorem is_Hausdorff.subsingleton {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] (h : M) :
@[instance]
def is_Hausdorff.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] [subsingleton M] :
M
theorem is_Hausdorff.infi_pow_smul {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] (h : M) :
(⨅ (n : ), I ^ n ) =
def Hausdorffification.of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :

The canonical linear map to the Hausdorffification.

Equations
theorem Hausdorffification.induction_on {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] {C : → Prop} (x : M) (ih : ∀ (x : M), C ( x)) :
C x
@[instance]
def Hausdorffification.is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
M)
def Hausdorffification.lift {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [ M] {N : Type u_3} [ N] [h : N] (f : M →ₗ[R] N) :

universal property of Hausdorffification: any linear map to a Hausdorff module extends to a unique map from the Hausdorffification.

Equations
theorem Hausdorffification.lift_of {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [ M] {N : Type u_3} [ N] [h : N] (f : M →ₗ[R] N) (x : M) :
( x) = f x
theorem Hausdorffification.lift_comp_of {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [ M] {N : Type u_3} [ N] [h : N] (f : M →ₗ[R] N) :
.comp = f
theorem Hausdorffification.lift_eq {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [ M] {N : Type u_3} [ N] [h : N] (f : M →ₗ[R] N) (g : →ₗ[R] N) (hg : g.comp = f) :

Uniqueness of lift.

@[instance]
def is_precomplete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [ M] :
@[instance]
def is_precomplete.top {R : Type u_1} [comm_ring R] (M : Type u_2) [ M] :
@[instance]
def is_precomplete.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] [subsingleton M] :
def adic_completion.of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :

The canonical linear map to the completion.

Equations
@[simp]
theorem adic_completion.of_apply {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (x : M) (n : ) :
( M) x).val n = ((I ^ n ).mkq) x
def adic_completion.eval {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) :

Linearly evaluating a sequence in the completion at a given input.

Equations
@[simp]
theorem adic_completion.coe_eval {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) :
n) = λ (f : M)), f.val n
theorem adic_completion.eval_apply {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) (f : M)) :
n) f = f.val n
theorem adic_completion.eval_of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) (x : M) :
n) ( M) x) = ((I ^ n ).mkq) x
@[simp]
theorem adic_completion.eval_comp_of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) :
n).comp M) = (I ^ n ).mkq
@[simp]
theorem adic_completion.range_eval {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] (n : ) :
n).range =
@[ext]
theorem adic_completion.ext {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [ M] {x y : M)} (h : ∀ (n : ), n) x = n) y) :
x = y
@[instance]
def adic_completion.is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
M)
@[instance]
def is_adic_complete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [ M] :
theorem is_adic_complete.subsingleton {R : Type u_1} [comm_ring R] (M : Type u_2) [ M] (h : M) :
@[instance]
def is_adic_complete.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] [subsingleton M] :
theorem is_adic_complete.le_jacobson_bot {R : Type u_1} [comm_ring R] (I : ideal R) [ R] :