Theorems · Definition · commutative algebra

IsAdicComplete.StrictMono.liftRingHom

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

A variant of IsAdicComplete.liftRingHom. Only takes f n : R →+* S ⧸ I ^ (a n) from a strictly increasing sequence a n.

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

4 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRingIsAdicComplete