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} [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.

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.

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.

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

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

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

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

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

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• @IsHausdorff.bot = @IsHausdorff.bot.proof_1

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

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

Equations

• @IsHausdorff.of_subsingleton = @IsHausdorff.of_subsingleton.proof_1

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

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.

Equations

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

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

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)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Hausdorffification.lift I f = Submodule.liftQ (⨅ (n : ℕ), I ^ n • ⊤) f (_ : ⨅ (n : ℕ), I ^ n • ⊤ ≤ Submodule.comap f ⊥)

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

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

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.

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

Equations

• @IsPrecomplete.bot = @IsPrecomplete.bot.proof_1

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

Equations

• @IsPrecomplete.top = @IsPrecomplete.top.proof_1

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

Equations

• @IsPrecomplete.of_subsingleton = @IsPrecomplete.of_subsingleton.proof_1

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.

Equations

• One or more equations did not get rendered due to their size.

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

@[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 • ⊤)

@[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) = ⊤

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

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 }

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• @IsAdicComplete.bot = @IsAdicComplete.bot.proof_1

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

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

Equations

• @IsAdicComplete.of_subsingleton = @IsAdicComplete.of_subsingleton.proof_1

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