Theorems · Definition · commutative algebra

IsAdicComplete.liftAlgHom

{R : Type u_3} →
  {S : Type u_4} →
    {A : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (I : Ideal S) →
              [IsAdicComplete I S] →
                [inst_4 : CommRing A] →
                  [inst_5 : Algebra R A] →
                    (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) →
                      (∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) → A →ₐ[R] S

AlgHom version of IsAdicCompletion.liftRingHom.

Defined in

Mathlib.RingTheory.AdicCompletion.RingHom

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsAdicCompleteCommRingAlgebra