Theorems · Definition · commutative algebra

IsAdicComplete.liftRingHom

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

Universal property of IsAdicComplete for rings. The lift ring map lift I f hf : R →+* S of a sequence of compatible ring maps f n : R →+* S ⧸ (I ^ n).

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

6 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRingIsAdicComplete