mathlib documentation

linear_algebra.adic_completion

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

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

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

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

Equations
Instances
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 : ), (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) [add_comm_group M] [module R M] :

theorem is_Hausdorff.subsingleton {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] :

@[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] :
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) :
(∀ (x : M), C ((Hausdorffification.of I M) x))C x

@[instance]
def Hausdorffification.is_Hausdorff {R : Type u_1} [comm_ring R] (I : ideal R) (M : Type u_2) [add_comm_group M] [module R M] :

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

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) :

Uniqueness of lift.

@[instance]
def is_precomplete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :

@[instance]
def is_precomplete.top {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :

@[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)} :
(∀ (n : ), (adic_completion.eval I M n) x = (adic_completion.eval I M n) y)x = y

@[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] :

@[instance]
def is_adic_complete.bot {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :

theorem is_adic_complete.subsingleton {R : Type u_1} [comm_ring R] (M : Type u_2) [add_comm_group M] [module R M] :

@[instance]
def is_adic_complete.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] :