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

theorem AdicCompletion.transitionMap_map_pow {R : Type u_1} [CommRing R] (I : Ideal R) {m : ℕ} {n : ℕ} {a : ℕ} (hmn : m ≤ n) (x : R ⧸ I ^ n • ⊤) : (AdicCompletion.transitionMap I R hmn) (x ^ a) = (AdicCompletion.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 = let f := Subtype.val; Function.Injective.commRing f ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• AdicCompletion.instAlgebra I = Algebra.mk { toFun := fun (r : R) => ⟨(algebraMap R ((n : ℕ) → R ⧸ I ^ n • ⊤)) r, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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

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

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 (AdicCompletion.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 (AdicCompletion.AdicCauchySequence I R)

Equations

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

noncomputable instance AdicCompletion.instNatCastAdicCauchySequence {R : Type u_1} [CommRing R] (I : Ideal R) : NatCast (AdicCompletion.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 (AdicCompletion.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 (AdicCompletion.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 (AdicCompletion.AdicCauchySequence I R)

Equations

• AdicCompletion.instCommRingAdicCauchySequence I = let f := Subtype.val; Function.Injective.commRing f ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• AdicCompletion.instAlgebraAdicCauchySequence I = Algebra.mk { toFun := fun (r : R) => ⟨(algebraMap R (ℕ → R)) r, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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

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

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

noncomputable 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

noncomputable 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 • ⊤)) ⋯ ⋯

noncomputable 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

• ⋯ = ⋯

noncomputable 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

noncomputable 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 ⋯ ⋯

noncomputable 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

• ⋯ = ⋯