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.

source

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

Instances

source

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

Instances

source

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

Instances

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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 M be finitely generated [Stacks, 0G1Q].

Equations

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

Instances For

source

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

IsHausdorff ⊥ M

source

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

Subsingleton M

source

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

source

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

source

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

Instances For

source

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

source

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)

source

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 ⋯

Instances For

source

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

source

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

source

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.

source

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

IsPrecomplete ⊥ M

source

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

IsPrecomplete ⊤ M

source

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

source

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.

Instances For

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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

source

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)

source

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)

source

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)

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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)

source

@[simp]

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

LinearMap.range (eval I M n) = ⊤

source

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)

source

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

source

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

source

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

Instances For

source

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 }

Instances For

source

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

Instances For

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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, ⋯⟩ }

source

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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, ⋯⟩ }

source

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

source

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 }

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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, ⋯⟩

Instances For

source

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

source

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

Instances For

source

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

source

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.

source

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.

source

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.

source

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

Instances For

source

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

source

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

source

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

source

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)

source

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

source

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

source

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)

source

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

source

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)

source

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

Instances For

source

@[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] (a✝ : M) :

(ofLinearEquiv I M) a✝ = (of I M) a✝

source

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

source

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

source

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 ⋯

Instances For

source

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

source

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

source

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

source

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

source

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 commutes

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

Then it is the map IsAdicComplete.lift.

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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 ⋯

source

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

IsAdicComplete ⊥ M

source

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

Subsingleton M

source

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

source

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

I ≤ ⊥.jacobson

Documentation

Mathlib.RingTheory.AdicCompletion.Basic

Completion of a module with respect to an ideal. #

Main definitions #