mathlib3 documentation

linear_algebra.adic_completion

Completion of a module with respect to an ideal. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[class]
structure is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :
Prop

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

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

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

Instances of this typeclass
@[class]
structure is_adic_complete {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :
Prop

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

Instances of this typeclass
theorem is_Hausdorff.haus {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [add_comm_group M] [module R M] (h : is_Hausdorff I 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} [add_comm_group M] [module R M] :
is_Hausdorff I 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} [add_comm_group M] [module R M] (h : is_precomplete I M) {f : M} :
( {m n : }, m n f 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} [add_comm_group M] [module R M] :
is_precomplete I M (f : M), ( {m n : }, m n f m f n [SMOD I ^ m ]) ( (L : M), (n : ), f n L [SMOD I ^ n ])
@[reducible]
def Hausdorffification {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R 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) [add_comm_group M] [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.

Equations
Instances for adic_completion
@[protected, instance]
def is_Hausdorff.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :
@[protected]
theorem is_Hausdorff.subsingleton {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (h : is_Hausdorff M) :
@[protected, instance]
def is_Hausdorff.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] [subsingleton M] :
theorem is_Hausdorff.infi_pow_smul {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [add_comm_group M] [module R M] (h : is_Hausdorff I M) :
( (n : ), I ^ n ) =
def Hausdorffification.of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R 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} [add_comm_group M] [module R M] {C : Hausdorffification I M Prop} (x : Hausdorffification I M) (ih : (x : M), C ((Hausdorffification.of I M) x)) :
C x
@[protected, instance]
def Hausdorffification.lift {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [h : is_Hausdorff I 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} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [h : is_Hausdorff I N] (f : M →ₗ[R] N) (x : M) :
theorem Hausdorffification.lift_comp_of {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [h : is_Hausdorff I N] (f : M →ₗ[R] N) :
theorem Hausdorffification.lift_eq {R : Type u_1} [comm_ring R] (I : ideal R) {M : Type u_2} [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] [h : is_Hausdorff I N] (f : M →ₗ[R] N) (g : Hausdorffification I M →ₗ[R] N) (hg : g.comp (Hausdorffification.of I M) = f) :

Uniqueness of lift.

@[protected, instance]
def is_precomplete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :
@[protected, instance]
def is_precomplete.top {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :
@[protected, instance]
def is_precomplete.of_subsingleton {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] [subsingleton M] :
def adic_completion.of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R 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) [add_comm_group M] [module R M] (x : M) (n : ) :
((adic_completion.of I 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) [add_comm_group M] [module R 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) [add_comm_group M] [module R M] (n : ) :
(adic_completion.eval I M n) = λ (f : (adic_completion I M)), f.val n
theorem adic_completion.eval_apply {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] (n : ) (f : (adic_completion I M)) :
theorem adic_completion.eval_of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] (n : ) (x : M) :
@[simp]
theorem adic_completion.eval_comp_of {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] (n : ) :
@[simp]
theorem adic_completion.range_eval {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] (n : ) :
@[ext]
theorem adic_completion.ext {R : Type u_1} [comm_ring R] {I : ideal R} {M : Type u_2} [add_comm_group M] [module R M] {x y : (adic_completion I M)} (h : (n : ), (adic_completion.eval I M n) x = (adic_completion.eval I M n) y) :
x = y
@[protected, instance]
def adic_completion.is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :
@[protected, instance]
def is_adic_complete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :
@[protected]
theorem is_adic_complete.subsingleton {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] (h : is_adic_complete M) :
@[protected, instance]