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.

source

class IsHausdorff {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup 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

source

class IsPrecomplete {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

Prop

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

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

Instances

source

class IsAdicComplete {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] extends IsHausdorff , IsPrecomplete :

Prop

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

Instances

source

theorem IsHausdorff.haus {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] :

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

source

theorem isHausdorff_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] :

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

source

theorem IsPrecomplete.prec {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] :

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

source

theorem isPrecomplete_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] :

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

source

@[reducible]

def Hausdorffification {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

Type u_2

The Hausdorffification of a module with respect to an ideal.

Instances For

source

def adicCompletion {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup 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.

Instances For

source

instance IsHausdorff.bot {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

IsHausdorff ⊥ M

source

theorem IsHausdorff.subsingleton {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (h : IsHausdorff ⊤ M) :

Subsingleton M

source

instance IsHausdorff.of_subsingleton {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [Subsingleton M] :

IsHausdorff I M

source

theorem IsHausdorff.iInf_pow_smul {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (h : IsHausdorff I M) :

⨅ (n : ℕ), I ^ n • ⊤ = ⊥

source

def Hausdorffification.of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

M →ₗ[R] Hausdorffification I M

The canonical linear map to the Hausdorffification.

Instances For

source

theorem Hausdorffification.induction_on {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup 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

instance Hausdorffification.instIsHausdorffHausdorffificationAddCommGroupToRingIInfSubmoduleToSemiringToCommSemiringToAddCommMonoidInstInfSetSubmoduleNatHSMulIdealInstHSMulHasSMul'HPowInstHPowPowToMonoidToMonoidWithZeroToSemiringIdemSemiringIdTopInstTopSubmoduleModule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

IsHausdorff I (Hausdorffification I M)

source

def Hausdorffification.lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [h : IsHausdorff 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.

Instances For

source

theorem Hausdorffification.lift_of {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [h : IsHausdorff 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} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) :

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

source

theorem Hausdorffification.lift_eq {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) (g : Hausdorffification I M →ₗ[R] N) (hg : LinearMap.comp g (Hausdorffification.of I M) = f) :

g = Hausdorffification.lift I f

Uniqueness of lift.

source

instance IsPrecomplete.bot {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

IsPrecomplete ⊥ M

source

instance IsPrecomplete.top {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

IsPrecomplete ⊤ M

source

instance IsPrecomplete.of_subsingleton {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [Subsingleton M] :

IsPrecomplete I M

source

def adicCompletion.of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

M →ₗ[R] { x // x ∈ adicCompletion I M }

The canonical linear map to the completion.

Instances For

source

@[simp]

theorem adicCompletion.of_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (x : M) (n : ℕ) :

↑(↑(adicCompletion.of I M) x) n = ↑(Submodule.mkQ (I ^ n • ⊤)) x

source

def adicCompletion.eval {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) :

{ x // x ∈ adicCompletion I M } →ₗ[R] M ⧸ I ^ n • ⊤

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

Instances For

source

@[simp]

theorem adicCompletion.coe_eval {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) :

↑(adicCompletion.eval I M n) = fun f => ↑f n

source

theorem adicCompletion.eval_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) (f : { x // x ∈ adicCompletion I M }) :

↑(adicCompletion.eval I M n) f = ↑f n

source

theorem adicCompletion.eval_of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) (x : M) :

↑(adicCompletion.eval I M n) (↑(adicCompletion.of I M) x) = ↑(Submodule.mkQ (I ^ n • ⊤)) x

source

@[simp]

theorem adicCompletion.eval_comp_of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) :

LinearMap.comp (adicCompletion.eval I M n) (adicCompletion.of I M) = Submodule.mkQ (I ^ n • ⊤)

source

@[simp]

theorem adicCompletion.range_eval {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) :

LinearMap.range (adicCompletion.eval I M n) = ⊤

source

theorem adicCompletion.ext {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {x : { x // x ∈ adicCompletion I M }} {y : { x // x ∈ adicCompletion I M }} (h : ∀ (n : ℕ), ↑(adicCompletion.eval I M n) x = ↑(adicCompletion.eval I M n) y) :

x = y

source

instance adicCompletion.instIsHausdorffSubtypeForAllNatQuotientSubmoduleToSemiringToCommSemiringToAddCommMonoidHasQuotientToRingHSMulIdealInstHSMulHasSMul'HPowInstHPowPowToMonoidToMonoidWithZeroToSemiringIdemSemiringIdTopInstTopSubmoduleMemAddCommMonoidAddCommGroupModuleModuleInstMembershipSetLikeAdicCompletionAddCommGroupAddCommGroupModule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] :

IsHausdorff I { x // x ∈ adicCompletion I M }

source

instance IsAdicComplete.bot {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] :

IsAdicComplete ⊥ M

source

theorem IsAdicComplete.subsingleton {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (h : IsAdicComplete ⊤ M) :

Subsingleton M

source

instance IsAdicComplete.of_subsingleton {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [Subsingleton M] :

IsAdicComplete I M

source

theorem IsAdicComplete.le_jacobson_bot {R : Type u_1} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :

I ≤ Ideal.jacobson ⊥