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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• AdicCompletion.instMul I = { mul := fun (x y : AdicCompletion I R) => ⟨↑x * ↑y, ⋯⟩ }

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

Equations

• AdicCompletion.instOne I = { one := ⟨1, ⋯⟩ }

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

Equations

• AdicCompletion.instNatCast I = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

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

Equations

• AdicCompletion.instIntCast I = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

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

Equations

• AdicCompletion.instPowNat I = { pow := fun (x : AdicCompletion I R) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

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

Equations

• AdicCompletion.instCommRing I = Function.Injective.commRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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)

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• AdicCompletion.evalₐ I n = (↑(Ideal.quotientEquivAlgOfEq R ⋯)).comp (AlgHom.ofLinearMap (AdicCompletion.eval I R 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)

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.

Equations

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

noncomputable 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

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

Equations

• AdicCompletion.instMulAdicCauchySequence I = { mul := fun (x y : AdicCompletion.AdicCauchySequence I R) => ⟨↑x * ↑y, ⋯⟩ }

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

Equations

• AdicCompletion.instOneAdicCauchySequence I = { one := ⟨1, ⋯⟩ }

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

Equations

• AdicCompletion.instNatCastAdicCauchySequence I = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩ }

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

Equations

• AdicCompletion.instIntCastAdicCauchySequence I = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }

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

Equations

• AdicCompletion.instPowAdicCauchySequenceNat I = { pow := fun (x : AdicCompletion.AdicCauchySequence I R) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

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

Equations

• AdicCompletion.instCommRingAdicCauchySequence I = Function.Injective.commRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

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

@[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

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_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 • ⊤)

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

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

Equations

• AdicCompletion.module I = { toSMul := AdicCompletion.smul I, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

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.

Equations

• AdicCompletion.liftRingHom I f hf = { toFun := fun (x : R) => ⟨fun (n : ℕ) => (Submodule.factor ⋯) ((f n) x), ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

@[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