Theorems · Definition · commutative algebra

AdicCompletion.sum

{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)] →
              [DecidableEq ι] →
                (DirectSum ι fun j => AdicCompletion I (M j)) →ₗ[AdicCompletion I R]
                  AdicCompletion I (DirectSum ι fun j => M j)

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

Defined in

Mathlib.RingTheory.AdicCompletion.Functoriality

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleDecidableEq