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 #

• IsHausdorff I M: this says that the intersection of I^n M is 0.
• IsPrecomplete I M: this says that every Cauchy sequence converges.
• IsAdicComplete I M: this says that M is Hausdorff and precomplete.
• Hausdorffification I M: this is the universal Hausdorff module with a map from M.
• adicCompletion 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 IsHausdorff {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

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

Instances
class IsPrecomplete {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

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

Instances
class IsAdicComplete {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] extends , :

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

Instances
theorem IsHausdorff.haus {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] :
∀ (x : M), (∀ (n : ), x 0 [SMOD I ^ n ]) → x = 0
theorem isHausdorff_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] :
∀ (x : M), (∀ (n : ), x 0 [SMOD I ^ n ]) → x = 0
theorem IsPrecomplete.prec {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] :
∀ {f : M}, (∀ {m n : }, m nf m f n [SMOD I ^ m ]) → L, ∀ (n : ), f n L [SMOD I ^ n ]
theorem isPrecomplete_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] :
∀ (f : M), (∀ {m n : }, m nf m f n [SMOD I ^ m ]) → L, ∀ (n : ), f n L [SMOD I ^ n ]
@[reducible]
def Hausdorffification {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Type u_2

The Hausdorffification of a module with respect to an ideal.

Instances For
def adicCompletion {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Submodule R ((n : ) → M I ^ n )

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.

Instances For
instance IsHausdorff.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
theorem IsHausdorff.subsingleton {R : Type u_1} [] {M : Type u_2} [] [Module R M] (h : ) :
instance IsHausdorff.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
theorem IsHausdorff.iInf_pow_smul {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (h : ) :
⨅ (n : ), I ^ n =
def Hausdorffification.of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

The canonical linear map to the Hausdorffification.

Instances For
theorem Hausdorffification.induction_on {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {C : } (x : ) (ih : (x : M) → C (↑() x)) :
C x
def Hausdorffification.lift {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [h : ] (f : M →ₗ[R] N) :

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

Instances For
theorem Hausdorffification.lift_of {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [h : ] (f : M →ₗ[R] N) (x : M) :
↑() (↑() x) = f x
theorem Hausdorffification.lift_comp_of {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [h : ] (f : M →ₗ[R] N) :
= f
theorem Hausdorffification.lift_eq {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] [h : ] (f : M →ₗ[R] N) (g : →ₗ[R] N) (hg : = f) :

Uniqueness of lift.

instance IsPrecomplete.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
instance IsPrecomplete.top {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
instance IsPrecomplete.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
def adicCompletion.of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
M →ₗ[R] { x // x }

The canonical linear map to the completion.

Instances For
@[simp]
theorem adicCompletion.of_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (x : M) (n : ) :
↑(↑() x) n = ↑(Submodule.mkQ (I ^ n )) x
def adicCompletion.eval {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
{ x // x } →ₗ[R] M I ^ n

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

Instances For
@[simp]
theorem adicCompletion.coe_eval {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
↑() = fun f => f n
theorem adicCompletion.eval_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) (f : { x // x }) :
↑() f = f n
theorem adicCompletion.eval_of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) (x : M) :
↑() (↑() x) = ↑(Submodule.mkQ (I ^ n )) x
@[simp]
theorem adicCompletion.eval_comp_of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
@[simp]
theorem adicCompletion.range_eval {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
theorem adicCompletion.ext {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {x : { x // x }} {y : { x // x }} (h : ∀ (n : ), ↑() x = ↑() y) :
x = y
instance IsAdicComplete.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
theorem IsAdicComplete.subsingleton {R : Type u_1} [] (M : Type u_2) [] [Module R M] (h : ) :
instance IsAdicComplete.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
theorem IsAdicComplete.le_jacobson_bot {R : Type u_1} [] (I : ) [] :