Isomorphism invariance of the unipotent radical

An isomorphism of finite-type commutative Hopf algebras carries connected normal smooth unipotent closed subgroups to such subgroups. Consequently it carries the greatest one to the greatest one: the defining Hopf ideal of the unipotent radical pulls back to the defining ideal of the source radical.

This file packages that equality as an isomorphism between the coordinate Hopf algebras of the two unipotent radicals. The isomorphism commutes with their coordinate quotient maps, which characterizes it uniquely and makes identity and composition functoriality available without unfolding the chosen defining ideals.

Main declarations

• TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.comapOfIso: transport a radical candidate across an ambient isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.comapOfSurjective_unipotentRadicalDefiningIdeal: the defining ideal of the unipotent radical is invariant under isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso: the induced isomorphism of unipotent radicals.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 6.45--6.46.
• A. Borel, Linear Algebraic Groups, Section 11.21.

The formal organization follows the existing center-isomorphism interface in TauCeti.Algebra.AlgebraicGroup.Center.Isomorphism.

This completes the isomorphism-invariance interface of the unipotent-radical construction in Layer 5 of the ReductiveGroups roadmap. It lets the Layer 6 structure theory use the radical independently of a chosen coordinate presentation.

theorem TauCeti.HopfIdeal.IsUnipotentRadicalCandidate.comapOfIso {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} {I : HopfIdeal k ↑K.obj} (hI : IsUnipotentRadicalCandidate K I) (e : H ≅ K) : IsUnipotentRadicalCandidate H (I.comapOfSurjective (FiniteTypeCommHopfAlgCat.toBialgHom e.hom) ⋯)

Pulling a unipotent-radical candidate back across an ambient isomorphism gives a unipotent-radical candidate in the source.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.comapOfSurjective_unipotentRadicalDefiningIdeal {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) : K.unipotentRadicalDefiningIdeal.comapOfSurjective (toBialgHom e.hom) ⋯ = H.unipotentRadicalDefiningIdeal

An ambient isomorphism pulls the defining ideal of the target's unipotent radical back to the defining ideal of the source's unipotent radical.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) : H.unipotentRadical ≅ K.unipotentRadical

An isomorphism of finite-type commutative Hopf algebras induces an isomorphism of their unipotent radicals.

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso e = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.FiniteTypeCommHopfAlgCat.quotientIsoOfIso e K.unipotentRadicalDefiningIdeal

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalCoordinateMap_comp_unipotentRadicalIsoOfIso_hom {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) : CategoryTheory.CategoryStruct.comp H.unipotentRadicalCoordinateMap (unipotentRadicalIsoOfIso e).hom = CategoryTheory.CategoryStruct.comp e.hom K.unipotentRadicalCoordinateMap

The isomorphism of unipotent radicals commutes with the coordinate quotient maps.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalCoordinateMap_comp_unipotentRadicalIsoOfIso_inv {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) : CategoryTheory.CategoryStruct.comp K.unipotentRadicalCoordinateMap (unipotentRadicalIsoOfIso e).inv = CategoryTheory.CategoryStruct.comp e.inv H.unipotentRadicalCoordinateMap

The inverse isomorphism of unipotent radicals commutes with the coordinate quotient maps.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadical_hom_ext {k : Type u} [Field k] {H X : FiniteTypeCommHopfAlgCat k} {f g : H.unipotentRadical ⟶ X} (h : CategoryTheory.CategoryStruct.comp H.unipotentRadicalCoordinateMap f = CategoryTheory.CategoryStruct.comp H.unipotentRadicalCoordinateMap g) : f = g

A morphism out of a unipotent radical is determined by its composite with the coordinate quotient map.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadical_hom_ext_iff {k : Type u} [Field k] {H X : FiniteTypeCommHopfAlgCat k} {f g : H.unipotentRadical ⟶ X} : f = g ↔ CategoryTheory.CategoryStruct.comp H.unipotentRadicalCoordinateMap f = CategoryTheory.CategoryStruct.comp H.unipotentRadicalCoordinateMap g

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso_refl {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} : unipotentRadicalIsoOfIso (CategoryTheory.Iso.refl H) = CategoryTheory.Iso.refl H.unipotentRadical

The isomorphism induced by the identity isomorphism is the identity on the unipotent radical.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso_trans {k : Type u} [Field k] {H K L : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) (f : K ≅ L) : unipotentRadicalIsoOfIso (e ≪≫ f) = unipotentRadicalIsoOfIso e ≪≫ unipotentRadicalIsoOfIso f

Isomorphisms induced on unipotent radicals respect composition.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalIsoOfIso_symm {k : Type u} [Field k] {H K : FiniteTypeCommHopfAlgCat k} (e : H ≅ K) : (unipotentRadicalIsoOfIso e).symm = unipotentRadicalIsoOfIso e.symm

The inverse of the isomorphism induced on unipotent radicals is the isomorphism induced by the inverse ambient isomorphism.