Theorems · Definition · commutative algebra

AdicCompletion.sumInv

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

If ι is finite, we use the equivalence of sum and product to obtain an inverse for AdicCompletion.sum from AdicCompletion.pi.

Defined in

Mathlib.RingTheory.AdicCompletion.Functoriality

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleFintype