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

theorem IsHausdorff.haus' {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [self : IsHausdorff I M] (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 • ⊤]

theorem IsPrecomplete.prec' {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] [self : 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 • ⊤]

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, inline]

noncomputable abbrev 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 • ⊤)

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

• AdicCompletion.transitionMap I M hmn = (I ^ n • ⊤).liftQ (I ^ m • ⊤).mkQ ⋯

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

• AdicCompletion I M = { f : (n : ℕ) → M ⧸ I ^ n • ⊤ // ∀ {m n : ℕ} (hmn : m ≤ n), (AdicCompletion.transitionMap I M hmn) (f n) = f m }

noncomputable 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 100]

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

noncomputable 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 = (⨅ (n : ℕ), I ^ n • ⊤).mkQ

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

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

Equations

• ⋯ = ⋯

noncomputable 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 = (⨅ (n : ℕ), I ^ n • ⊤).liftQ 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.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

noncomputable 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

• ⋯ = ⋯

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

noncomputable instance AdicCompletion.instZero {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Zero (AdicCompletion I M)

Equations

• AdicCompletion.instZero I M = { zero := ⟨0, ⋯⟩ }

noncomputable instance AdicCompletion.instAdd {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Add (AdicCompletion I M)

Equations

• AdicCompletion.instAdd I M = { add := fun (x y : AdicCompletion I M) => ⟨↑x + ↑y, ⋯⟩ }

noncomputable instance AdicCompletion.instNeg {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Neg (AdicCompletion I M)

Equations

• AdicCompletion.instNeg I M = { neg := fun (x : AdicCompletion I M) => ⟨-↑x, ⋯⟩ }

noncomputable instance AdicCompletion.instSub {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Sub (AdicCompletion I M)

Equations

• AdicCompletion.instSub I M = { sub := fun (x y : AdicCompletion I M) => ⟨↑x - ↑y, ⋯⟩ }

noncomputable instance AdicCompletion.instSMulNat {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul ℕ (AdicCompletion I M)

Equations

• AdicCompletion.instSMulNat I M = { smul := fun (n : ℕ) (x : AdicCompletion I M) => ⟨n • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.instSMulInt {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul ℤ (AdicCompletion I M)

Equations

• AdicCompletion.instSMulInt I M = { smul := fun (n : ℤ) (x : AdicCompletion I M) => ⟨n • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.instAddCommGroup {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AddCommGroup (AdicCompletion I M)

Equations

• AdicCompletion.instAddCommGroup I M = let f := Subtype.val; Function.Injective.addCommGroup f ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance AdicCompletion.instSMul {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul R (AdicCompletion I M)

Equations

• AdicCompletion.instSMul I M = { smul := fun (r : R) (x : AdicCompletion I M) => ⟨r • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.instModule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Module R (AdicCompletion I M)

Equations

• AdicCompletion.instModule I M = let f := { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }; Function.Injective.module R f ⋯ ⋯

noncomputable def AdicCompletion.incl {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AdicCompletion I M →ₗ[R] (n : ℕ) → M ⧸ I ^ n • ⊤

The canonical inclusion from the completion to the product.

Equations

• AdicCompletion.incl I M = { toFun := fun (x : AdicCompletion I M) => ↑x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AdicCompletion.incl_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (x : AdicCompletion I M) (n : ℕ) : (AdicCompletion.incl I M) x n = ↑x n

noncomputable 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

• AdicCompletion.of I M = { toFun := fun (x : M) => ⟨fun (n : ℕ) => (I ^ n • ⊤).mkQ x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[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 = (I ^ n • ⊤).mkQ x

noncomputable 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 = { 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) = (I ^ n • ⊤).mkQ 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 = (I ^ n • ⊤).mkQ

theorem AdicCompletion.eval_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(AdicCompletion.eval I M 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) = ⊤

@[simp]

theorem AdicCompletion.val_zero {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : ↑0 n = 0

@[simp]

theorem AdicCompletion.val_add {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (f : AdicCompletion I M) (g : AdicCompletion I M) : ↑(f + g) n = ↑f n + ↑g n

@[simp]

theorem AdicCompletion.val_sub {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (f : AdicCompletion I M) (g : AdicCompletion I M) : ↑(f - g) n = ↑f n - ↑g n

@[simp]

theorem AdicCompletion.val_sum {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {α : Type u_4} (s : Finset α) (f : α → AdicCompletion I M) (n : ℕ) : ↑(s.sum f) n = ∑ a ∈ s, ↑(f a) n

theorem AdicCompletion.val_smul {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (r : R) (f : AdicCompletion I M) : ↑(r • f) n = r • ↑f n

theorem AdicCompletion.ext_iff {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} : x = y ↔ ∀ (n : ℕ), ↑x n = ↑y 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 : ℕ), ↑x n = ↑y n) : x = y

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

Equations

• ⋯ = ⋯

@[simp]

theorem AdicCompletion.transitionMap_mk {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} (hmn : m ≤ n) (x : M) : (AdicCompletion.transitionMap I M hmn) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

@[simp]

theorem AdicCompletion.transitionMap_eq {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : AdicCompletion.transitionMap I M ⋯ = LinearMap.id

@[simp]

theorem AdicCompletion.transitionMap_comp {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : AdicCompletion.transitionMap I M hmn ∘ₗ AdicCompletion.transitionMap I M hnk = AdicCompletion.transitionMap I M ⋯

@[simp]

theorem AdicCompletion.transitionMap_comp_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} {k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) (x : M ⧸ I ^ k • ⊤) : (AdicCompletion.transitionMap I M hmn) ((AdicCompletion.transitionMap I M hnk) x) = (AdicCompletion.transitionMap I M ⋯) x

@[simp]

theorem AdicCompletion.transitionMap_comp_eval_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I M) : (AdicCompletion.transitionMap I M hmn) (↑x n) = ↑x m

@[simp]

theorem AdicCompletion.transitionMap_comp_eval {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} (hmn : m ≤ n) : AdicCompletion.transitionMap I M hmn ∘ₗ AdicCompletion.eval I M n = AdicCompletion.eval I M m

noncomputable def AdicCompletion.IsAdicCauchy {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : ℕ → M) : Prop

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

Equations

• AdicCompletion.IsAdicCauchy I M f = ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]

noncomputable def AdicCompletion.AdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Type u_2

The type of I-adic Cauchy sequences.

Equations

• AdicCompletion.AdicCauchySequence I M = { f : ℕ → M // AdicCompletion.IsAdicCauchy I M f }

noncomputable def AdicCompletion.AdicCauchySequence.submodule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Submodule R (ℕ → M)

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

Equations

• AdicCompletion.AdicCauchySequence.submodule I M = { carrier := {f : ℕ → M | AdicCompletion.IsAdicCauchy I M f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable instance AdicCompletion.AdicCauchySequence.instZero {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Zero (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instZero I M = { zero := ⟨0, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instAdd {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Add (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instAdd I M = { add := fun (x y : AdicCompletion.AdicCauchySequence I M) => ⟨↑x + ↑y, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instNeg {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Neg (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instNeg I M = { neg := fun (x : AdicCompletion.AdicCauchySequence I M) => ⟨-↑x, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instSub {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Sub (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instSub I M = { sub := fun (x y : AdicCompletion.AdicCauchySequence I M) => ⟨↑x - ↑y, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instSMulNat {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul ℕ (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instSMulNat I M = { smul := fun (n : ℕ) (x : AdicCompletion.AdicCauchySequence I M) => ⟨n • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instSMulInt {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul ℤ (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instSMulInt I M = { smul := fun (n : ℤ) (x : AdicCompletion.AdicCauchySequence I M) => ⟨n • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instAddCommGroup {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AddCommGroup (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instAddCommGroup I M = let f := Subtype.val; Function.Injective.addCommGroup f ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable instance AdicCompletion.AdicCauchySequence.instSMul {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : SMul R (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instSMul I M = { smul := fun (r : R) (x : AdicCompletion.AdicCauchySequence I M) => ⟨r • ↑x, ⋯⟩ }

noncomputable instance AdicCompletion.AdicCauchySequence.instModule {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Module R (AdicCompletion.AdicCauchySequence I M)

Equations

• AdicCompletion.AdicCauchySequence.instModule I M = let f := { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }; Function.Injective.module R f ⋯ ⋯

noncomputable instance AdicCompletion.AdicCauchySequence.instCoeFunForallNat {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : CoeFun (AdicCompletion.AdicCauchySequence I M) fun (x : AdicCompletion.AdicCauchySequence I M) => ℕ → M

Equations

• AdicCompletion.AdicCauchySequence.instCoeFunForallNat I M = { coe := fun (f : AdicCompletion.AdicCauchySequence I M) => ↑f }

@[simp]

theorem AdicCompletion.AdicCauchySequence.zero_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : ↑0 n = 0

@[simp]

theorem AdicCompletion.AdicCauchySequence.add_apply {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (f : AdicCompletion.AdicCauchySequence I M) (g : AdicCompletion.AdicCauchySequence I M) : ↑(f + g) n = ↑f n + ↑g n

@[simp]

theorem AdicCompletion.AdicCauchySequence.sub_apply {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (f : AdicCompletion.AdicCauchySequence I M) (g : AdicCompletion.AdicCauchySequence I M) : ↑(f - g) n = ↑f n - ↑g n

@[simp]

theorem AdicCompletion.AdicCauchySequence.smul_apply {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) (r : R) (f : AdicCompletion.AdicCauchySequence I M) : ↑(r • f) n = r • ↑f n

theorem AdicCompletion.AdicCauchySequence.ext_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {x : AdicCompletion.AdicCauchySequence I M} {y : AdicCompletion.AdicCauchySequence I M} : x = y ↔ ∀ (n : ℕ), ↑x n = ↑y n

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

theorem AdicCompletion.AdicCauchySequence.mk_eq_mk {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} (hmn : m ≤ n) (f : AdicCompletion.AdicCauchySequence I M) : Submodule.Quotient.mk (↑f n) = Submodule.Quotient.mk (↑f m)

The defining property of an adic cauchy sequence unwrapped.

theorem AdicCompletion.isAdicCauchy_iff {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : ℕ → M) : AdicCompletion.IsAdicCauchy I M f ↔ ∀ (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} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : ℕ → M) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) : AdicCompletion.AdicCauchySequence I M

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

Equations

• AdicCompletion.AdicCauchySequence.mk I M f h = ⟨f, ⋯⟩

@[simp]

theorem AdicCompletion.AdicCauchySequence.mk_coe {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : ℕ → M) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) : ∀ (a : ℕ), ↑(AdicCompletion.AdicCauchySequence.mk I M f h) a = f a

noncomputable def AdicCompletion.mk {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : AdicCompletion.AdicCauchySequence I M →ₗ[R] AdicCompletion I M

The canonical linear map from cauchy sequences to the completion.

Equations

• AdicCompletion.mk I M = { toFun := fun (f : AdicCompletion.AdicCauchySequence I M) => ⟨fun (n : ℕ) => (I ^ n • ⊤).mkQ (↑f n), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AdicCompletion.mk_apply_coe {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : AdicCompletion.AdicCauchySequence I M) (n : ℕ) : ↑((AdicCompletion.mk I M) f) n = (I ^ n • ⊤).mkQ (↑f n)

theorem AdicCompletion.mk_zero_of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (f : AdicCompletion.AdicCauchySequence I M) (h : ∃ (k : ℕ), ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤) : (AdicCompletion.mk I M) 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} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Function.Surjective ⇑(AdicCompletion.mk I M)

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

theorem AdicCompletion.induction_on {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] {p : AdicCompletion I M → Prop} (x : AdicCompletion I M) (h : ∀ (f : AdicCompletion.AdicCauchySequence I M), p ((AdicCompletion.mk I M) 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} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) : M →ₗ[R] AdicCompletion I N

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

Equations

• AdicCompletion.lift I f h = { toFun := fun (x : M) => ⟨fun (n : ℕ) => (f n) x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AdicCompletion.eval_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] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) : AdicCompletion.eval I N n ∘ₗ AdicCompletion.lift I f ⋯ = f n

@[simp]

theorem AdicCompletion.eval_lift_apply {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] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) (x : M) : ↑((AdicCompletion.lift I f ⋯) x) n = (f n) x

noncomputable 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 100]

noncomputable 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 ≤ ⊥.jacobson