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.

theorem AdicCompletion.transitionMap_ideal_mk {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : R) : (transitionMap I R hmn) ((Ideal.Quotient.mk (I ^ n • ⊤)) x) = (Ideal.Quotient.mk (I ^ m • ⊤)) x

theorem AdicCompletion.transitionMap_map_one {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) : (transitionMap I R hmn) 1 = 1

theorem AdicCompletion.transitionMap_map_mul {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : R ⧸ I ^ n • ⊤) (y : R ⧸ I ^ n • ⊤) : (transitionMap I R hmn) (x * y) = (transitionMap I R hmn) x * (transitionMap I R hmn) y

theorem AdicCompletion.transitionMap_map_pow {R : Type u_1} [CommRing R] (I : Ideal R) {m n a : ℕ} (hmn : m ≤ n) (x : R ⧸ I ^ n • ⊤) : (transitionMap I R hmn) (x ^ a) = (transitionMap I R hmn) x ^ a

noncomputable def AdicCompletion.transitionMapₐ {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) : R ⧸ I ^ n • ⊤ →ₐ[R] R ⧸ I ^ m • ⊤

AdicCompletion.transitionMap as an algebra homomorphism.

noncomputable def AdicCompletion.subalgebra {R : Type u_1} [CommRing R] (I : Ideal R) : Subalgebra R ((n : ℕ) → R ⧸ I ^ n • ⊤)

AdicCompletion I R is an R-subalgebra of ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R).

noncomputable def AdicCompletion.subring {R : Type u_1} [CommRing R] (I : Ideal R) : Subring ((n : ℕ) → R ⧸ I ^ n • ⊤)

AdicCompletion I R is a subring of ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R).

noncomputable instance AdicCompletion.instMul {R : Type u_1} [CommRing R] (I : Ideal R) : Mul (AdicCompletion I R)

noncomputable instance AdicCompletion.instOne {R : Type u_1} [CommRing R] (I : Ideal R) : One (AdicCompletion I R)

noncomputable instance AdicCompletion.instNatCast {R : Type u_1} [CommRing R] (I : Ideal R) : NatCast (AdicCompletion I R)

noncomputable instance AdicCompletion.instIntCast {R : Type u_1} [CommRing R] (I : Ideal R) : IntCast (AdicCompletion I R)

noncomputable instance AdicCompletion.instPowNat {R : Type u_1} [CommRing R] (I : Ideal R) : Pow (AdicCompletion I R) ℕ

noncomputable instance AdicCompletion.instCommRing {R : Type u_1} [CommRing R] (I : Ideal R) : CommRing (AdicCompletion I R)

noncomputable instance AdicCompletion.instAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (I : Ideal R) [Algebra S R] : Algebra S (AdicCompletion I R)

@[simp]

theorem AdicCompletion.val_one {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : ↑1 n = 1

@[simp]

theorem AdicCompletion.val_mul {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x y : AdicCompletion I R) : ↑(x * y) n = ↑x n * ↑y n

noncomputable def AdicCompletion.evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : AdicCompletion I R →ₐ[R] R ⧸ I ^ n

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.

@[simp]

theorem AdicCompletion.evalₐ_mk {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCauchySequence I R) : (evalₐ I n) ((mk I R) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)

noncomputable def AdicCompletion.AdicCauchySequence.subalgebra {R : Type u_1} [CommRing R] (I : Ideal R) : Subalgebra R (ℕ → R)

AdicCauchySequence I R is an R-subalgebra of ℕ → R.

noncomputable def AdicCompletion.AdicCauchySequence.subring {R : Type u_1} [CommRing R] (I : Ideal R) : Subring (ℕ → R)

AdicCauchySequence I R is a subring of ℕ → R.

noncomputable instance AdicCompletion.instMulAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : Mul (AdicCauchySequence I R)

noncomputable instance AdicCompletion.instOneAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : One (AdicCauchySequence I R)

noncomputable instance AdicCompletion.instNatCastAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : NatCast (AdicCauchySequence I R)

noncomputable instance AdicCompletion.instIntCastAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : IntCast (AdicCauchySequence I R)

noncomputable instance AdicCompletion.instPowAdicCauchySequenceNat {R : Type u_1} [CommRing R] (I : Ideal R) : Pow (AdicCauchySequence I R) ℕ

noncomputable instance AdicCompletion.instCommRingAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : CommRing (AdicCauchySequence I R)

noncomputable instance AdicCompletion.instAlgebraAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : Algebra R (AdicCauchySequence I R)

@[simp]

theorem AdicCompletion.one_apply {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : ↑1 n = 1

@[simp]

theorem AdicCompletion.mul_apply {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (f g : AdicCauchySequence I R) : ↑(f * g) n = ↑f n * ↑g n

noncomputable def AdicCompletion.mkₐ {R : Type u_1} [CommRing R] (I : Ideal R) : AdicCauchySequence I R →ₐ[R] AdicCompletion I R

The canonical algebra map from adic cauchy sequences to the adic completion.

@[simp]

theorem AdicCompletion.mkₐ_apply_coe {R : Type u_1} [CommRing R] (I : Ideal R) (a : AdicCauchySequence I R) (n : ℕ) : ↑((mkₐ I) a) n = (Ideal.Quotient.mk (I ^ n • ⊤)) (↑a n)

@[simp]

theorem AdicCompletion.evalₐ_mkₐ {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCauchySequence I R) : (evalₐ I n) ((mkₐ I) x) = (Ideal.Quotient.mk (I ^ n)) (↑x n)

theorem AdicCompletion.Ideal.mk_eq_mk {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) : (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)

theorem AdicCompletion.smul_mk {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) (x : AdicCauchySequence I M) : ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

noncomputable instance AdicCompletion.instSMulQuotientIdealHSMulTopSubmodule {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] : SMul (R ⧸ I • ⊤) (M ⧸ I • ⊤)

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

theorem AdicCompletion.mk_smul_mk {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] (r : R) (x : M) : (Ideal.Quotient.mk (I • ⊤)) r • Submodule.Quotient.mk x = r • Submodule.Quotient.mk x

theorem AdicCompletion.val_smul_eq_evalₐ_smul {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] (n : ℕ) (r : AdicCompletion I R) (x : M ⧸ I ^ n • ⊤) : ↑r n • x = (evalₐ I n) r • x

noncomputable instance AdicCompletion.instModuleQuotientIdealHSMulTopSubmodule {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] : Module (R ⧸ I • ⊤) (M ⧸ I • ⊤)

instance AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] : IsScalarTower R (R ⧸ I • ⊤) (M ⧸ I • ⊤)

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

@[simp]

theorem AdicCompletion.smul_eval {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] (n : ℕ) (r : AdicCompletion I R) (x : AdicCompletion I M) : ↑(r • x) n = ↑r n • ↑x n

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

AdicCompletion I M is naturally an AdicCompletion I R module.

instance AdicCompletion.instIsScalarTower_1 {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_3} [AddCommGroup M] [Module R M] : IsScalarTower R (AdicCompletion I R) (AdicCompletion I M)