mathlib documentation

linear_algebra.​adic_completion

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

Equations
  • _ = _
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] :

Equations
  • _ = _
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] :

Equations
  • _ = _
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] :

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

Equations
  • _ = _
@[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] :

Equations
  • _ = _
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] :

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

Equations
  • _ = _
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] :

Equations
  • _ = _