Theorems · Theorem · commutative algebra

IsAdicComplete.StrictMono.mk_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] {n : ℕ} (x : R),
  (Ideal.Quotient.mk (I ^ a n)) ((IsAdicComplete.StrictMono.liftRingHom I ha f ⋯) x) = (f n) x

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

3 results in Mathlib

Foundations

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

Assumes

NonAssocSemiringCommRingIsAdicComplete