Lift of ring homomorphisms to adic completions

Let R, S be rings, I be an ideal of S. In this file we prove that a compatible family of ring homomorphisms from a ring R to S ⧸ I ^ n can be lifted to a ring homomorphism R →+* AdicCompletion I S. If S is I-adically complete, then this compatible family of ring homomorphisms can be lifted to a ring homomorphism R →+* S.

Main definitions

• IsAdicComplete.liftRingHom: if R is I-adically complete, then a compatible family of ring maps S →+* R ⧸ I ^ n can be lifted to a unique ring map S →+* R. Together with mk_liftRingHom_apply and eq_liftRingHom, it gives the universal property of R being I-adically complete.

noncomputable def IsAdicComplete.liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [CommRing S] (I : Ideal S) [IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {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).

@[simp]

theorem IsAdicComplete.of_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [CommRing S] (I : Ideal S) [IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (x : R) : (AdicCompletion.of I S) ((liftRingHom I f ⋯) x) = (AdicCompletion.liftRingHom I f ⋯) x

@[simp]

theorem IsAdicComplete.ofAlgEquiv_comp_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [CommRing S] (I : Ideal S) [IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) : (↑(AdicCompletion.ofAlgEquiv I)).comp (liftRingHom I f ⋯) = AdicCompletion.liftRingHom I f ⋯

@[simp]

theorem IsAdicComplete.mk_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [CommRing S] (I : Ideal S) [IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (n : ℕ) (x : R) : (Ideal.Quotient.mk (I ^ n)) ((liftRingHom I f ⋯) x) = (f n) x

The composition of lift linear map lift I f hf : R →+* S with the canonical projection S →+* S ⧸ (I ^ n) is f n .

@[simp]

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

theorem IsAdicComplete.eq_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [CommRing S] (I : Ideal S) [IsAdicComplete I S] (f : (n : ℕ) → R →+* S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorPow I hle).comp (f n) = f m) (F : R →+* S) (hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)).comp F = f n) : F = liftRingHom I f ⋯

Uniqueness of the lift. Given a compatible family of linear maps f n : R →ₗ[R] S ⧸ (I ^ n). If F : R →+* S makes the following diagram commute

  R
  | \
 F|  \ f n
  |   \
  v    v
  S --> S ⧸ (I ^ n)

Then it is the map IsAdicComplete.lift.

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

AlgHom version of IsAdicCompletion.liftRingHom.

@[simp]

theorem IsAdicComplete.mk_liftAlgHom {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [Algebra R S] (I : Ideal S) [IsAdicComplete I S] [CommRing A] [Algebra R A] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (n : ℕ) (x : A) : (Ideal.Quotient.mk (I ^ n)) ((liftAlgHom I f ⋯) x) = (f n) x

@[simp]

theorem IsAdicComplete.mkₐ_comp_liftAlgHom {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [Algebra R S] (I : Ideal S) [IsAdicComplete I S] [CommRing A] [Algebra R A] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (n : ℕ) : (Ideal.Quotient.mkₐ R (I ^ n)).comp (liftAlgHom I f ⋯) = f n

theorem IsAdicComplete.algHom_ext {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommRing R] [CommRing S] [Algebra R S] (I : Ideal S) [IsAdicComplete I S] [CommRing A] [Algebra R A] {f g : A →ₐ[R] S} (H : ∀ (n : ℕ), (Ideal.Quotient.mkₐ R (I ^ n)).comp f = (Ideal.Quotient.mkₐ R (I ^ n)).comp g) : f = g

theorem IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq' {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [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) {m n : ℕ} (hle : m ≤ n) : (Ideal.Quotient.factorPow I ⋯).comp (f n) = f m

RingHom variant of IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq.

noncomputable def IsAdicComplete.StrictMono.liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [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) [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.

@[simp]

theorem IsAdicComplete.StrictMono.mk_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [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) [IsAdicComplete I S] {n : ℕ} (x : R) : (Ideal.Quotient.mk (I ^ a n)) ((liftRingHom I ha f ⋯) x) = (f n) x

@[simp]

theorem IsAdicComplete.StrictMono.mk_comp_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [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) [IsAdicComplete I S] {n : ℕ} : (Ideal.Quotient.mk (I ^ a n)).comp (liftRingHom I ha f ⋯) = f n

theorem IsAdicComplete.StrictMono.eq_liftRingHom {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [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) [IsAdicComplete I S] {F : R →+* S} (hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n) : F = liftRingHom I ha f ⋯