Algebra instance on adic completion #
In this file we provide an algebra instance on the adic completion of a ring. Then the adic completion of any module is a module over the adic completion of the ring.
Implementation details #
We do not make a separate adic completion type in algebra case, to not duplicate all module
theoretic results on adic completions. This choice does cause some trouble though,
since I ^ n • ⊤
is not defeq to I ^ n
. We try to work around most of the trouble by
providing as much API as possible.
AdicCompletion.transitionMap
as an algebra homomorphism.
Equations
- AdicCompletion.transitionMapₐ I hmn = AlgHom.ofLinearMap (AdicCompletion.transitionMap I R hmn) ⋯ ⋯
Instances For
AdicCompletion I R
is an R
-subalgebra of ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)
.
Equations
- AdicCompletion.subalgebra I = (AdicCompletion.submodule I R).toSubalgebra ⋯ ⋯
Instances For
AdicCompletion I R
is a subring of ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)
.
Equations
- AdicCompletion.subring I = (AdicCompletion.subalgebra I).toSubring
Instances For
Equations
Equations
The canonical algebra map from the adic completion to R ⧸ I ^ n
.
This is AdicCompletion.eval
postcomposed with the algebra isomorphism
R ⧸ (I ^ n • ⊤) ≃ₐ[R] R ⧸ I ^ n
.
Equations
- AdicCompletion.evalₐ I n = let_fun h := ⋯; (↑(Ideal.quotientEquivAlgOfEq R h)).comp (AlgHom.ofLinearMap (AdicCompletion.eval I R n) ⋯ ⋯)
Instances For
AdicCauchySequence I R
is an R
-subalgebra of ℕ → R
.
Equations
- AdicCompletion.AdicCauchySequence.subalgebra I = (AdicCompletion.AdicCauchySequence.submodule I R).toSubalgebra ⋯ ⋯
Instances For
AdicCauchySequence I R
is a subring of ℕ → R
.
Equations
Instances For
The canonical algebra map from adic cauchy sequences to the adic completion.
Equations
- AdicCompletion.mkₐ I = AlgHom.ofLinearMap (AdicCompletion.mk I R) ⋯ ⋯
Instances For
Scalar multiplication of R ⧸ (I • ⊤)
on M ⧸ (I • ⊤)
. This is used in order to have
good definitional behaviour for the module instance on adic completions
Equations
- AdicCompletion.instSMulQuotientIdealHSMulTopSubmodule I = { smul := fun (r : R ⧸ I • ⊤) (x : M ⧸ I • ⊤) => Quotient.liftOn r (fun (x_1 : R) => x_1 • x) ⋯ }
Equations
- AdicCompletion.smul I = { smul := fun (r : AdicCompletion I R) (x : AdicCompletion I M) => ⟨fun (n : ℕ) => (AdicCompletion.eval I R n) r • (AdicCompletion.eval I M n) x, ⋯⟩ }
AdicCompletion I M
is naturally an AdicCompletion I R
module.
Equations
- AdicCompletion.module I = Module.mk ⋯ ⋯
Equations
- ⋯ = ⋯