Surjectivity of the Lie differential of a formally smooth morphism #
A formally smooth morphism of affine monoid schemes induces a surjective Lie algebra morphism on tangent spaces at the identity, with values in any commutative coefficient algebra. For affine groups, this gives the surjectivity needed for the Lie-dimension formula for a 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.derivationCompLieHom_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)
:
The Lie differential of a formally smooth affine monoid morphism is surjective.