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 #

is_Hausdorff I M: this says that the intersection of I^n M is 0.
is_precomplete I M: this says that every Cauchy sequence converges.
is_adic_complete I M: this says that M is Hausdorff and precomplete.
Hausdorffification I M: this is the universal Hausdorff module with a map from M.
completion 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.

source

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

haus' : ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0

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

Instances of this typeclass

source

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

prec' : ∀ (f : ℕ → M), (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → (∃ (L : M), ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤])

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

Instances of this typeclass

source

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

to_is_Hausdorff : is_Hausdorff I M
to_is_precomplete : is_precomplete I M

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

Instances of this typeclass

source

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

source

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

source

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 • ⊤])

source

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 • ⊤])

source

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

Hausdorffification I M = (M ⧸ ⨅ (n : ℕ), I ^ n • ⊤)

source

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

adic_completion I M = {carrier := {f : Π (n : ℕ), M ⧸ I ^ n • ⊤ | ∀ {m n : ℕ} (h : m ≤ n), ⇑((I ^ n • ⊤).liftq (I ^ m • ⊤).mkq _) (f n) = f m}, add_mem' := _, zero_mem' := _, smul_mem' := _}

Instances for ↥adic_completion

adic_completion.is_Hausdorff

source

@[protected, instance]

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

is_Hausdorff ⊥ M

source

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

subsingleton M

source

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

is_Hausdorff I M

source

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 • ⊤) = ⊥

source

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

M →ₗ[R] Hausdorffification I M

The canonical linear map to the Hausdorffification.

Equations

Hausdorffification.of I M = (⨅ (n : ℕ), I ^ n • ⊤).mkq

source

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

source

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

is_Hausdorff I (Hausdorffification I M)

source

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

Hausdorffification I M →ₗ[R] N

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

Equations

Hausdorffification.lift I f = (⨅ (n : ℕ), I ^ n • ⊤).liftq f _

source

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

⇑(Hausdorffification.lift I f) (⇑(Hausdorffification.of I M) x) = ⇑f x

source

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

(Hausdorffification.lift I f).comp (Hausdorffification.of I M) = f

source

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

g = Hausdorffification.lift I f

Uniqueness of lift.

source

@[protected, instance]

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

is_precomplete ⊥ M

source

@[protected, instance]

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

is_precomplete ⊤ M

source

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

is_precomplete I M

source

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

M →ₗ[R] ↥(adic_completion I M)

The canonical linear map to the completion.

Equations

adic_completion.of I M = {to_fun := λ (x : M), ⟨λ (n : ℕ), ⇑((I ^ n • ⊤).mkq) x, _⟩, map_add' := _, map_smul' := _}

source

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

source

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

↥(adic_completion I M) →ₗ[R] M ⧸ I ^ n • ⊤

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

Equations

adic_completion.eval I M n = {to_fun := λ (f : ↥(adic_completion I M)), f.val n, map_add' := _, map_smul' := _}

source

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

source

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

⇑(adic_completion.eval I M n) f = f.val n

source

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

⇑(adic_completion.eval I M n) (⇑(adic_completion.of I M) x) = ⇑((I ^ n • ⊤).mkq) x

source

@[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 : ℕ) :

(adic_completion.eval I M n).comp (adic_completion.of I M) = (I ^ n • ⊤).mkq

source

@[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 : ℕ) :

linear_map.range (adic_completion.eval I M n) = ⊤

source

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

source

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

is_Hausdorff I ↥(adic_completion I M)

source

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

is_adic_complete ⊥ M

source

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

subsingleton M

source

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

is_adic_complete I M

source

theorem is_adic_complete.le_jacobson_bot {R : Type u_1} [comm_ring R] (I : ideal R) [is_adic_complete I R] :

I ≤ ⊥.jacobson