Lie dimensions of kernels of formally smooth group morphisms #
For a formally smooth affine group morphism G → H with finite-dimensional tangent space
at the identity of G, the dimensions satisfy dim Lie(ker f) + dim Lie(H) = dim Lie(G).
The groups themselves need not be smooth. Formal smoothness gives the surjectivity of the
differential, and CommHopfAlgCat.kernelLieEquiv identifies its 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.CommHopfAlgCat.finrank_kernelLie_add_finrank_lie_of_formallySmooth
{k : Type u}
[Field k]
{H K : CommHopfAlgCat k}
[Module.Finite k (Derivation k (↑K) (Bialgebra.CounitAlgebra k (↑K) k))]
(f : H ⟶ K)
(hf : (↑(CommHopfAlgCat.Hom.hom f)).FormallySmooth)
:
Module.finrank k
(Derivation k (↑K ⧸ (kernelHopfIdeal f).toIdeal)
(Bialgebra.CounitAlgebra k (↑K ⧸ (kernelHopfIdeal f).toIdeal) k)) + Module.finrank k (Derivation k (↑H) (Bialgebra.CounitAlgebra k (↑H) k)) = Module.finrank k (Derivation k (↑K) (Bialgebra.CounitAlgebra k (↑K) k))
For a formally smooth affine group morphism, the Lie dimensions of its kernel and target
add to the Lie dimension of its source. Only the source tangent space must be finite-dimensional.
The coordinate morphism f : H ⟶ K represents the group morphism Spec K → Spec H.