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
Instances For
AdicCompletion I R
is a subring of ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)
.
Equations
Instances For
Equations
- AdicCompletion.instMul I = { mul := fun (x y : AdicCompletion I R) => ⟨↑x * ↑y, ⋯⟩ }
Equations
- AdicCompletion.instPowNat I = { pow := fun (x : AdicCompletion I R) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }
Equations
- AdicCompletion.instCommRing I = Function.Injective.commRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
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 = (↑(Ideal.quotientEquivAlgOfEq R ⋯)).comp (AlgHom.ofLinearMap (AdicCompletion.eval I R n) ⋯ ⋯)
Instances For
AdicCauchySequence I R
is an R
-subalgebra of ℕ → R
.
Equations
Instances For
AdicCauchySequence I R
is a subring of ℕ → R
.
Equations
Instances For
Equations
- AdicCompletion.instMulAdicCauchySequence I = { mul := fun (x y : AdicCompletion.AdicCauchySequence I R) => ⟨↑x * ↑y, ⋯⟩ }
Equations
- AdicCompletion.instPowAdicCauchySequenceNat I = { pow := fun (x : AdicCompletion.AdicCauchySequence I R) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }
Equations
- AdicCompletion.instCommRingAdicCauchySequence I = Function.Injective.commRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
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.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 = { toSMul := AdicCompletion.smul I, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }