# 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
theorem IsHausdorff.haus' {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] [self : ] (x : M) :
(∀ (n : ), x 0 [SMOD I ^ n ])x = 0
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
theorem IsPrecomplete.prec' {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] [self : ] (f : M) :
(∀ {m n : }, m nf m f n [SMOD I ^ m ])∃ (L : M), ∀ (n : ), f n L [SMOD I ^ n ]
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 : M), ∀ (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 : M), ∀ (n : ), f n L [SMOD I ^ n ]
@[reducible, inline]
noncomputable abbrev 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.

Equations
Instances For
noncomputable def AdicCompletion.transitionMap {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } (hmn : m n) :
M I ^ n →ₗ[R] M I ^ m

The canonical linear map M ⧸ (I ^ n • ⊤) →ₗ[R] M ⧸ (I ^ m • ⊤) for m ≤ n used to define AdicCompletion.

Equations
Instances For
noncomputable def AdicCompletion {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Type u_2

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
noncomputable instance IsHausdorff.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
Equations
• =
theorem IsHausdorff.subsingleton {R : Type u_1} [] {M : Type u_2} [] [Module R M] (h : ) :
@[instance 100]
noncomputable instance IsHausdorff.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
Equations
• =
theorem IsHausdorff.iInf_pow_smul {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (h : ) :
⨅ (n : ), I ^ n =
noncomputable def Hausdorffification.of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

The canonical linear map to the Hausdorffification.

Equations
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
noncomputable instance Hausdorffification.instIsHausdorff {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• =
noncomputable 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.

Equations
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 : g ∘ₗ = f) :

Uniqueness of lift.

noncomputable instance IsPrecomplete.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
Equations
• =
noncomputable instance IsPrecomplete.top {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
Equations
• =
@[instance 100]
noncomputable instance IsPrecomplete.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
Equations
• =
noncomputable def AdicCompletion.submodule {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Submodule R ((n : ) → M I ^ n )

AdicCompletion is the submodule of compatible families in ∀ n : ℕ, M ⧸ (I ^ n • ⊤).

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance AdicCompletion.instZero {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Zero ()
Equations
• = { zero := 0, }
noncomputable instance AdicCompletion.instAdd {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { add := fun (x y : ) => x + y, }
noncomputable instance AdicCompletion.instNeg {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Neg ()
Equations
• = { neg := fun (x : ) => -x, }
noncomputable instance AdicCompletion.instSub {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Sub ()
Equations
• = { sub := fun (x y : ) => x - y, }
noncomputable instance AdicCompletion.instSMulNat {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { smul := fun (n : ) (x : ) => n x, }
noncomputable instance AdicCompletion.instSMulInt {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { smul := fun (n : ) (x : ) => n x, }
noncomputable instance AdicCompletion.instAddCommGroup {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
noncomputable instance AdicCompletion.instSMul {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
SMul R ()
Equations
• = { smul := fun (r : R) (x : ) => r x, }
noncomputable instance AdicCompletion.instModule {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Module R ()
Equations
• = let f := { toFun := Subtype.val, map_zero' := , map_add' := };
noncomputable def AdicCompletion.incl {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
→ₗ[R] (n : ) → M I ^ n

The canonical inclusion from the completion to the product.

Equations
• = { toFun := fun (x : ) => x, map_add' := , map_smul' := }
Instances For
@[simp]
theorem AdicCompletion.incl_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (x : ) (n : ) :
() x n = x n
noncomputable def AdicCompletion.of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

The canonical linear map to the completion.

Equations
• = { toFun := fun (x : M) => fun (n : ) => (I ^ n ).mkQ x, , map_add' := , map_smul' := }
Instances For
@[simp]
theorem AdicCompletion.of_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (x : M) (n : ) :
(() x) n = (I ^ n ).mkQ x
noncomputable def AdicCompletion.eval {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
→ₗ[R] M I ^ n

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

Equations
• = { toFun := fun (f : ) => f n, map_add' := , map_smul' := }
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 : ) :
() f = f n
theorem AdicCompletion.eval_of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) (x : M) :
() (() x) = (I ^ n ).mkQ x
@[simp]
theorem AdicCompletion.eval_comp_of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
∘ₗ = (I ^ n ).mkQ
theorem AdicCompletion.eval_surjective {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 : ) :
@[simp]
theorem AdicCompletion.val_zero {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
0 n = 0
@[simp]
theorem AdicCompletion.val_add {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (f : ) (g : ) :
(f + g) n = f n + g n
@[simp]
theorem AdicCompletion.val_sub {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (f : ) (g : ) :
(f - g) n = f n - g n
@[simp]
theorem AdicCompletion.val_sum {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {α : Type u_4} (s : ) (f : α) (n : ) :
(s.sum f) n = as, (f a) n
theorem AdicCompletion.val_smul {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (r : R) (f : ) :
(r f) n = r f n
theorem AdicCompletion.ext {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {x : } {y : } (h : ∀ (n : ), x n = y n) :
x = y
theorem AdicCompletion.ext_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {x : } {y : } :
x = y ∀ (n : ), x n = y n
noncomputable instance AdicCompletion.instIsHausdorff {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• =
@[simp]
theorem AdicCompletion.transitionMap_mk {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } (hmn : m n) (x : M) :
@[simp]
theorem AdicCompletion.transitionMap_eq {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
= LinearMap.id
@[simp]
theorem AdicCompletion.transitionMap_comp {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } {k : } (hmn : m n) (hnk : n k) :
∘ₗ =
@[simp]
theorem AdicCompletion.transitionMap_comp_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } {k : } (hmn : m n) (hnk : n k) (x : M I ^ k ) :
() (() x) = () x
@[simp]
theorem AdicCompletion.transitionMap_comp_eval_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } (hmn : m n) (x : ) :
() (x n) = x m
@[simp]
theorem AdicCompletion.transitionMap_comp_eval {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {m : } {n : } (hmn : m n) :
∘ₗ =
noncomputable def AdicCompletion.IsAdicCauchy {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : M) :

A sequence ℕ → M is an I-adic Cauchy sequence if for every m ≤ n, f m ≡ f n modulo I ^ m • ⊤.

Equations
Instances For
noncomputable def AdicCompletion.AdicCauchySequence {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Type u_2

The type of I-adic Cauchy sequences.

Equations
• = { f : M // }
Instances For
noncomputable def AdicCompletion.AdicCauchySequence.submodule {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Submodule R (M)

The type of I-adic cauchy sequences is a submodule of the product ℕ → M.

Equations
• = { carrier := {f : M | }, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
noncomputable instance AdicCompletion.AdicCauchySequence.instZero {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { zero := 0, }
noncomputable instance AdicCompletion.AdicCauchySequence.instAdd {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { add := fun (x y : ) => x + y, }
noncomputable instance AdicCompletion.AdicCauchySequence.instNeg {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { neg := fun (x : ) => -x, }
noncomputable instance AdicCompletion.AdicCauchySequence.instSub {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { sub := fun (x y : ) => x - y, }
noncomputable instance AdicCompletion.AdicCauchySequence.instSMulNat {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { smul := fun (n : ) (x : ) => n x, }
noncomputable instance AdicCompletion.AdicCauchySequence.instSMulInt {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { smul := fun (n : ) (x : ) => n x, }
noncomputable instance AdicCompletion.AdicCauchySequence.instAddCommGroup {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
noncomputable instance AdicCompletion.AdicCauchySequence.instSMul {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = { smul := fun (r : R) (x : ) => r x, }
noncomputable instance AdicCompletion.AdicCauchySequence.instModule {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
Equations
• = let f := { toFun := Subtype.val, map_zero' := , map_add' := };
noncomputable instance AdicCompletion.AdicCauchySequence.instCoeFunForallNat {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :
CoeFun fun (x : ) => M
Equations
• = { coe := fun (f : ) => f }
@[simp]
theorem AdicCompletion.AdicCauchySequence.zero_apply {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (n : ) :
0 n = 0
@[simp]
theorem AdicCompletion.AdicCauchySequence.add_apply {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (f : ) (g : ) :
(f + g) n = f n + g n
@[simp]
theorem AdicCompletion.AdicCauchySequence.sub_apply {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (f : ) (g : ) :
(f - g) n = f n - g n
@[simp]
theorem AdicCompletion.AdicCauchySequence.smul_apply {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (n : ) (r : R) (f : ) :
(r f) n = r f n
theorem AdicCompletion.AdicCauchySequence.ext {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {x : } {y : } (h : ∀ (n : ), x n = y n) :
x = y
theorem AdicCompletion.AdicCauchySequence.ext_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {x : } {y : } :
x = y ∀ (n : ), x n = y n
theorem AdicCompletion.AdicCauchySequence.mk_eq_mk {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {m : } {n : } (hmn : m n) (f : ) :

The defining property of an adic cauchy sequence unwrapped.

theorem AdicCompletion.isAdicCauchy_iff {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : M) :
∀ (n : ), f n f (n + 1) [SMOD I ^ n ]

The I-adic cauchy condition can be checked on successive n.

noncomputable def AdicCompletion.AdicCauchySequence.mk {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : M) (h : ∀ (n : ), f n f (n + 1) [SMOD I ^ n ]) :

Construct I-adic cauchy sequence from sequence satisfying the successive cauchy condition.

Equations
• = f,
Instances For
@[simp]
theorem AdicCompletion.AdicCauchySequence.mk_coe {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : M) (h : ∀ (n : ), f n f (n + 1) [SMOD I ^ n ]) :
∀ (a : ), () a = f a
noncomputable def AdicCompletion.mk {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

The canonical linear map from cauchy sequences to the completion.

Equations
• = { toFun := fun (f : ) => fun (n : ) => (I ^ n ).mkQ (f n), , map_add' := , map_smul' := }
Instances For
@[simp]
theorem AdicCompletion.mk_apply_coe {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : ) (n : ) :
(() f) n = (I ^ n ).mkQ (f n)
theorem AdicCompletion.mk_zero_of {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] (f : ) (h : ∃ (k : ), nk, mn, ln, f m I ^ l ) :
() f = 0

Criterion for checking that an adic cauchy sequence is mapped to zero in the adic completion.

theorem AdicCompletion.mk_surjective {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] :

Every element in the adic completion is represented by a Cauchy sequence.

theorem AdicCompletion.induction_on {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] {p : Prop} (x : ) (h : ∀ (f : ), p (() f)) :
p x

To show a statement about an element of adicCompletion I M, it suffices to check it on Cauchy sequences.

noncomputable def AdicCompletion.lift {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] (f : (n : ) → M →ₗ[R] N I ^ n ) (h : ∀ {m n : } (hle : m n), ∘ₗ f n = f m) :

Lift a compatible family of linear maps M →ₗ[R] N ⧸ (I ^ n • ⊤ : Submodule R N) to the I-adic completion of M.

Equations
• = { toFun := fun (x : M) => fun (n : ) => (f n) x, , map_add' := , map_smul' := }
Instances For
@[simp]
theorem AdicCompletion.eval_lift {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] (f : (n : ) → M →ₗ[R] N I ^ n ) (h : ∀ {m n : } (hle : m n), ∘ₗ f n = f m) (n : ) :
∘ₗ = f n
@[simp]
theorem AdicCompletion.eval_lift_apply {R : Type u_1} [] (I : ) {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] (f : (n : ) → M →ₗ[R] N I ^ n ) (h : ∀ {m n : } (hle : m n), ∘ₗ f n = f m) (n : ) (x : M) :
(() x) n = (f n) x
noncomputable instance IsAdicComplete.bot {R : Type u_1} [] (M : Type u_2) [] [Module R M] :
Equations
• =
theorem IsAdicComplete.subsingleton {R : Type u_1} [] (M : Type u_2) [] [Module R M] (h : ) :
@[instance 100]
noncomputable instance IsAdicComplete.of_subsingleton {R : Type u_1} [] (I : ) (M : Type u_2) [] [Module R M] [] :
Equations
• =
theorem IsAdicComplete.le_jacobson_bot {R : Type u_1} [] (I : ) [] :
I .jacobson