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 ofI^n M
is0
.IsPrecomplete I M
: this says that every Cauchy sequence converges.IsAdicComplete I M
: this says thatM
is Hausdorff and precomplete.Hausdorffification I M
: this is the universal Hausdorff module with a map fromM
.AdicCompletion I M
: ifI
is finitely generated, then this is the universal complete module (TODO) with a map fromM
. This map is injective iffM
is Hausdorff and surjective iffM
is precomplete.
A module M
is precomplete with respect to an ideal I
if every Cauchy sequence converges.
Instances
A module M
is I
-adically complete if it is Hausdorff and precomplete.
Instances
The canonical linear map M ⧸ (I ^ n • ⊤) →ₗ[R] M ⧸ (I ^ m • ⊤)
for m ≤ n
used
to define AdicCompletion
.
Instances For
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
Instances For
The canonical linear map to the Hausdorffification.
Instances For
Universal property of Hausdorffification: any linear map to a Hausdorff module extends to a unique map from the Hausdorffification.
Instances For
Uniqueness of lift.
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
Equations
- AdicCompletion.instZero I M = { zero := ⟨0, ⋯⟩ }
Equations
- AdicCompletion.instAdd I M = { add := fun (x y : AdicCompletion I M) => ⟨↑x + ↑y, ⋯⟩ }
Equations
- AdicCompletion.instNeg I M = { neg := fun (x : AdicCompletion I M) => ⟨-↑x, ⋯⟩ }
Equations
- AdicCompletion.instSub I M = { sub := fun (x y : AdicCompletion I M) => ⟨↑x - ↑y, ⋯⟩ }
Equations
- AdicCompletion.instSMulNat I M = { smul := fun (n : ℕ) (x : AdicCompletion I M) => ⟨n • ↑x, ⋯⟩ }
Equations
- AdicCompletion.instSMulInt I M = { smul := fun (n : ℤ) (x : AdicCompletion I M) => ⟨n • ↑x, ⋯⟩ }
Equations
- AdicCompletion.instAddCommGroup I M = Function.Injective.addCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- AdicCompletion.instSMul I M = { smul := fun (r : R) (x : AdicCompletion I M) => ⟨r • ↑x, ⋯⟩ }
Equations
- AdicCompletion.instModule I M = Function.Injective.module R { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
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
The canonical linear map to the completion.
Equations
Instances For
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
A sequence ℕ → M
is an I
-adic Cauchy sequence if for every m ≤ n
,
f m ≡ f n
modulo I ^ m • ⊤
.
Instances For
The type of I
-adic Cauchy sequences.
Equations
- AdicCompletion.AdicCauchySequence I M = { f : ℕ → M // AdicCompletion.IsAdicCauchy I M f }
Instances For
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
Equations
- AdicCompletion.AdicCauchySequence.instZero I M = { zero := ⟨0, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instAdd I M = { add := fun (x y : AdicCompletion.AdicCauchySequence I M) => ⟨↑x + ↑y, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instNeg I M = { neg := fun (x : AdicCompletion.AdicCauchySequence I M) => ⟨-↑x, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instSub I M = { sub := fun (x y : AdicCompletion.AdicCauchySequence I M) => ⟨↑x - ↑y, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instSMulNat I M = { smul := fun (n : ℕ) (x : AdicCompletion.AdicCauchySequence I M) => ⟨n • ↑x, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instSMulInt I M = { smul := fun (n : ℤ) (x : AdicCompletion.AdicCauchySequence I M) => ⟨n • ↑x, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instAddCommGroup I M = Function.Injective.addCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- AdicCompletion.AdicCauchySequence.instSMul I M = { smul := fun (r : R) (x : AdicCompletion.AdicCauchySequence I M) => ⟨r • ↑x, ⋯⟩ }
Equations
- AdicCompletion.AdicCauchySequence.instModule I M = Function.Injective.module R { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
Equations
- AdicCompletion.AdicCauchySequence.instCoeFunForallNat I M = { coe := fun (f : AdicCompletion.AdicCauchySequence I M) => ↑f }
The defining property of an adic cauchy sequence unwrapped.
Construct I
-adic cauchy sequence from sequence satisfying the successive cauchy condition.
Equations
- AdicCompletion.AdicCauchySequence.mk I M f h = ⟨f, ⋯⟩
Instances For
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
Criterion for checking that an adic cauchy sequence is mapped to zero in the adic completion.
Every element in the adic completion is represented by a Cauchy sequence.
To show a statement about an element of adicCompletion I M
, it suffices to check it
on Cauchy sequences.
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' := ⋯ }