Smooth morphisms

An R-algebra A is formally smooth if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at least one lift A →ₐ[R] B. It is smooth if it is formally smooth and of finite presentation.

We show that the property of being formally smooth extends onto nilpotent ideals, and that it is stable under R-algebra homomorphisms and compositions.

We show that smooth is stable under algebra isomorphisms, composition and localization at an element.

theorem Algebra.formallySmooth_iff (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Algebra.FormallySmooth R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

class Algebra.FormallySmooth (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Prop

An R algebra A is formally smooth if for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at least one lift A →ₐ[R] B.

See https://stacks.math.columbia.edu/tag/00TI.

• comp_surjective : ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

theorem Algebra.FormallySmooth.comp_surjective {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] [self : Algebra.FormallySmooth R A] ⦃B : Type u⦄ [CommRing B] [Algebra R B] (I : Ideal B) : I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp

theorem Algebra.FormallySmooth.exists_lift {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [_RB : Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : ∃ (f : A →ₐ[R] B), (Ideal.Quotient.mkₐ R I).comp f = g

noncomputable def Algebra.FormallySmooth.lift {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : A →ₐ[R] B

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I square-zero, this is an arbitrary lift A →ₐ[R] B.

Equations

• Algebra.FormallySmooth.lift I hI g = ⋯.choose

@[simp]

theorem Algebra.FormallySmooth.comp_lift {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) : (Ideal.Quotient.mkₐ R I).comp (Algebra.FormallySmooth.lift I hI g) = g

@[simp]

theorem Algebra.FormallySmooth.mk_lift {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) (x : A) : (Ideal.Quotient.mk I) ((Algebra.FormallySmooth.lift I hI g) x) = g x

noncomputable def Algebra.FormallySmooth.liftOfSurjective {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] {C : Type u} [CommRing C] [Algebra R C] [Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker ↑g)) : A →ₐ[R] B

For a formally smooth R-algebra A and a map f : A →ₐ[R] B ⧸ I with I nilpotent, this is an arbitrary lift A →ₐ[R] B.

Equations

• Algebra.FormallySmooth.liftOfSurjective f g hg hg' = Algebra.FormallySmooth.lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)

@[simp]

theorem Algebra.FormallySmooth.liftOfSurjective_apply {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] {C : Type u} [CommRing C] [Algebra R C] [Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker ↑g)) (x : A) : g ((Algebra.FormallySmooth.liftOfSurjective f g hg hg') x) = f x

@[simp]

theorem Algebra.FormallySmooth.comp_liftOfSurjective {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] {C : Type u} [CommRing C] [Algebra R C] [Algebra.FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective ⇑g) (hg' : IsNilpotent (RingHom.ker ↑g)) : g.comp (Algebra.FormallySmooth.liftOfSurjective f g hg hg') = f

theorem Algebra.FormallySmooth.of_equiv {R : Type u} [CommSemiring R] {A : Type u} {B : Type u} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Algebra.FormallySmooth R A] (e : A ≃ₐ[R] B) : Algebra.FormallySmooth R B

instance Algebra.FormallySmooth.mvPolynomial (R : Type u) [CommSemiring R] (σ : Type u) : Algebra.FormallySmooth R (MvPolynomial σ R)

Equations

• ⋯ = ⋯

instance Algebra.FormallySmooth.polynomial (R : Type u) [CommSemiring R] : Algebra.FormallySmooth R (Polynomial R)

Equations

• ⋯ = ⋯

theorem Algebra.FormallySmooth.comp (R : Type u) [CommSemiring R] (A : Type u) [CommSemiring A] [Algebra R A] (B : Type u) [Semiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.FormallySmooth R A] [Algebra.FormallySmooth A B] : Algebra.FormallySmooth R B

theorem Algebra.FormallySmooth.of_split {R : Type u} [CommRing R] {P : Type u} {A : Type u} [CommRing A] [Algebra R A] [CommRing P] [Algebra R P] (f : P →ₐ[R] A) [Algebra.FormallySmooth R P] (g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2) (hg : f.kerSquareLift.comp g = AlgHom.id R A) : Algebra.FormallySmooth R A

theorem Algebra.FormallySmooth.iff_split_surjection {R : Type u} [CommRing R] {P : Type u} {A : Type u} [CommRing A] [Algebra R A] [CommRing P] [Algebra R P] (f : P →ₐ[R] A) (hf : Function.Surjective ⇑f) [Algebra.FormallySmooth R P] : Algebra.FormallySmooth R A ↔ ∃ (g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2), f.kerSquareLift.comp g = AlgHom.id R A

Let P →ₐ[R] A be a surjection with kernel J, and P a formally smooth R-algebra, then A is formally smooth over R iff the surjection P ⧸ J ^ 2 →ₐ[R] A has a section.

Geometric intuition: we require that a first-order thickening of Spec A inside Spec P admits a retraction.

instance Algebra.FormallySmooth.base_change {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] (B : Type u) [CommSemiring B] [Algebra R B] [Algebra.FormallySmooth R A] : Algebra.FormallySmooth B (TensorProduct R B A)

Equations

• ⋯ = ⋯

theorem Algebra.FormallySmooth.of_isLocalization {R : Type u} {Rₘ : Type u} [CommRing R] [CommRing Rₘ] (M : Submonoid R) [Algebra R Rₘ] [IsLocalization M Rₘ] : Algebra.FormallySmooth R Rₘ

theorem Algebra.FormallySmooth.localization_base {R : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsLocalization M Rₘ] [Algebra.FormallySmooth R Sₘ] : Algebra.FormallySmooth Rₘ Sₘ

theorem Algebra.FormallySmooth.localization_map {R : Type u} {S : Type u} {Rₘ : Type u} {Sₘ : Type u} [CommRing R] [CommRing S] [CommRing Rₘ] [CommRing Sₘ] (M : Submonoid R) [Algebra R S] [Algebra R Sₘ] [Algebra S Sₘ] [Algebra R Rₘ] [Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ] [Algebra.FormallySmooth R S] : Algebra.FormallySmooth Rₘ Sₘ

class Algebra.Smooth (R : Type u) [CommSemiring R] (A : Type u) [Semiring A] [Algebra R A] : Prop

An R algebra A is smooth if it is formally smooth and of finite presentation.

In the stacks project, the definition of smooth is completely different, and tag https://stacks.math.columbia.edu/tag/00TN proves that their definition is equivalent to this.

• formallySmooth : Algebra.FormallySmooth R A
• finitePresentation : Algebra.FinitePresentation R A

theorem Algebra.Smooth.formallySmooth {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] [self : Algebra.Smooth R A] : Algebra.FormallySmooth R A

theorem Algebra.Smooth.finitePresentation {R : Type u} [CommSemiring R] {A : Type u} [Semiring A] [Algebra R A] [self : Algebra.Smooth R A] : Algebra.FinitePresentation R A

theorem Algebra.Smooth.of_equiv {R : Type u} [CommRing R] {A : Type u} {B : Type u} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Smooth R A] (e : A ≃ₐ[R] B) : Algebra.Smooth R B

Being smooth is transported via algebra isomorphisms.

theorem Algebra.Smooth.of_isLocalization_Away {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R A] (r : R) [IsLocalization.Away r A] : Algebra.Smooth R A

Localization at an element is smooth.

theorem Algebra.Smooth.comp (R : Type u) [CommRing R] (A : Type u) (B : Type u) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [Algebra.Smooth R A] [Algebra.Smooth A B] : Algebra.Smooth R B

Smooth is stable under composition.

instance Algebra.Smooth.baseChange (R : Type u) [CommRing R] (A : Type u) (B : Type u) [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Algebra.Smooth R A] : Algebra.Smooth B (TensorProduct R B A)

Smooth is stable under base change.

Equations

• ⋯ = ⋯