Isomorphism invariance of the solvable radical

An isomorphism of finite-type commutative Hopf algebras carries connected normal smooth solvable closed subgroups to such subgroups. Consequently it carries the greatest one to the greatest one: the defining Hopf ideal of the solvable 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 solvable radicals. The isomorphism commutes with their coordinate quotient maps, which characterizes it uniquely and gives its identity, composition, and inverse laws.

Main declarations

• TauCeti.HopfIdeal.IsSolvableRadicalCandidate.comapOfIso: transport a radical candidate across an ambient isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.comapOfSurjective_solvableRadicalDefiningIdeal: the defining ideal of the solvable radical is invariant under isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalIsoOfIso: the induced isomorphism of solvable 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 TauCeti.Algebra.AlgebraicGroup.Unipotent.Radical.Isomorphism.

This supplies the isomorphism-invariance interface for the solvable radical required by Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap. It lets the subsequent structure theory use the radical independently of a chosen coordinate presentation.

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

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

@[simp]

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

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

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

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

Equations

• TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalIsoOfIso e = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.FiniteTypeCommHopfAlgCat.quotientIsoOfIso e K.solvableRadicalDefiningIdeal

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.solvableRadicalIsoOfIso_refl {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} : solvableRadicalIsoOfIso (CategoryTheory.Iso.refl H) = CategoryTheory.Iso.refl H.solvableRadical

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

@[simp]

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

Isomorphisms induced on solvable radicals respect composition.

@[simp]

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

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