Unipotent radicals and quotient images #
This file supplies the common reduction used to identify a unipotent radical with the kernel of a quotient homomorphism. Once the image of the radical in the target is trivial, maximality gives one ideal containment and triviality gives the other.
Main declaration #
TauCeti.FiniteTypeCommHopfAlgCat. unipotentRadicalDefiningIdeal_eq_kernelHopfIdeal_of_quotient_image_eq_augmentation: a unipotent-radical candidate kernel is the radical when the radical has trivial image.
This reduction supports identifying kernels of quotient homomorphisms with unipotent radicals.
theorem
TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_kernelHopfIdeal_of_quotient_image_eq_augmentation
{k : Type u}
[Field k]
(H : FiniteTypeCommHopfAlgCat k)
(D : CommHopfAlgCat k)
(f : D ⟶ H.obj)
(hf : HopfIdeal.IsUnipotentRadicalCandidate H (CommHopfAlgCat.kernelHopfIdeal f))
(himage :
HopfIdeal.ker
(CommHopfAlgCat.Hom.hom
(CategoryTheory.CategoryStruct.comp f (CommHopfAlgCat.mkQuotient H.obj H.unipotentRadicalDefiningIdeal))) = HopfIdeal.augmentation k ↑D)
:
A unipotent-radical candidate kernel is the unipotent radical if the image of the radical in the target is trivial. The image is represented by the kernel of the composite coordinate map.
theorem
TauCeti.FiniteTypeCommHopfAlgCat.smoothUnipotent_image_quotient_unipotentRadical
{k : Type u}
[Field k]
(H : FiniteTypeCommHopfAlgCat k)
{D : CommHopfAlgCat k}
[Algebra.FiniteType k ↑D]
(f : D ⟶ H.obj)
:
smoothCommHopfAlgProperty k
(CommHopfAlgCat.image
(CategoryTheory.CategoryStruct.comp f (CommHopfAlgCat.mkQuotient H.obj H.unipotentRadicalDefiningIdeal))) ∧ geometricallyUnipotentPointsCommHopfAlgProperty k
(CommHopfAlgCat.image
(CategoryTheory.CategoryStruct.comp f (CommHopfAlgCat.mkQuotient H.obj H.unipotentRadicalDefiningIdeal)))
The image of the unipotent radical under a homomorphism out of its ambient group is smooth and geometrically unipotent.