Theorems · Theorem · commutative algebra

IsAdicComplete.StrictMono.eq_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)
  (hf : ∀ {m : ℕ}, (Ideal.Quotient.factorPow I ⋯).comp (f (m + 1)) = f m) [inst_2 : IsAdicComplete I S] {F : R →+* S},
  (∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n) → F = IsAdicComplete.StrictMono.liftRingHom I ha f ⋯

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRingIsAdicComplete