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

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

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

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

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

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

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 : M), ∀ (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 : M), ∀ (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

• ⋯ = ⋯

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

• ⋯ = ⋯

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.instIsHausdorffHausdorffificationAddCommGroupToRingIInfSubmoduleToSemiringToCommSemiringToAddCommMonoidNatInstInfSetSubmoduleHSMulIdealInstHSMulHasSMul'HPowInstHPowToNatPowToMonoidToMonoidWithZeroToSemiringIdemSemiringIdTopInstTopSubmoduleModule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : IsHausdorff I (Hausdorffification I M)

Equations

• ⋯ = ⋯

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 ⋯

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

def adicCompletion.of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : M →ₗ[R] ↥(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 : ℕ) : ↥(adicCompletion I M) →ₗ[R] M ⧸ I ^ n • ⊤

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

Equations

• adicCompletion.eval I M n = { toAddHom := { toFun := fun (f : ↥(adicCompletion I M)) => ↑f n, map_add' := ⋯ }, map_smul' := ⋯ }

@[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 : ↥(adicCompletion I M)) => ↑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 : ↥(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 : ℕ) : 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 : ↥(adicCompletion I M)} {y : ↥(adicCompletion I M)} (h : ∀ (n : ℕ), (adicCompletion.eval I M n) x = (adicCompletion.eval I M n) y) : x = y

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

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