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.