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.

Main definitions

• evalₐ: the canonical algebra map from the adic completion to R ⧸ I ^ n.

• AdicCompletion.liftRingHom: given a compatible family of ring maps R →+* S ⧸ I ^ n, the lift ring map R →+* AdicCompletion I S.

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.

theorem AdicCompletion.factor_evalₐ_eq_eval {R : Type u_1} [CommRing R] (I : Ideal R) {n : ℕ} (x : AdicCompletion I R) (h : I ^ n ≤ I ^ n • ⊤) : (Ideal.Quotient.factor h) ((evalₐ I n) x) = (eval I R n) x

theorem AdicCompletion.factor_eval_eq_evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) {n : ℕ} (x : AdicCompletion I R) (h : I ^ n • ⊤ ≤ I ^ n) : (Submodule.factor h) ((eval I R n) x) = (evalₐ I n) x

@[simp]

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

The composition map R →+* AdicCompletion I R →+* R ⧸ I ^ n equals to the natural quotient map.

theorem AdicCompletion.surjective_evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : Function.Surjective ⇑(evalₐ 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)

theorem AdicCompletion.ext_evalₐ {R : Type u_1} [CommRing R] {I : Ideal R} {x y : AdicCompletion I R} (H : ∀ (n : ℕ), (evalₐ I n) x = (evalₐ I n) y) : x = y

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

The canonical projection from the I-adic completion to R ⧸ I.

@[simp]

theorem AdicCompletion.evalOneₐ_of {R : Type u_1} [CommRing R] (I : Ideal R) (x : R) : (evalOneₐ I) ((of I R) x) = (Ideal.Quotient.mk I) x

@[simp]

theorem AdicCompletion.factorₐ_evalₐ_one {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) : (Ideal.Quotient.factor ⋯) ((evalₐ I 1) x) = (evalOneₐ I) x

theorem AdicCompletion.evalOneₐ_surjective {R : Type u_1} [CommRing R] (I : Ideal R) : Function.Surjective ⇑(evalOneₐ I)

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)

noncomputable def AdicCompletion.liftRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [CommRing S] (I : Ideal S) (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) : R →+* AdicCompletion I S

The universal property of AdicCompletion for rings. The lift ring map R →+* AdicCompletion I S of a compatible family of ring maps R →+* S ⧸ I ^ n.

theorem AdicCompletion.factor_eval_liftRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [CommRing S] (I : Ideal S) (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ) (x : R) (h : I ^ n • ⊤ ≤ I ^ n) : (Submodule.factor h) ((eval I S n) ((liftRingHom I f ⋯) x)) = (f n) x

@[simp]

theorem AdicCompletion.evalₐ_liftRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [CommRing S] (I : Ideal S) (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ) (x : R) : (evalₐ I n) ((liftRingHom I f ⋯) x) = (f n) x

@[simp]

theorem AdicCompletion.evalₐ_comp_liftRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [CommRing S] (I : Ideal S) (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ) : (↑(evalₐ I n)).comp (liftRingHom I f ⋯) = f n

noncomputable def AdicCompletion.liftAlgHom {S : Type u_5} [CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [CommRing R] [CommRing A] [Algebra R A] [Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) : A →ₐ[R] AdicCompletion I S

AlgHom version of AdicCompletion.liftRingHom.

@[simp]

theorem AdicCompletion.evalₐ_liftAlgHom {S : Type u_5} [CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [CommRing R] [CommRing A] [Algebra R A] [Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (n : ℕ) (x : A) : (evalₐ I n) ((liftAlgHom I f ⋯) x) = (f n) x

@[simp]

theorem AdicCompletion.evalOneₐ_liftAlgHom {S : Type u_5} [CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [CommRing R] [CommRing A] [Algebra R A] [Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (x : A) : (evalOneₐ I) ((liftAlgHom I f ⋯) x) = (Ideal.Quotient.factorₐ R ⋯) ((f 1) x)

noncomputable def AdicCompletion.ofAlgEquiv {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] : S ≃ₐ[S] AdicCompletion I S

When S is I-adic complete, the canonical map from S to its I-adic completion is an S-algebra isomorphism.

@[simp]

theorem AdicCompletion.ofAlgEquiv_apply {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (x : S) : (ofAlgEquiv I) x = (of I S) x

@[simp]

theorem AdicCompletion.of_ofAlgEquiv_symm {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (x : AdicCompletion I S) : (of I S) ((ofAlgEquiv I).symm x) = x

@[simp]

theorem AdicCompletion.ofAlgEquiv_symm_of {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (x : S) : (ofAlgEquiv I).symm ((of I S) x) = x

theorem AdicCompletion.mk_smul_top_ofAlgEquiv_symm {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (n : ℕ) (x : AdicCompletion I S) : (Ideal.Quotient.mk (I ^ n • ⊤)) ((ofAlgEquiv I).symm x) = (eval I S n) x

@[simp]

theorem AdicCompletion.mk_ofAlgEquiv_symm {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (n : ℕ) (x : AdicCompletion I S) : (Ideal.Quotient.mk (I ^ n)) ((ofAlgEquiv I).symm x) = (evalₐ I n) x

@[simp]

theorem AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ {S : Type u_5} [CommRing S] (I : Ideal S) [IsAdicComplete I S] (x : AdicCompletion I S) : (Ideal.Quotient.mk I) ((ofAlgEquiv I).symm x) = (evalOneₐ I) x

noncomputable def AdicCompletion.kerProj {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f) : AdicCompletion (RingHom.ker f) S →ₐ[R] A

The canonical projection from the I-adic completion of S to S ⧸ I. Defined in terms of a surjective map S →ₐ[R] A.

@[simp]

theorem AdicCompletion.kerProj_of {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f) (x : S) : (kerProj hf) ((of (RingHom.ker f) S) x) = f x

theorem AdicCompletion.kerProj_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {A : Type u_4} [CommRing A] [Algebra R A] [Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(kerProj hf)