Documentation

Mathlib.RingTheory.AdicCompletion.Algebra

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) :
theorem AdicCompletion.transitionMap_map_one {R : Type u_1} [CommRing R] (I : Ideal R) {m : } {n : } (hmn : m n) :
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 ) :
theorem AdicCompletion.transitionMap_map_pow {R : Type u_1} [CommRing R] (I : Ideal R) {m : } {n : } {a : } (hmn : m n) (x : R I ^ n ) :
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
Instances For
    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
    Instances For
      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
      Instances For
        noncomputable instance AdicCompletion.instMul {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instOne {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instNatCast {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instIntCast {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instPowNat {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instCommRing {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        noncomputable instance AdicCompletion.instAlgebra {R : Type u_1} [CommRing R] (I : Ideal R) :
        Equations
        @[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 : ) :

        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
        Instances For
          @[simp]
          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
          Instances For
            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
            Instances For
              Equations
              Equations
              Equations
              Equations
              Equations
              Equations
              @[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

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

              Equations
              Instances For
                @[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)
                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
                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) :
                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.instIsScalarTowerQuotientIdealHSMulTopSubmodule {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] :
                Equations
                • =
                noncomputable instance AdicCompletion.smul {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] :
                Equations
                @[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] :

                AdicCompletion I M is naturally an AdicCompletion I R module.

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