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) : (AdicCompletion.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) : (AdicCompletion.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 • ⊤) : (AdicCompletion.transitionMap I R hmn) (x * y) = (AdicCompletion.transitionMap I R hmn) x * (AdicCompletion.transitionMap I R hmn) y

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.

Equations

• AdicCompletion.transitionMapₐ I hmn = AlgHom.ofLinearMap (AdicCompletion.transitionMap I R hmn) ⋯ ⋯

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

Equations

• AdicCompletion.subalgebra I = (AdicCompletion.submodule I R).toSubalgebra ⋯ ⋯

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

Equations

• AdicCompletion.subring I = (AdicCompletion.subalgebra I).toSubring

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

Equations

• AdicCompletion.instCommRing I = inferInstanceAs (CommRing ↥(AdicCompletion.subring I))

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

Equations

• AdicCompletion.instAlgebra I = inferInstanceAs (Algebra R ↥(AdicCompletion.subalgebra I))

@[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 : AdicCompletion I R) (y : AdicCompletion I R) : ↑(x * y) n = ↑x n * ↑y n

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.

Equations

• AdicCompletion.evalₐ I n = let_fun h := ⋯; (↑(Ideal.quotientEquivAlgOfEq R h)).comp (AlgHom.ofLinearMap (AdicCompletion.eval I R n) ⋯ ⋯)

@[simp]

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

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.

Equations

• AdicCompletion.AdicCauchySequence.subalgebra I = (AdicCompletion.AdicCauchySequence.submodule I R).toSubalgebra ⋯ ⋯

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

AdicCauchySequence I R is a subring of ℕ → R.

Equations

• AdicCompletion.AdicCauchySequence.subring I = (AdicCompletion.AdicCauchySequence.subalgebra I).toSubring

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

Equations

• AdicCompletion.instCommRingAdicCauchySequence I = inferInstanceAs (CommRing ↥(AdicCompletion.AdicCauchySequence.subring I))

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

Equations

• AdicCompletion.instAlgebraAdicCauchySequence I = inferInstanceAs (Algebra R ↥(AdicCompletion.AdicCauchySequence.subalgebra I))

@[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 : AdicCompletion.AdicCauchySequence I R) (g : AdicCompletion.AdicCauchySequence I R) : ↑(f * g) n = ↑f n * ↑g n

@[simp]

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

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

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

Equations

• AdicCompletion.mkₐ I = AlgHom.ofLinearMap (AdicCompletion.mk I R) ⋯ ⋯

@[simp]

theorem AdicCompletion.evalₐ_mkₐ {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x : AdicCompletion.AdicCauchySequence I R) : (AdicCompletion.evalₐ I n) ((AdicCompletion.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 : AdicCompletion.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_2} [AddCommGroup M] [Module R M] {m : ℕ} {n : ℕ} (hmn : m ≤ n) (r : AdicCompletion.AdicCauchySequence I R) (x : AdicCompletion.AdicCauchySequence I M) : ↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)

instance AdicCompletion.instSMulQuotientIdealHSMulTopSubmodule {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [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

Equations

• AdicCompletion.instSMulQuotientIdealHSMulTopSubmodule I = { smul := fun (r : R ⧸ I • ⊤) (x : M ⧸ I • ⊤) => Quotient.liftOn r (fun (x_1 : R) => x_1 • x) ⋯ }

theorem AdicCompletion.mk_smul_mk {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [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_2} [AddCommGroup M] [Module R M] (n : ℕ) (r : AdicCompletion I R) (x : M ⧸ I ^ n • ⊤) : ↑r n • x = (AdicCompletion.evalₐ I n) r • x

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

Equations

• AdicCompletion.instModuleQuotientIdealHSMulTopSubmodule I = Function.Surjective.moduleLeft (Ideal.Quotient.mk (I • ⊤)) ⋯ ⋯

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

Equations

• ⋯ = ⋯

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

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

@[simp]

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

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

AdicCompletion I M is naturally an AdicCompletion I R module.

Equations

• AdicCompletion.module I = Module.mk ⋯ ⋯

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

Equations

• ⋯ = ⋯