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 with a linear map AdicCompletion.lift from M. This map is injective iff M is Hausdorff and surjective iff M is precomplete.
• IsAdicComplete.lift: if N is I-adically complete, then a compatible family of linear maps M →ₗ[R] N ⧸ (I ^ n • ⊤) can be lifted to a unique linear map M →ₗ[R] N. Together with mk_lift_apply and eq_lift, it gives the universal property of being I-adically complete.

class IsHausdorff {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [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_4) [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_4) [AddCommGroup M] [Module R M] extends IsHausdorff I M, IsPrecomplete I M : Prop

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

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

theorem isAdicComplete_iff {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] : IsAdicComplete I M ↔ IsHausdorff I M ∧ IsPrecomplete I M

theorem IsHausdorff.haus {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [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_4} [AddCommGroup M] [Module R M] : IsHausdorff I M ↔ ∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0

theorem IsHausdorff.eq_iff_smodEq {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [IsHausdorff I M] {x y : M} : x = y ↔ ∀ (n : ℕ), x ≡ y [SMOD I ^ n • ⊤]

theorem IsHausdorff.map_algebraMap_iff {R : Type u_1} {S : Type u_2} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [CommRing S] [Module S M] [Algebra R S] [IsScalarTower R S M] : IsHausdorff (Ideal.map (algebraMap R S) I) M ↔ IsHausdorff I M

theorem IsHausdorff.of_map {R : Type u_1} {S : Type u_2} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [CommRing S] [Module S M] {J : Ideal S} [Algebra R S] [IsScalarTower R S M] (hIJ : Ideal.map (algebraMap R S) I ≤ J) [IsHausdorff J M] : IsHausdorff I M

theorem IsHausdorff.funext {R : Type u_1} [CommRing R] (I : Ideal R) {N : Type u_5} [AddCommGroup N] [Module R N] {M : Type u_6} [IsHausdorff I N] {f g : M → N} (h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)) : f = g

theorem IsHausdorff.StrictMono.funext {R : Type u_1} [CommRing R] (I : Ideal R) {N : Type u_5} [AddCommGroup N] [Module R N] {M : Type u_6} [IsHausdorff I N] {f g : M → N} {a : ℕ → ℕ} (ha : StrictMono a) (h : ∀ (n : ℕ) (m : M), Submodule.Quotient.mk (f m) = Submodule.Quotient.mk (g m)) : f = g

theorem IsHausdorff.funext' {R : Type u_6} {S : Type u_7} [CommRing S] (I : Ideal S) [IsHausdorff I S] {f g : R → S} (h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ n)) (f r) = (Ideal.Quotient.mk (I ^ n)) (g r)) : f = g

A variant of IsHausdorff.funext, where the target is a ring instead of a module.

theorem IsHausdorff.StrictMono.funext' {R : Type u_6} {S : Type u_7} [CommRing S] (I : Ideal S) [IsHausdorff I S] {f g : R → S} {a : ℕ → ℕ} (ha : StrictMono a) (h : ∀ (n : ℕ) (r : R), (Ideal.Quotient.mk (I ^ a n)) (f r) = (Ideal.Quotient.mk (I ^ a n)) (g r)) : f = g

A variant of IsHausdorff.StrictMono.funext, where the target is a ring instead of a module.

theorem IsPrecomplete.prec {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [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_4} [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.map_algebraMap_iff {R : Type u_1} {S : Type u_2} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [CommRing S] [Module S M] [Algebra R S] [IsScalarTower R S M] : IsPrecomplete (Ideal.map (algebraMap R S) I) M ↔ IsPrecomplete I M

@[reducible, inline]

noncomputable abbrev Hausdorffification {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] : Type u_4

The Hausdorffification of a module with respect to an ideal.

Equations

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

@[reducible, inline]

noncomputable abbrev AdicCompletion.transitionMap {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [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 = Submodule.factorPow I M hmn

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

The completion of a module with respect to an ideal.

This is Hausdorff but not necessarily complete: a classical sufficient condition for completeness is that I be finitely generated [Stacks, 05GG].

Equations

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

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

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

@[instance 100]

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

theorem IsHausdorff.iInf_pow_smul {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [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_4) [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_4} [AddCommGroup M] [Module R M] {C : Hausdorffification I M → Prop} (x : Hausdorffification I M) (ih : ∀ (x : M), C ((of I M) x)) : C x

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

noncomputable def Hausdorffification.lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [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_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) (x : M) : (lift I f) ((of I M) x) = f x

theorem Hausdorffification.lift_comp_of {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) : lift I f ∘ₗ of I M = f

theorem Hausdorffification.lift_eq {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [h : IsHausdorff I N] (f : M →ₗ[R] N) (g : Hausdorffification I M →ₗ[R] N) (hg : g ∘ₗ of I M = f) : g = lift I f

Uniqueness of lift.

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

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

@[instance 100]

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

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

theorem AdicCompletion.val_zero_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [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_4} [AddCommGroup M] [Module R M] (f g : AdicCompletion I M) : ↑(f + g) = ↑f + ↑g

@[simp]

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

@[simp]

theorem AdicCompletion.val_neg {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] (f : AdicCompletion I M) : ↑(-f) = -↑f

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

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

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

theorem AdicCompletion.val_smul {R : Type u_1} {S : Type u_2} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (s : S) (f : AdicCompletion I M) : ↑(s • f) = s • ↑f

theorem AdicCompletion.val_smul_apply {R : Type u_1} {S : Type u_2} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (s : S) (f : AdicCompletion I M) (n : ℕ) : ↑(s • f) n = s • ↑f n

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

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

@[instance_reducible]

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

Equations

• AdicCompletion.instAddCommGroup I M = Function.Injective.addCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance AdicCompletion.instModuleOfIsScalarTower {R : Type u_1} {S : Type u_2} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S (AdicCompletion I M)

Equations

• AdicCompletion.instModuleOfIsScalarTower I M = Function.Injective.module S { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

instance AdicCompletion.instIsScalarTower {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [SMul S T] [SMul S R] [SMul T R] [SMul S M] [SMul T M] [IsScalarTower S R M] [IsScalarTower T R M] [IsScalarTower S T M] : IsScalarTower S T (AdicCompletion I M)

instance AdicCompletion.instSMulCommClass {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [SMul S R] [SMul T R] [SMul S M] [SMul T M] [IsScalarTower S R M] [IsScalarTower T R M] [SMulCommClass S T M] : SMulCommClass S T (AdicCompletion I M)

instance AdicCompletion.instIsCentralScalar {R : Type u_1} {S : Type u_2} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [SMul S R] [SMul Sᵐᵒᵖ R] [SMul S M] [SMul Sᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S (AdicCompletion I M)

noncomputable def AdicCompletion.incl {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [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_4) [AddCommGroup M] [Module R M] (x : AdicCompletion I M) (n : ℕ) : (incl I M) x n = ↑x n

@[simp]

theorem AdicCompletion.val_sum {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {ι : Type u_6} (s : Finset ι) (f : ι → AdicCompletion I M) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

theorem AdicCompletion.val_sum_apply {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {ι : Type u_6} (s : Finset ι) (f : ι → AdicCompletion I M) (n : ℕ) : ↑(∑ i ∈ s, f i) n = ∑ i ∈ s, ↑(f i) n

noncomputable def AdicCompletion.of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [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_4) [AddCommGroup M] [Module R M] (x : M) (n : ℕ) : ↑((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_4) [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_4) [AddCommGroup M] [Module R M] (n : ℕ) : ⇑(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_4) [AddCommGroup M] [Module R M] (n : ℕ) (f : AdicCompletion I M) : (eval I M n) f = ↑f n

theorem AdicCompletion.eval_of {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] (n : ℕ) (x : M) : (eval I M n) ((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_4) [AddCommGroup M] [Module R M] (n : ℕ) : eval I M n ∘ₗ of I M = (I ^ n • ⊤).mkQ

theorem AdicCompletion.eval_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] (n : ℕ) : Function.Surjective ⇑(eval I M n)

@[simp]

theorem AdicCompletion.range_eval {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] (n : ℕ) : (eval I M n).range = ⊤

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

@[simp]

theorem AdicCompletion.transitionMap_comp_eval_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I M) : (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_4) [AddCommGroup M] [Module R M] {m n : ℕ} (hmn : m ≤ n) : transitionMap I M hmn ∘ₗ eval I M n = eval I M m

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

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_4) [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' := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• AdicCompletion.AdicCauchySequence.instAddCommGroup I M = Function.Injective.addCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

noncomputable instance AdicCompletion.AdicCauchySequence.instCoeFunForallNat {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] : CoeFun (AdicCauchySequence I M) fun (x : 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_4) [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_4} [AddCommGroup M] [Module R M] (n : ℕ) (f g : 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_4} [AddCommGroup M] [Module R M] (n : ℕ) (f g : 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_4} [AddCommGroup M] [Module R M] (n : ℕ) (r : R) (f : AdicCauchySequence I M) : ↑(r • f) n = r • ↑f n

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

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

theorem AdicCompletion.AdicCauchySequence.mk_eq_mk {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {m n : ℕ} (hmn : m ≤ n) (f : 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_4) [AddCommGroup M] [Module R M] (f : ℕ → M) : 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_4) [AddCommGroup M] [Module R M] (f : ℕ → M) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) : 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_4) [AddCommGroup M] [Module R M] (f : ℕ → M) (h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) (a✝ : ℕ) : ↑(mk I M f h) a✝ = f a✝

noncomputable def AdicCompletion.mk {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] : 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_4) [AddCommGroup M] [Module R M] (f : AdicCauchySequence I M) (n : ℕ) : ↑((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_4) [AddCommGroup M] [Module R M] (f : AdicCauchySequence I M) (h : ∃ (k : ℕ), ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤) : (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_4) [AddCommGroup M] [Module R M] : Function.Surjective ⇑(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_4) [AddCommGroup M] [Module R M] {p : AdicCompletion I M → Prop} (x : AdicCompletion I M) (h : ∀ (f : AdicCauchySequence I M), p ((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_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), 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_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) : eval I N n ∘ₗ lift I f ⋯ = f n

@[simp]

theorem AdicCompletion.eval_lift_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) (n : ℕ) (x : M) : ↑((lift I f ⋯) x) n = (f n) x

theorem AdicCompletion.lift_add {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (f g : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (hf : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) (hg : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ g n = g m) : lift I (f + g) ⋯ = lift I f ⋯ + lift I g ⋯

theorem AdicCompletion.lift_smul {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (c : R) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (hf : ∀ {m n : ℕ} (hle : m ≤ n), transitionMap I N hle ∘ₗ f n = f m) : lift I (c • f) ⋯ = c • lift I f ⋯

theorem AdicCompletion.of_injective_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] : Function.Injective ⇑(of I M) ↔ IsHausdorff I M

theorem AdicCompletion.of_injective {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [IsHausdorff I M] : Function.Injective ⇑(of I M)

@[simp]

theorem AdicCompletion.of_inj {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] [IsHausdorff I M] {a b : M} : (of I M) a = (of I M) b ↔ a = b

theorem AdicCompletion.of_surjective_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] : Function.Surjective ⇑(of I M) ↔ IsPrecomplete I M

theorem AdicCompletion.of_surjective {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [IsPrecomplete I M] : Function.Surjective ⇑(of I M)

theorem AdicCompletion.of_bijective_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] : Function.Bijective ⇑(of I M) ↔ IsAdicComplete I M

theorem AdicCompletion.of_bijective {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [IsAdicComplete I M] : Function.Bijective ⇑(of I M)

noncomputable def AdicCompletion.ofLinearEquiv {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [IsAdicComplete I M] : M ≃ₗ[R] AdicCompletion I M

When M is I-adic complete, the canonical map from M to its I-adic completion is a linear equivalence.

Equations

• AdicCompletion.ofLinearEquiv I M = LinearEquiv.ofBijective (AdicCompletion.of I M) ⋯

@[simp]

theorem AdicCompletion.ofLinearEquiv_apply {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [IsAdicComplete I M] (x : M) : (ofLinearEquiv I M) x = (of I M) x

@[simp]

theorem AdicCompletion.ofLinearEquiv_symm_of {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] [IsAdicComplete I M] (x : M) : (ofLinearEquiv I M).symm ((of I M) x) = x

@[simp]

theorem AdicCompletion.of_ofLinearEquiv_symm {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] [IsAdicComplete I M] (x : AdicCompletion I M) : (of I M) ((ofLinearEquiv I M).symm x) = x

theorem AdicCompletion.pow_smul_top_le_ker_eval {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] (n : ℕ) : I ^ n • ⊤ ≤ (eval I M n).ker

theorem AdicCompletion.val_apply_mem_smul_top_iff {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {m n : ℕ} {x : AdicCompletion I M} (m_ge : n ≤ m) : ↑x m ∈ I ^ n • ⊤ ↔ ↑x n = 0

theorem IsAdicComplete.map_algebraMap_iff {R : Type u_1} {S : Type u_2} [CommRing R] (I : Ideal R) (M : Type u_4) [AddCommGroup M] [Module R M] [CommRing S] [Module S M] [Algebra R S] [IsScalarTower R S M] : IsAdicComplete (Ideal.map (algebraMap R S) I) M ↔ IsAdicComplete I M

noncomputable def IsAdicComplete.lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) : M →ₗ[R] N

Universal property of IsAdicComplete. The lift linear map lift I f h : M →ₗ[R] N of a sequence of compatible linear maps f n : M →ₗ[R] N ⧸ (I ^ n • ⊤).

Equations

• IsAdicComplete.lift I f h = ↑(AdicCompletion.ofLinearEquiv I N).symm ∘ₗ AdicCompletion.lift I f ⋯

@[simp]

theorem IsAdicComplete.of_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) (x : M) : (AdicCompletion.of I N) ((lift I f ⋯) x) = (AdicCompletion.lift I f ⋯) x

@[simp]

theorem IsAdicComplete.of_comp_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) : AdicCompletion.of I N ∘ₗ lift I f ⋯ = AdicCompletion.lift I f ⋯

@[simp]

theorem IsAdicComplete.mk_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) (n : ℕ) (x : M) : Submodule.Quotient.mk ((lift I f ⋯) x) = (f n) x

The composition of lift linear map lift I f h : M →ₗ[R] N with the canonical projection N → N ⧸ (I ^ n • ⊤) is f n .

@[simp]

theorem IsAdicComplete.mkQ_comp_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) (n : ℕ) : (I ^ n • ⊤).mkQ ∘ₗ lift I f ⋯ = f n

The composition of lift linear map lift I f h : M →ₗ[R] N with the canonical projection N →ₗ[R] N ⧸ (I ^ n • ⊤) is f n.

theorem IsAdicComplete.eq_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] [IsAdicComplete I N] {f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤} (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m) {F : M →ₗ[R] N} (hF : ∀ (n : ℕ), (I ^ n • ⊤).mkQ ∘ₗ F = f n) : F = lift I f ⋯

Uniqueness of the lift. Given a compatible family of linear maps f n : M →ₗ[R] N ⧸ (I ^ n • ⊤). If F : M →ₗ[R] N makes the following diagram commute

  N
  | \
 F|  \ f n
  |   \
  v    v
  M --> M ⧸ (I ^ n • ⊤)

Then it is the map IsAdicComplete.lift.

noncomputable def IsAdicComplete.StrictMono.extend {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (n : ℕ) : M →ₗ[R] N ⧸ I ^ n • ⊤

Instead of providing all M →ₗ[R] N ⧸ (I ^ n • ⊤), one can just provide M →ₗ[R] N ⧸ (I ^ (a n) • ⊤) for a strictly increasing sequence a n to recover all M →ₗ[R] N ⧸ (I ^ n • ⊤).

Equations

• IsAdicComplete.StrictMono.extend ha f n = Submodule.factorPow I N ⋯ ∘ₗ f n

theorem IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) {m n : ℕ} (hle : m ≤ n) : Submodule.factorPow I N ⋯ ∘ₗ f n = f m

theorem IsAdicComplete.StrictMono.extend_eq {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) (n : ℕ) : extend ha f (a n) = f n

theorem IsAdicComplete.StrictMono.factorPow_comp_extend {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) {m n : ℕ} (hle : m ≤ n) : Submodule.factorPow I N hle ∘ₗ extend ha f n = extend ha f m

noncomputable def IsAdicComplete.StrictMono.lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] : M →ₗ[R] N

A variant of IsAdicComplete.lift. Only takes f n : M →ₗ[R] N ⧸ (I ^ (a n) • ⊤) from a strictly increasing sequence a n.

Equations

• IsAdicComplete.StrictMono.lift I ha f hf = IsAdicComplete.lift I (IsAdicComplete.StrictMono.extend ha f) ⋯

theorem IsAdicComplete.StrictMono.of_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] (x : M) : (AdicCompletion.of I N) ((lift I ha f ⋯) x) = (AdicCompletion.lift I (extend ha f) ⋯) x

theorem IsAdicComplete.StrictMono.of_comp_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] : AdicCompletion.of I N ∘ₗ lift I ha f ⋯ = AdicCompletion.lift I (extend ha f) ⋯

@[simp]

theorem IsAdicComplete.StrictMono.mk_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] {n : ℕ} (x : M) : Submodule.Quotient.mk ((lift I ha f ⋯) x) = (f n) x

@[simp]

theorem IsAdicComplete.StrictMono.mkQ_comp_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] {n : ℕ} : (I ^ a n • ⊤).mkQ ∘ₗ lift I ha f ⋯ = f n

theorem IsAdicComplete.StrictMono.eq_lift {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_4} [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] {a : ℕ → ℕ} (ha : StrictMono a) (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m) [IsAdicComplete I N] {F : M →ₗ[R] N} (hF : ∀ (n : ℕ), (I ^ a n • ⊤).mkQ ∘ₗ F = f n) : F = lift I ha f ⋯

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

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

@[instance 100]

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

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