Formally smooth algebras and adic completion

Let A be a formally smooth R-algebra. Then any algebra map A →ₐ[R] S ⧸ I lifts to an algebra map A →ₐ[R] S if S is I-adically complete.

This is used in the proof that a smooth algebra over a Noetherian ring is flat (see Mathlib.RingTheory.Smooth.Flat).

theorem Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} [CommRing S] [Algebra R S] [FormallySmooth R A] {I : Ideal S} (f : A →ₐ[R] S ⧸ I) : ∃ (g : A →ₐ[R] AdicCompletion I S), (AlgHom.restrictScalars R (AdicCompletion.evalOneₐ I)).comp g = f

If A is formally smooth over R, any map A →ₐ[R] S ⧸ I lifts to A →ₐ[R] AdicCompletion I S.

theorem Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} [CommRing S] [Algebra R S] [FormallySmooth R A] {I : Ideal S} [IsAdicComplete I S] (f : A →ₐ[R] S ⧸ I) : ∃ (g : A →ₐ[R] S), (Ideal.Quotient.mkₐ R I).comp g = f

If A is formally smooth over R, any map A →ₐ[R] S ⧸ I lifts to A →ₐ[R] S if S is I-adically complete. See Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq for a version about AdicCompletion.

theorem Algebra.FormallySmooth.exists_kerProj_comp_eq_id {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} [CommRing S] [Algebra R S] [FormallySmooth R A] (f : S →ₐ[R] A) (hf : Function.Surjective ⇑f) : ∃ (g : A →ₐ[R] AdicCompletion (RingHom.ker f) S), (AdicCompletion.kerProj hf).comp g = AlgHom.id R A

If A is formally smooth over R, the projection from the adic completion of S at the kernel of f : S →ₐ[R] A has a section.