# 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]
def 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.

Equations
Instances
@[class]
def 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.

Equations
Instances
@[class]
def is_adic_complete {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] :
Prop

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

Equations
Instances
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] :

@[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] :
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) :
(∀ (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] :
(M →ₗ[R] N) →ₗ[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) :
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)} :
(∀ (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] :

@[instance]
def is_adic_complete.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [ M] [subsingleton M] :