Theorems · Definition · commutative algebra

AdicCompletion.pi

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              AdicCompletion I ((j : ι) → M j) →ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I (M j)

The canonical map from the adic completion of the product to the product of the adic completions.

Defined in

Mathlib.RingTheory.AdicCompletion.Functoriality

Cited by

3 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule