Sections of formally unramified algebras

Let P and B be R-algebras, with B a formally unramified P-algebra, and let σ : B →ₐ[R] R be a retraction, the algebraic form of a section of Spec B → Spec R. The composite P → B → R is a point of Spec P. Formal unramifiedness says that the conormal module ker σ / (ker σ)² of the section is generated by the equations of this point: every element of ker σ is, modulo (ker σ)², a combination of images of the kernel of P → R. When that kernel is principal and ker σ is finitely generated (as it is when B is finitely presented over R), Nakayama's lemma turns this into a single local equation for the section, away from an element r with σ r = 1.

For an étale coordinate P = R[X] of a smooth relative curve this produces the local equation of a section; see TauCeti.RingTheory.Smooth.Section.

Main results

• Algebra.FormallyUnramified.ker_le_map_ker_sup_pow_two: ker σ is generated modulo (ker σ)² by the image of the kernel of the induced point P → R.
• Algebra.FormallyUnramified.exists_smul_ker_le_span_singleton: if moreover ker σ is finitely generated and the kernel of the point P → R is generated by u, then some r with σ r = 1 satisfies r • ker σ ≤ (u).

References

• Stacks Project, Tag 00DV: Nakayama's lemma.

theorem Algebra.FormallyUnramified.ker_le_map_ker_sup_pow_two {R : Type u_1} {P : Type u_2} {B : Type u_3} [CommRing R] [CommRing P] [CommRing B] [Algebra R P] [Algebra R B] [Algebra P B] [IsScalarTower R P B] [FormallyUnramified P B] (σ : B →ₐ[R] R) : RingHom.ker σ ≤ Ideal.map (algebraMap P B) (RingHom.ker (σ.comp (IsScalarTower.toAlgHom R P B))) ⊔ RingHom.ker σ ^ 2

Let B be a formally unramified P-algebra, where P and B are R-algebras, and let σ : B →ₐ[R] R be a retraction. Then ker σ is generated modulo (ker σ)² by the image of the kernel of the composite P → B → R: the conormal module of the section is spanned by equations coming from P.

theorem Algebra.FormallyUnramified.exists_smul_ker_le_span_singleton {R : Type u_1} {P : Type u_2} {B : Type u_3} [CommRing R] [CommRing P] [CommRing B] [Algebra R P] [Algebra R B] [Algebra P B] [IsScalarTower R P B] [FormallyUnramified P B] (σ : B →ₐ[R] R) (hfg : (RingHom.ker σ).FG) {u : P} (hu : RingHom.ker (σ.comp (IsScalarTower.toAlgHom R P B)) = Ideal.span {u}) : ∃ (r : B), σ r = 1 ∧ r • RingHom.ker σ ≤ Ideal.span {(algebraMap P B) u}

Let B be an R-algebra which is formally unramified over an R-algebra P, and let σ : B →ₐ[R] R be a retraction with finitely generated kernel (for instance, B finitely presented over R, by Algebra.FinitePresentation.ker_fG_of_surjective). If the kernel of the induced point P → R is generated by a single element u, then some r ∈ B with σ r = 1 satisfies r • ker σ ≤ (u); so after inverting r, the ideal ker σ is generated by the image of u.