Surjectivity of the differential of a formally smooth morphism #
A formally smooth morphism of affine monoid schemes induces a surjection on tangent spaces at the identity, with values in any commutative coefficient algebra. No finite presentation, field, or smoothness assumption on either monoid is needed.
For affine groups, this supplies the surjectivity term of the tangent sequence of a smooth morphism, and hence the dimension formula for its scheme-theoretic kernel.
References #
- J. S. Milne, Algebraic Groups (2017), §1.e, Proposition 1.63, for the relation between smoothness, differential surjectivity, and kernel dimensions for group varieties; §10.b, 10.6, and Appendix A.51 for the dual-number description of Lie and tangent spaces.
theorem
TauCeti.derivationComp_surjective_of_formallySmooth
{R : Type u_1}
{A : Type u_2}
{A' : Type u_3}
{B : Type u_4}
[CommRing R]
[CommRing A]
[Bialgebra R A]
[CommRing A']
[Bialgebra R A']
[CommRing B]
[Algebra R B]
(φ : A' →ₐc[R] A)
(hφ : (↑φ).FormallySmooth)
:
A formally smooth coordinate morphism induces a surjection on counit-valued derivations. This is surjectivity of the differential of the corresponding affine monoid morphism.