Theorems · Definition · commutative algebra

AdicCompletion.liftRingHom

{R : Type u_4} →
  {S : Type u_5} →
    [inst : NonAssocSemiring R] →
      [inst_1 : CommRing S] →
        (I : Ideal S) →
          (f : (n : ℕ) → R →+* S ⧸ I ^ n) →
            (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) → R →+* AdicCompletion I S

The universal property of AdicCompletion for rings. The lift ring map R →+* AdicCompletion I S of a compatible family of ring maps R →+* S ⧸ I ^ n.

Defined in

Mathlib.RingTheory.AdicCompletion.Algebra

Cited by

9 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRing